debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	made delegate a datatype	qadeer	2011-12-30
\| \| \| \|	added a DatatypeConstructor class
*	fixed problems with datatypes	qadeer	2011-12-29
\| \| \| \| \|	removed stale contracts in stratified inlining added test to datatypes
*	fixed a completeness problem in houdini with inlining	qadeer	2011-12-18
\|
*	Fixed the Boogie build.	wuestholz	2011-12-16
\|
*	Dafny: Made sure that error locations refer to the Dafny program, even if ↵	wuestholz	2011-12-15
\| \| \| \|	the /print option is used.
*	Boogie: Changed Expr.Not to keep swap arguments rather change direction of ↵	Rustan Leino	2011-12-12
\| \| \| \|	operator when negating <, <=, >=, or >
*	Merge	Rustan Leino	2011-12-07
\|\
\| *	Merge	Michal Moskal	2011-12-07
\| \|\
\| * \|	Fix atg file and add comment about Set/Variable/	Michal Moskal	2011-12-07
\| \| \|
\| * \|	Make set iteration order deterministic	Michal Moskal	2011-12-07
\| \| \| \| \| \| \| \| \| \| \| \|	Make the set class generic
* \| \|	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}
\| *	Emit attribute on a requires	akashlal	2011-12-04
\|/
*	Added option of turning off model generation in SI. Can be very expensive ↵	akashlal	2011-11-26
\| \| \| \|	sometimes.
*	fixed bug in the inlineDepth option for houdini	qadeer	2011-11-23
\| \| \| \|	small clean up in the inlining implementation
*	Merge	qadeer	2011-11-22
\|\
\| *	Boogie: don't resolve ignored types (that is, "extern" types that have been ↵	Rustan Leino	2011-11-22
\| \| \| \| \| \| \| \|	thrown out)
* \|	added support for handling duplicate axioms	qadeer	2011-11-22
\|/
*	Added lazy summary computation to stratified inlining (not finished yet)	akashlal	2011-11-20
\|
*	commented calls to GC.Collect()	qadeer	2011-11-18
\|
*	changed the semantics of requires and ensures for inlined procedures	qadeer	2011-11-17
\|
*	Boogie: fixed build error (incorrect type in Contract.Result)	Rustan Leino	2011-11-16
\|
*	Merge	akashlal	2011-11-16
\|\
\| *	Debugging output for stratified inlining. Emit attribute on Ensures while	Unknown	2011-11-16
\| \| \| \| \| \| \| \|	printing it.
* \|	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.
*	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
\|