debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	BoogieDriver: correctly display time taken by prover if >60 seconds	Peter Collingbourne	2012-07-30
\|
*	Boogie: formated elapsed time	Jason Koenig	2012-06-28
\|
*	integrating predication	qadeer	2012-06-19
\|
*	testing a fix in SI	qadeer	2012-06-07
\| \| \| \| \|	also changing back the output path in BoogieDriver also disabling z3api for now since it does not build
*	Merging again	Ken McMillan	2012-06-07
\|\
\| *	Trying to merge with recent changes, failing.	Ken McMillan	2012-06-05
\| \|\
\| \| *	Some changes to support expanded use of z3api.	Ken McMillan	2012-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after).
* \| \|	Boogie: add /printCFG command line option, which prints each ↵	Peter Collingbourne	2012-06-06
\|/ / \| \| \| \| \| \|	implementation's CFG in Graphviz format
* \|	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.
* \|	more refactoring in stratified inlining	qadeer	2012-05-24
\| \|
* \|	starting the implementation of the new stratified inlining API	qadeer	2012-05-21
\| \|
* \|	removed lazy inlining	qadeer	2012-04-28
\| \|
* \|	unsat core for houdini	qadeer	2012-04-27
\| \|
* \|	houdini cleanup continued	qadeer	2012-03-10
\| \|
* \|	small fix for a bug I introduced during the refactoring of InferAndVerify	qadeer	2012-03-02
\| \|
* \|	various refactorings related to houdini	qadeer	2012-03-02
\| \|
* \|	further fixes related to using uninterpreted function for error traces	qadeer	2012-02-25
\| \| \| \| \| \| \| \|	removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
* \|	bug fixes related to using ControlFlowFunction instead of labels	qadeer	2012-02-23
\|/
*	Use DateTime.UtcNow instead of DateTime.Now	stobies	2012-01-11
\| \| \| \|	see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx
*	Dafny: changed translation to be sensitive to refinement inheritance; this ↵	Rustan Leino	2012-01-09
\| \| \| \|	feature is now functional, provided the refining module does not add or change anything
*	Boogie: output number of proof obligations (asserts) along with timing ↵	Rustan Leino	2012-01-09
\| \| \| \|	information when using the /trace option
*	Merge	Rustan Leino	2011-12-05
\|\
* \|	Boogie: Added new abstract interpretation harness, which uses native Boogie ↵	Rustan Leino	2011-12-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred}
\| *	added more instrumentation to Houdini	qadeer	2011-12-05
\| \| \| \| \| \| \| \| \| \|	when vcgen fails, instead of stopping houdini, the failing vc is added to a list of blacklisted vcs fixed bug in the call graph generation when inlining is used
\| *	added a mechanism for supplying the list of input bpl files inside a .txt file	qadeer	2011-12-01
\|/
*	added some more statistics to houdini	qadeer	2011-11-24
\| \| \| \|	added a coupe more regressions for houdini+inlineDepth
*	fixed bug in the inlineDepth option for houdini	qadeer	2011-11-23
\| \| \| \|	small clean up in the inlining implementation
*	commented calls to GC.Collect()	qadeer	2011-11-18
\|
*	/contractInfer always prints the computed assignment now	qadeer	2011-11-16
\| \| \| \|	enabled the houdini regressions
*	Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵	Rustan Leino	2011-11-15
\| \| \| \|	CommandLineOptions to separate the options that belong to these 3 tools.
*	added the option /inlineDepth:n. This option defaults to -1. If the user ↵	qadeer	2011-11-13
\| \| \| \| \| \|	provides a non-negative number then that number is used to inline procedures not annotated by {:inline n} attribute.
*	moved the addition of selectors and testers to program.Resolve	qadeer	2011-11-11
\|
*	copied all attributes of the constructor (except for :constructor) to the ↵	qadeer	2011-11-09
\| \| \| \|	selector and membership functions
*	added membership tests	qadeer	2011-10-05
\|
*	implementing datatypes	qadeer	2011-10-05
\|
*	updated Houdini so it works with SMTLib	qadeer	2011-09-27
\|
*	further updates to bit vector analysis	qadeer	2011-08-09
\|
*	various changes to boogie for bitvector analysis and bctprovider	qadeer	2011-08-08
\|
*	further changes for making houdini work	qadeer	2011-08-04
\|
*	cleaned up houdini options	qadeer	2011-08-04
\|
*	Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to ↵	Unknown	2011-07-05
\| \| \| \|	the Z3 version to use
*	Avoid restarting the theorem prover for stratified inlining because it	Unknown	2011-06-25
\| \| \| \| \|	can lose context. Added a cache for FindLeastToVerify
*	Boogie: added features to help with modular verification. In particular, ↵	Rustan Leino	2011-05-13
\| \| \| \|	define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations.
*	Re-enabled quantifier checking in the Checked configuration.	mikebarnett	2011-03-16
\|
*	Turn off quantifier checking in the runtime checking.	mikebarnett	2011-03-14
\|
*	Added a new solution configuration, Checked, that builds the Checked ↵	mikebarnett	2011-03-07
\| \| \| \|	configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
*	Stratified inlining: Added concrete values to error traces. Added an extra ↵	akashlal	2011-02-17
\| \| \| \|	flag "inferLeastForUnsat".
*	Dafny: removed CEV instrumentation	rustanleino	2011-02-03
\|
*	The TPTP backend works for some very limited examples	MichalMoskal	2011-01-18
\|
*	Add functions generated in lambda-expansion of function body to top-level ↵	MichalMoskal	2010-12-17
\| \| \| \|	program declarations.