debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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
\|
*	Chalice: refining lists doesn't quite work yet...	kyessenov	2010-08-22
\|
*	Chalice: limited functions are still problematic (see Calculator.chalice)	kyessenov	2010-08-22
\|
*	Chalice:	kyessenov	2010-08-22
\| \| \| \|	* coupling invariants work (with certain restrictions as described in TODO comments)
*	Boogie build failed	codeplexbot	2010-08-21
\|
*	Chalice:	kyessenov	2010-08-21
\| \| \| \| \|	* fix a compilation problem (scalac relied on old binaries) * combinator parser and state don't work well together -- added higher-order parser for method transform
*	server-side rename	kyessenov	2010-08-21
\|
*	Boogie: Changed reference of Z3api.csproj to the differently-GUIDded ↵	tabarbe	2010-08-20
\| \| \| \|	Core.csproj, rather than Core.sscproj's old GUID.
*	Boogie: Committing changed references	tabarbe	2010-08-20
\|
*	Boogie: Adding required source file, deleting no-longer-necessarry one	tabarbe	2010-08-20
\|
*	Boogie: Committing changed source files	tabarbe	2010-08-20
\|
*	Boogie: Renaming core sources in preparation for port commit	tabarbe	2010-08-20
\| \| \| \|	*The deletion part of the rename did not occur
*	Boogie: Renaming core sources in preparation for port commit	tabarbe	2010-08-20
\|
*	Added the port of Z3api. It is simply a port to the latest version of ↵	qadeer	2010-08-20
\| \| \| \|	Microsoft.Z3.dll and to C#. It does not work yet.
*	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 some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Added user option for bounding inlining depth	akashlal	2010-08-20
\|
*	Chalice: added syntax, printer and resolver for coupling invariants	kyessenov	2010-08-20
\|
*	Boogie build succeeded	codeplexbot	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 some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	VS 2010 mode for Chalice: some errors didn't show up in the window because ↵	kyessenov	2010-08-20
\| \| \| \|	positions were negative
*	Boogie: Fixed a few contracts errors	tabarbe	2010-08-19
\|
*	Boogie: Removed and completed a task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed and completed a task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed a completed task comment, added a forgotten ↵	tabarbe	2010-08-19
\| \| \| \|	Contract.EnsuresOnThrow<>()
*	Boogie: Removed a completed task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed a completed task comment	tabarbe	2010-08-19
\|
*	Boogie: Removed an old task comment	tabarbe	2010-08-19
\|
*	Chalice: more regression tests; cosmetic changes to code	kyessenov	2010-08-19
\|
*	Added recursion-bound-guided search for stratified inlining	akashlal	2010-08-19
\|