debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Boogie Provers: Changed the references from binary to project references.	tabarbe	2010-07-27
\|
*	Boogie: AssemblyInfo.cs is no longer required for the build; cce.cs is.	tabarbe	2010-07-23
\|
*	Boogie: Committing my port of simplify, along with the slightly changed ↵	tabarbe	2010-07-23
\| \| \| \|	references of simplify's dependents.
*	Boogie: Renaming Simplify.sscproj and source files in preparation for ↵	tabarbe	2010-07-23
\| \| \| \|	committing my port of Simplify.csproj.
*	Boogie: One last file to add for the port commit. Also, AssemblyInfo.ssc is ↵	tabarbe	2010-07-22
\| \| \| \|	no longer necessarry.
*	Boogie: Committing my port of the SMTLib project	tabarbe	2010-07-22
\|
*	Boogie: Renaming the source files for the SMTLib project in preparation for ↵	tabarbe	2010-07-22
\| \| \| \|	commiting my port of the project.
*	Boogie: This file is no longer necessary, with how the csproj file is ↵	tabarbe	2010-07-22
\| \| \| \|	structured.
*	Boogie: Repaired a reentrancy error in Z3/Simplify.	tabarbe	2010-07-22
\|
*	Boogie: Looks like the default namespace should be Microsoft.Boogie.Z3, ↵	tabarbe	2010-07-22
\| \| \| \|	rather than Provers.Z3. I updated that.
*	Boogie: Changed the assembly name for the Z3 project to Provers.Z3.dll, so ↵	tabarbe	2010-07-22
\| \| \| \|	that it matches the namespace.
*	Boogie: Fixing incorrect referencing of Microsoft.Contracts (the Code ↵	tabarbe	2010-07-21
\| \| \| \|	Contracts dll) in AbsInt, Isabelle, and Z3
*	Boogie: Forgot this file when I checked in the port of Z3. (cce = Code ↵	tabarbe	2010-07-21
\| \| \| \|	Contracts Extensions - utility methods for the port that are not present in Code Contracts.)
*	Boogie: Committing ported version of Z3.	tabarbe	2010-07-20
\|
*	Boogie: Typo with the renaming. Fixed	tabarbe	2010-07-20
\|
*	Boogie: Let's try that rename again, shall we?	tabarbe	2010-07-20
\|
*	Boogie: Rename didn't work. Resetting to try again	tabarbe	2010-07-20
\|
*	Boogie/Z3: Renaming the sources for Z3 in preparation for commit of my port ↵	tabarbe	2010-07-20
\| \| \| \|	of the project.
*	Boogie/Isabelle: implemented missing translation of if-then-else expressions	sboehme	2010-07-20
\|
*	Boogie: Changed how the references in AbsInt are referenced, and fixed a ↵	tabarbe	2010-07-19
\| \| \| \|	typo in the Spec# version of Z3's ProverInterface.ssc
*	Boogie: Whoops, forgot to check this in. Sorry if it broke the build.	tabarbe	2010-07-19
\|
*	<Boogie> Final removal of Isabelle's mention of a Properties.cs file	tabarbe	2010-07-16
\|
*	<Boogie> Removed the AssemblyInfo.cs file from Isabelle.	tabarbe	2010-07-16
\|
*	<Boogie> Removed references to AssemblyInfo.cs files - unnecessary for the ↵	tabarbe	2010-07-16
\| \| \| \|	building/execution of the program
*	Boogie/Isabelle: Added tags of some places that generate errors when Code ↵	tabarbe	2010-07-15
\| \| \| \|	Contracts checking is on, that should resolve once Core ports
*	<Boogie> <Isabelle> Turned off Code Contracts Runtime Checking. Will enable ↵	tabarbe	2010-07-15
\| \| \| \|	on all ports once Core is ported. <\Isabelle> <\Boogie>
*	Fixed reference to InterimKey.snk.	mikebarnett	2010-07-14
\|
*	Fixed project files to point to references correctly and also to remove ↵	mikebarnett	2010-07-14
\| \| \| \|	assembly signing information from AssemblyInfo.cs files (which since that was the only thing in BoogieDriver's assembly info, deleted that file). Now signing information is specified in the project files.
*	Boogie/Isabelle: Had to redirect some references required for building.	tabarbe	2010-07-14
\|
*	Boogie/Isabelle && Boogie/BoogieDriver: Moved the AssemblyInfo.cs files into ↵	tabarbe	2010-07-14
\| \| \| \|	the required subfolders.
*	Isabelle: No need for this file anymore.	tabarbe	2010-07-14
\|
*	Boogie/Isabelle: Yet again trying to get Prover.cs committing.	tabarbe	2010-07-14
\|
*	Boogie: As the filename suggests, I am trying to give Tortoise a kick in the ↵	tabarbe	2010-07-14
\| \| \| \|	pants here.
*	Boogie/Isabelle: Committing Isabelle port	tabarbe	2010-07-14
\|
*	Boogie: More rename snafu fixing	tabarbe	2010-07-14
\|
*	<Boogie> More rename fixing </Boogie>	tabarbe	2010-07-14
\|
*	<Boogie> <Isabelle> Fixing rename error <\Isabelle> <\Boogie>	tabarbe	2010-07-14
\|
*	<Boogie> <Isabelle> Renaming the source files of the Isabelle project in ↵	tabarbe	2010-07-14
\| \| \| \|	preparation for integrating my ported copies of that project. <\Isabelle> <\Boogie>
*	Boogie: Added stratified inlining. It is enabled using the flag ↵	akashlal	2010-07-07
\| \| \| \|	/stratifiedInline:1.
*	Boogie:	rustanleino	2010-06-22
\| \| \| \| \| \| \| \| \|	* Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below). Dafny: * Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are * Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results. * Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
*	Derive IsabelleContext from DeclFreeProverContext	stobies	2010-06-16
\|
*	Boogie:	rustanleino	2010-06-08
\| \| \| \| \| \| \| \| \|	* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it). * Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it). Dafny: * Split off some tests from Test/dafny0 into Test/dafny1. * Added Test/dafny1/UltraFilter.dfy.
*	Updated to find the latest version of Z3 (2.7) and made the algorithm ↵	wuestholz	2010-05-28
\| \| \| \|	slightly more robust.
*	Added another option for lazy inlining based on macro expansion. This ↵	qadeer	2010-05-03
\| \| \| \|	option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.
*	Updated to find the latest version of Z3 (2.6).	wuestholz	2010-05-02
\|
*	1. Fixed lazy inlining implementation so that inlined procedures use live ↵	qadeer	2010-04-30
\| \| \| \| \| \|	variable analysis as well 2. Separeted model printing from the lazy inlining option
*	1. Fixed an off-by-one error in parsing array partitions in Z3 models	qadeer	2010-04-19
\| \| \| \| \|	2. Added code for printing array partitions 3. Set UseAbstractInterpretation=false in case lazy inlining is being used
*	Fixed a bug. Call RegisterType before the collection of Select and Store ↵	qadeer	2010-04-19
\| \| \| \|	functions in TypeDeclCollector.
*	First cut of lazy inlining. The option can be turned on by the flag ↵	qadeer	2010-04-17
\| \| \| \|	/lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
*	Implement if-then-else expression.	MichalMoskal	2010-02-18
\|