debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Dafny: compile quantifiers	rustanleino	2011-03-26
\| \| \| \| \| \|	Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges
*	Re-enabled quantifier checking in the Checked configuration.	mikebarnett	2011-03-16
\|
*	new algorithm for dead code detection (vc:doomed)	schaef	2011-03-15
\|
*	Turn off quantifier checking in the runtime checking.	mikebarnett	2011-03-14
\|
*	Replaced all dictionaries that mapped to bool (i.e., were being used to ↵	mikebarnett	2011-03-10
\| \| \| \|	implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
*	Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵	mikebarnett	2011-03-10
\| \| \| \| \| \|	dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
*	Added a new solution configuration, Checked, that builds the Checked ↵	mikebarnett	2011-03-07
\| \| \| \|	configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
*	Fix some more contracts.	mikebarnett	2011-03-07
\|
*	Fix contracts so runtime checking can be turned on.	mikebarnett	2011-03-07
\|
*	Add VCExprNAry.UniformArguments property to return arguments of nested ↵	MichalMoskal	2011-02-15
\| \| \| \|	And/Or nodes.
*	Move name-quoting (already for SMT2 not SMT1) into a seprate class	MichalMoskal	2011-02-15
\|
*	The TPTP backend works for some very limited examples	MichalMoskal	2011-01-18
\|
*	Use a made-up name when Context.Lookup() cannot find a name	MichalMoskal	2010-12-10
\|
*	Added version.cs as link to those projects that were missing it	stobies	2010-12-06
\| \| \| \|	Select 4.0 client profile on all projects
*	Factored out the ParserHelper class into a separate project and updated the ↵	wuestholz	2010-12-02
\| \| \| \| \| \|	files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
*	Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln	qadeer	2010-12-01
\|
*	Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵	qadeer	2010-11-27
\| \| \| \|	Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
*	Boogie:	rustanleino	2010-10-12
\| \| \| \| \| \|	* enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	created a new build target called z3apidebug.	qadeer	2010-08-29
\| \| \| \| \|	only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver.
*	Boogie: Commented out all occurences of repeated inherited contracts - makes ↵	tabarbe	2010-08-27
\| \| \| \|	fewer error messages when compiling with runtime checking on.
*	Boogie: Removed some errors with code contracts (commenting out ↵	tabarbe	2010-08-27
\| \| \| \|	doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
*	Boogie: Removed an incorrect Ensures clause on a void method.	tabarbe	2010-08-27
\|
*	Boogie: Changed the cce classes into one separate project, which every other ↵	tabarbe	2010-08-27
\| \| \| \|	project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
*	Boogie: Basetypes port 3/3: Committing changed references	tabarbe	2010-08-27
\| \| \| \|	Z3api.csproj shouldn't get in the way this time 'round.
*	minor error	qadeer	2010-08-27
\|
*	Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵	tabarbe	2010-08-27
\| \| \| \|	files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
*	Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵	tabarbe	2010-08-26
\| \| \| \|	Core to jive with recent changes made to the cce class.
*	Disabled an expensive contract check. Instead, only check things that are ↵	akashlal	2010-08-23
\| \| \| \|	actually used.
*	Boogie: Committing changed references	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed a few contracts errors	tabarbe	2010-08-19
\|
*	Boogie: Removed and completed a task comment	tabarbe	2010-08-19
\|
*	Chase type synonyms in arguments/results of map types when generating name ↵	MichalMoskal	2010-08-18
\| \| \| \|	(with tE:m).
*	Change Synonym type printing to what it was, use a workaround in ↵	MichalMoskal	2010-08-18
\| \| \| \|	TypeToString() instead. Add test for /typeEncoding:m.
*	Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m ↵	MichalMoskal	2010-08-18
\| \| \| \|	use separate Z3 type per Boogie type
*	Make /typeEncoding:m work with arrays	MichalMoskal	2010-08-18
\|
*	Boogie: Adding 1 more necessary source file for VCExpr, removing an ↵	tabarbe	2010-08-13
\| \| \| \|	unnecessary one
*	Boogie: Committing new source code for VCExpr	tabarbe	2010-08-13
\|
*	Boogie: Renaming VCExpr sources in preparation for port commit	tabarbe	2010-08-13
\|
*	Boogie: Added boolean code expressions (sans well-formedness checks on the ↵	rustanleino	2010-08-10
\| \| \| \|	input).
*	Boogie: Fixed a few line endings	tabarbe	2010-08-06
\|
*	Boogie: Removed trailing spaces in code	tabarbe	2010-08-04
\|
*	Fixed bug in translation of select/store arguments that are Boolean	qadeer	2010-04-20
\|
*	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.
*	Boogie:	rustanleino	2010-02-20
\| \| \| \| \| \| \| \| \| \| \|	* Bug fix: Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case) * Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants. Previously, the only option was to instrument at the beginning and end of every basic block. The new option, which is now the default, is to instrument only at the beginning of loop heads. * Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized * Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1 Boogie refactoring: * Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand * Cleaned up some parsing of command-line options
*	Implement if-then-else expression.	MichalMoskal	2010-02-18
\|
*	* Added "deprecated" comment in help message about /interprocInfer switch. ↵	rustanleino	2010-02-18
\| \| \| \| \| \| \|	The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods