debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Worked on improving program snapshot verification.	wuestholz	2013-06-07
\|
*	Changed the prover interface to report traces for time outs and out of memory.	wuestholz	2013-05-30
\|
*	Adding background model to fixedpoint counterexamples and small code ↵	Ken McMillan	2013-05-29
\| \| \| \|	contracts fixes
*	Changed the 'CounterexampleComparer' to take traces into account.	wuestholz	2013-05-26
\|
*	Changed the 'CounterexampleComparer' to take error messages of assertions ↵	wuestholz	2013-05-24
\| \| \| \|	into account.
*	Use the new ProverInterface's Evaluate method in stratified inlinig	Unknown	2013-01-03
\| \| \| \|	(guarded by the flag /useProverEvaluate)
*	bunch of refactorings	Unknown	2012-10-03
\| \| \| \| \| \| \| \| \|	- moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
*	Removed AIFramework from Boogie -- use native trivial or native ↵	boehmes	2012-09-27
\| \| \| \| \| \| \|	interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
*	Dafny/Boogie/BVD: made Dafny plug-in for BVD work again	Rustan Leino	2012-06-08
\|
*	Removed program argument from VerifyImplementation. It is redundant since ↵	qadeer	2012-05-29
\| \| \| \| \| \|	the constructor of ConditionGeneration takes a program reference and stashes it in a field.
*	starting the implementation of the new stratified inlining API	qadeer	2012-05-21
\|
*	z3 process is killed now	qadeer	2012-05-01
\|
*	clean up in stratified inlining	qadeer	2012-04-29
\|
*	eliminated class ErrorModel	qadeer	2012-04-28
\|
*	Boogie: output number of proof obligations (asserts) along with timing ↵	Rustan Leino	2012-01-09
\| \| \| \|	information when using the /trace option
*	fixed problems with datatypes	qadeer	2011-12-29
\| \| \| \| \|	removed stale contracts in stratified inlining added test to datatypes
*	Make set iteration order deterministic	Michal Moskal	2011-12-07
\| \| \| \|	Make the set class generic
*	Boogie: Fixed a crash due to old expressions in lambda expressions that were ↵	wuestholz	2011-12-02
\| \| \| \| \| \|	not replaced after lambda expansion. (reported by Florian Egli)
*	refactoring houdini so that it creates only a single instance of z3	qadeer	2011-11-16
\|
*	Eliminated unused argument in the constructor for Checker	qadeer	2011-11-16
\|
*	Name the constant used in @MV_state function applications - otherwise we get ↵	Michal Moskal	2011-09-26
\| \| \| \|	invalid Z3 files
*	fixes to model value generation for stratified inlining	qadeer	2011-09-12
\|
*	further fixes	qadeer	2011-09-08
\|
*	partial check in regarding getting states working with stratified inlining	qadeer	2011-09-06
\|
*	added code to handle irreducible graphs	qadeer	2011-08-20
\|
*	ported all the counterexample code to Michal's new Model class; the goal is ↵	Unknown	2011-06-27
\| \| \| \|	to eliminate the class ErrorModel from the codebase.
*	early clearing of live variables and incarnation maps	qadeer	2011-06-24
\|
*	Print recorded value of any type	akashlal	2011-03-21
\|
*	Print out requested values in the counterexample trace	akashlal	2011-03-17
\|
*	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.
*	Fix contracts so runtime checking can be turned on.	mikebarnett	2011-03-07
\|
*	Stratified inlining: Added concrete values to error traces. Added an extra ↵	akashlal	2011-02-17
\| \| \| \|	flag "inferLeastForUnsat".
*	Boogie: Did some minor refactoring.	wuestholz	2010-12-10
\|
*	Construct @MV_state function only once so it doesn't get renamed to ↵	MichalMoskal	2010-12-02
\| \| \| \|	@MV_state@@0 when we have more than one procedure to verify
*	Refactoring: pulled out all code for stratified inlining to a new file.	akashlal	2010-11-23
\|
*	Dafny: a partial first crack at a Dafny model-viewer provider, including ↵	rustanleino	2010-11-01
\| \| \| \|	captureState mark-ups in the Boogie code generated from Dafny
*	Skip unchagned variables in model dumps. Fix testcase	MichalMoskal	2010-10-14
\|
*	Add interfaces for langauge providers. Start with VCC provider.	MichalMoskal	2010-10-12
\|
*	Add missing Clone() when storing incarnation maps; update testcase to make ↵	MichalMoskal	2010-10-12
\| \| \| \| \| \|	this clear Construct states in Model properly, nuke direct printing.
*	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
\|
*	Add state sequence API and creation, still untested	MichalMoskal	2010-10-08
\|
*	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
*	Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal ↵	akashlal	2010-09-05
\| \| \| \|	that it has reached the recursion bound.
*	Henrique's addition to the the ErrorHandler API to retrieve models	qadeer	2010-09-03
\|
*	Added a way of recovering counterexample paths after loop extraction. ↵	akashlal	2010-09-01
\| \| \| \|	Stable, but still buggy.
*	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).