debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	BeginCheck now adds context.Axioms as well as the conjecture to the context.	qadeer	2010-08-29
\| \| \| \|	Also started using the new quantifier api.
*	Added a constructor to a contract class otherwise the compiler complained ↵	mikebarnett	2010-08-28
\| \| \| \|	about the default nullary one calling its base class nullary ctor, and there wasn't one.
*	Boogie: Accidentally created a service references folder in Boogie's folder ↵	tabarbe	2010-08-27
\| \| \| \|	tree. Fixed that error.
*	Boogie: Simplify: Added a contracts class that I forgot in the initial porting.	tabarbe	2010-08-27
\|
*	Dafny: fallback to ShallowType (elements of IndexField arrays seem to have ↵	sboehme	2010-08-27
\| \| \| \|	Type null)
*	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).
*	Dafny: added inlined functions making reads and updates of the heap explicit	sboehme	2010-08-27
\|
*	Boogie: Removed an incorrect Ensures clause on a void method.	tabarbe	2010-08-27
\|
*	fixed bug with function name look up	qadeer	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: Adding an autobuild and regression cmd file for Boogie and Dafny - ↵	tabarbe	2010-08-27
\| \| \| \|	Cleans and builds both projects, then executes the regressions if the build succeeded. If the build had failed, it will stop the script.
*	Boogie: Added Z3api to the build configuration.	tabarbe	2010-08-27
\|
*	Boogie: Changed a messed-up refference to Z3api back to its previous state.	tabarbe	2010-08-27
\|
*	Boogie: Basetypes port 3/3: Committing changed references	tabarbe	2010-08-27
\| \| \| \|	Z3api.csproj shouldn't get in the way this time 'round.
*	Boogie: Basetypes port 2/3: Committing new source file, deleting old one	tabarbe	2010-08-27
\|
*	Boogie: Basetypes port 1/3: Committing new sources	tabarbe	2010-08-27
\|
*	Boogie: Renaming the Basetypes sources in preparation for my port commit.	tabarbe	2010-08-27
\|
*	Bug fixes and logging for z3api	akashlal	2010-08-27
\|
*	Addint ignore file for GIT	stobies	2010-08-27
\|
*	added some more apis to Z3api	qadeer	2010-08-27
\| \| \| \|	also added a reference from BoogieDriver to z3api
*	Added a (temporary) CCE file so that Z3Api can build.	mikebarnett	2010-08-27
\|
*	simplified the push-pop business	qadeer	2010-08-27
\|
*	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: Graph port 2/3: Committing new source file, deleting old one	tabarbe	2010-08-27
\|
*	Boogie: Graph port 1/3: Committing new sources	tabarbe	2010-08-27
\|
*	Boogie: Renaming the Graph files in preparation for the commit of my port.	tabarbe	2010-08-27
\|
*	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.
*	Boogie: AIFramework port part 2/3: Committing needed source file, deleting ↵	tabarbe	2010-08-26
\| \| \| \|	unnecessarry one.
*	Boogie: AIFramework port part 1/3: Committing new sources.	tabarbe	2010-08-26
\|
*	Boogie: Renaming the AIFramework sources in preparation for committal of my ↵	tabarbe	2010-08-26
\| \| \| \|	port of the project
*	Minor additions to z3api	akashlal	2010-08-26
\|
*	bug fixes in z3api	qadeer	2010-08-26
\|
*	Boogie build failed	codeplexbot	2010-08-25
\|
*	fixed z3api so that it works on small examples now.	qadeer	2010-08-24
\|
*	Boogie build failed	codeplexbot	2010-08-24
\|
*	Chalice: working out mask transfers between concrete and abstract heaps -- ↵	kyessenov	2010-08-24
\| \| \| \|	next goal is to make this verify!
*	Chalice:	kyessenov	2010-08-24
\| \| \| \| \|	* fix bugs -- translateAssert and etran.fromPreGlobals were referring to globals by name instead of using current globals * example of finding duplicate elements in a sequence using a bitset
*	Chalice: exhale spec statement post condition in refinement block ↵	kyessenov	2010-08-23
\| \| \| \|	translation; tag global coupling assertions (bug fix)
*	Chalice: copy concrete values for every permission in coupling invariants of ↵	kyessenov	2010-08-23
\| \| \| \|	"this"
*	Report a bug in Z3 instead of evil input "?"	kyessenov	2010-08-23
\|
*	Added a short description of new flags added to Boogie.	akashlal	2010-08-23
\|
*	Disabled an expensive contract check. Instead, only check things that are ↵	akashlal	2010-08-23
\| \| \| \|	actually used.
*	Chalice:	kyessenov	2010-08-23
\| \| \| \| \| \|	* added celebrity example (theory of sequences is still weak to prove basic things...) * bug in Chalice: old in while loops is ignored, needs to be fixed if ever want to complete DSW example * evil input from Z3 makes subsequent refinement proofs unsound; need to debug before building upon DSW.chalice; the error is triggered when adding parent field to Node
*	further fixes to Z3api project trying to make it work; still a long way off.	qadeer	2010-08-23
\|
*	Boogie build failed	codeplexbot	2010-08-23
\|
*	Fixed external references to other projects in the solution.	mikebarnett	2010-08-23
\| \| \| \|	Added version.cs to the project.
*	Chalice: spec stmt was unimplementable; changed it and refined; Z3 produces ↵	kyessenov	2010-08-22
\| \| \| \|	evil input again...
*	Chalice: start of a DSW refinement	kyessenov	2010-08-22
\|