debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Make the -mv option use the new Model class.	MichalMoskal	2010-10-12
\|
*	Boogie:	rustanleino	2010-10-12
\| \| \| \| \| \|	* enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
*	Boogie: fixed a Code Contract in the source	rustanleino	2010-10-09
\|
*	Fixes in state printing/initialization	MichalMoskal	2010-10-09
\|
*	Fix some bugs.	MichalMoskal	2010-10-09
\|
*	Add model/state printing and parsing	MichalMoskal	2010-10-09
\|
*	Add state sequence API and creation, still untested	MichalMoskal	2010-10-08
\|
*	Add the new model interface. Untested, doesn't yet include state sequence	MichalMoskal	2010-10-08
\|
*	Get rid of some CCI dependencies in Driver	MichalMoskal	2010-10-07
\|
*	Update to VS2010.	MichalMoskal	2010-10-07
\|
*	Minor fix to recursion depth in stratified inlining algorithm.	akashlal	2010-10-02
\|
*	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:	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
*	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 more stat printing	akashlal	2010-09-16
\|
*	Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal ↵	akashlal	2010-09-05
\| \| \| \|	that it has reached the recursion bound.
*	Fixed a performance issue with StratifiedInlining	akashlal	2010-09-05
\|
*	Fix for extractLoops	akashlal	2010-09-04
\|
*	Henrique's addition to the the ErrorHandler API to retrieve models	qadeer	2010-09-03
\|
*	Bug fix for StratifiedInlining. Use extra Booleans to model procedure calls, ↵	akashlal	2010-09-02
\| \| \| \|	instead of uninterpreted predicates.
*	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.
*	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: 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.
*	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.
*	bug fixes in z3api	qadeer	2010-08-26
\|
*	fixed z3api so that it works on small examples now.	qadeer	2010-08-24
\|
*	Boogie: Committing changed references	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
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Removed and completed a task comment	tabarbe	2010-08-19
\|
*	Added recursion-bound-guided search for stratified inlining	akashlal	2010-08-19
\|
*	Some reformatting and refactoring	akashlal	2010-08-18
\|
*	Added option for displaying stratified inlining's search	akashlal	2010-08-18
\|
*	Stratified inlining: Changed recursion into a loop.	akashlal	2010-08-16
\|
*	Bug fix for stratified inlining trace generation	akashlal	2010-08-16
\|
*	Added more options for stratified inlining	akashlal	2010-08-16
\|
*	Boogie: Committing changed references	tabarbe	2010-08-13
\|
*	Added the option /extractLoops to extract loops as procedure calls. If ↵	qadeer	2010-08-11
\| \| \| \|	either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
*	Fixed a contract	akashlal	2010-08-10
\|
*	Boogie: Added boolean code expressions (sans well-formedness checks on the ↵	rustanleino	2010-08-10
\| \| \| \|	input).
*	Boogie: Sorry about that - no need for the conditional compilation	tabarbe	2010-08-09
\|
*	Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.cs	tabarbe	2010-08-09
\|
*	More line ending fixups.	MichalMoskal	2010-08-06
\|