debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Update to include all build artifacts, also from Dafny	MichalMoskal	2010-10-07
\|
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	Chalice: fix a bug where output variables of a method were not decoupled.	kyessenov	2010-10-05
\|
*	Minor fix to recursion depth in stratified inlining algorithm.	akashlal	2010-10-02
\|
*	Util: Minor changes to the LaTeX listings packages for Boogie and Dafny.	wuestholz	2010-09-30
\|
*	Boogie:	rustanleino	2010-09-24
\| \| \| \| \|	* Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time.
*	Boogie build succeeded	codeplexbot	2010-09-23
\|
*	Boogie:	rustanleino	2010-09-23
\| \| \| \| \| \|	* Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
*	Dafny: Compilation of multi-dimensional arrays	rustanleino	2010-09-21
\|
*	Boogie build succeeded	codeplexbot	2010-09-20
\|
*	Some simplifications to coverage reporting for StratifiedInlining.	akashlal	2010-09-19
\|
*	Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.	akashlal	2010-09-18
\|
*	Added test for loop extraction	akashlal	2010-09-18
\|
*	Boogie build succeeded	codeplexbot	2010-09-17
\|
*	Dafny:	rustanleino	2010-09-17
\| \| \| \| \| \|	* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation) * Changed syntax of array length from \|a\| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays. * Internally, this meant adding support for built-in classes and readonly fields
*	Added more stat printing	akashlal	2010-09-16
\|
*	Boogie build succeeded	codeplexbot	2010-09-15
\|
*	Dafny:	rustanleino	2010-09-14
\| \| \| \| \| \| \| \|	* Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations
*	Boogie build succeeded	codeplexbot	2010-09-11
\|
*	added an optimization to extract loops so that only loop targets are treated ↵	qadeer	2010-09-10
\| \| \| \|	as output variables of the extracted procedure.
*	Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal ↵	akashlal	2010-09-05
\| \| \| \|	that it has reached the recursion bound.
*	Delete unreachable Blocks of an Impl before calling ExtractLoops().	akashlal	2010-09-05
\| \| \| \|	This helps avoid a crash inside NewComputeDominators().
*	Fixed a performance issue with StratifiedInlining	akashlal	2010-09-05
\|
*	Added tests for extractloops	akashlal	2010-09-04
\|
*	Fix for extractLoops	akashlal	2010-09-04
\|
*	Henrique's addition to the the ErrorHandler API to retrieve models	qadeer	2010-09-03
\|
*	Chalice: incorporate another regression test	kyessenov	2010-09-03
\|
*	more fixes to ExtractLoops	qadeer	2010-09-03
\|
*	Added a fix to extract loops code so that it returns a more comprehensive ↵	qadeer	2010-09-03
\| \| \| \|	map of block names to original blocks.
*	Changed the interface of Parse so that it can consume a program from a Stream	akashlal	2010-09-03
\|
*	bunch of fixes related to Boogie error model generation from the Z3 error ↵	qadeer	2010-09-03
\| \| \| \|	model generation
*	Vim: add keywords to Chalice	kyessenov	2010-09-02
\|
*	VS 2010: add "spec" as keyword in Chalice	kyessenov	2010-09-02
\|
*	Chalice: added Duplicates refinement from Verification Corner video	kyessenov	2010-09-02
\|
*	Chalice: fix in refinement loop target resolution; added "spec" as a keyword ↵	kyessenov	2010-09-02
\| \| \| \|	synonym to "var"
*	Bug fix for StratifiedInlining. Use extra Booleans to model procedure calls, ↵	akashlal	2010-09-02
\| \| \| \|	instead of uninterpreted predicates.
*	fixed bug in extract loops by ensuring that loop extraction is done in ↵	qadeer	2010-09-01
\| \| \| \|	nesting order
*	Minor fix to my previous commit	akashlal	2010-09-01
\|
*	Added a way of recovering counterexample paths after loop extraction. ↵	akashlal	2010-09-01
\| \| \| \|	Stable, but still buggy.
*	Version-stamp CCE assembly	stobies	2010-09-01
\|
*	Boogie build succeeded	codeplexbot	2010-09-01
\|
*	Added a new class LoopProcedure to represent the procedures representing ↵	qadeer	2010-09-01
\| \| \| \|	extracted loops.
*	Dafny: Added Dafny solutions to the VSComp 2010 problems	rustanleino	2010-09-01
\|
*	VS2010 mode for Dafny and Boogie: updated, for example to properly deal ↵	rustanleino	2010-09-01
\| \| \| \|	with string literals
*	Boogie build succeeded	codeplexbot	2010-08-31
\|
*	Dafny: added a command-line option to change the prelude file	sboehme	2010-08-30
\|
*	added a new api to Z3apiProcessTheoremProver for asserting axioms	qadeer	2010-08-29
\|
*	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.
*	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.