debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵	Rustan Leino	2011-10-27
\| \| \| \|	as if the old /bv:z were used
*	Name the constant used in @MV_state function applications - otherwise we get ↵	Michal Moskal	2011-09-26
\| \| \| \|	invalid Z3 files
*	Boogie: use (WEIGHT 0) with the select-of-store axioms	Rustan Leino	2011-06-29
\|
*	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.