debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	changed inlining code so that candidate preconditions and postconditions are ↵	qadeer	2011-11-15
\| \| \| \|	ignored
*	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
\|
*	Merge	qadeer	2011-11-07
\|\
\| *	Dafny: added a new /inductionHeuristic option	Rustan Leino	2011-11-04
\| \|
\| *	Dafny: added options to make Induction Heuristic apply to array index ↵	Rustan Leino	2011-11-04
\| \| \| \| \| \| \| \|	expressions
* \|	deleted unused code	qadeer	2011-11-01
\|/
*	Merge	Rustan Leino	2011-10-29
\|\
* \|	Dafny induction:	Rustan Leino	2011-10-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	* implemented induction tactic for result-less, non-mutating ghost methods * refine heuristics for determining if a variables is usefully passed to a recursive function * disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) * added command-line flags /induction and /inductionHeuristic (everything is on by default)
\| *	Boogie: Get rid of {:inline} attributes on axioms	Michal Moskal	2011-10-27
\| \|
\| *	Boogie: Get rid of {:ignore} feature on axioms	Michal Moskal	2011-10-27
\| \|
\| *	Boogie: removed unreachable or unused code	Rustan Leino	2011-10-27
\| \|
\| *	Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵	Rustan Leino	2011-10-27
\| \| \| \| \| \| \| \|	as if the old /bv:z were used
\| *	Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵	Rustan Leino	2011-10-27
\| \| \| \| \| \| \| \|	The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
\| *	Boogie: Changed default /prover to SMTLIB	Rustan Leino	2011-10-27
\|/
*	Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)	Unknown	2011-10-19
\|
*	Merge	Rustan Leino	2011-09-28
\|\
\| *	bitvector fixes	qadeer	2011-09-24
\| \|
\| *	Dafny: Fixed an assertion violation in the "Checked" configuration.	wuestholz	2011-09-20
\| \|
* \|	Merge	Rustan Leino	2011-09-17
\|\ \
\| \| *	Dafny: Added support for attributes on methods and constructors.	wuestholz	2011-09-16
\| \| \|
\| \| *	Fixed test failures in the "Checked" configuration.	wuestholz	2011-09-19
\| \|/
\| *	Added "free call" statements that don't check the precondition in the caller.	wuestholz	2011-09-14
\| \|
* \|	Dafny: generate a compiler error upon encountering an assume statement	Rustan Leino	2011-09-11
\|/ \| \| \|	Dafny: don't compile programs unless all methods have been verified (or a forced compile is requested)
*	further edits	qadeer	2011-09-01
\|
*	improved bitvector analysis	qadeer	2011-09-01
\|
*	Merge	qadeer	2011-08-29
\|\
* \|	more changes to bitvector analysis	qadeer	2011-08-29
\| \|
\| *	Merge	Michal Moskal	2011-08-29
\| \|\ \| \|/ \|/\|
\| *	Add PROVER_PATH prover option (to base options, but currently only used by ↵	Michal Moskal	2011-08-29
\| \| \| \| \| \| \| \| \| \| \| \|	SMTLib) Add support for Inspector with latest Z3/SMT2 frontend
* \|	Fixed a bug with "don't care" return value on an async call	Unknown	2011-08-24
\|/
*	Support for irreducible graphs (with extractLoops)	Unknown	2011-08-24
\|
*	reverting irreducible handling temporarily	qadeer	2011-08-21
\|\
* \|	added code to handle irreducible graphs	qadeer	2011-08-20
\| \|
* \|	deleted lazyinlining option 2 and 3	qadeer	2011-08-17
\| \| \| \| \| \| \| \|	fixed proc copy bounding
* \|	Added "procedure-copy bounding" for lazy inlining	Unknown	2011-08-10
\| \|
* \|	further updates to bit vector analysis	qadeer	2011-08-09
\| \|
* \|	more changes to bitvector analysis	qadeer	2011-08-09
\| \|
* \|	another bug fix in bct	qadeer	2011-08-08
\| \|
* \|	added a new file and fixed a bug in bct	qadeer	2011-08-08
\| \|
* \|	various changes to boogie for bitvector analysis and bctprovider	qadeer	2011-08-08
\| \|
* \|	cleaned up houdini options	qadeer	2011-08-04
\| \|
* \|	Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵	wuestholz	2011-07-15
\| \| \| \| \| \| \| \|	some trailing whitespace.
* \|	async call return value is either int or bv32	qadeer	2011-07-09
\| \|
* \|	ExtractLoops calls the same code for eliminating unreachable blocks that ↵	qadeer	2011-07-05
\| \| \| \| \| \| \| \| \| \| \| \|	normal VCgen calls. Deleted a procedure that was not being used as a result. Added an extra assume(false) at the end of each DispatchContinuation to help boogie vcgen.
* \|	Merge	Michal Moskal	2011-07-05
\|\ \
\| * \|	Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to ↵	Unknown	2011-07-05
\| \| \| \| \| \| \| \| \| \| \| \|	the Z3 version to use
\| * \|	Added the /noCheating option. (treats assume as assert and drops free.)	Jason Koenig	2011-07-01
\| \| \|
* \| \|	Allow : instead of = in options	Michal Moskal	2011-06-30
\| \|/ \|/\|
\| *	Added option to force Dafny compilation, even if verification fails.	Jason Koenig	2011-06-30
\|/