debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Added an attribute to set the time limit for implementations.	wuestholz	2013-07-12
\|
*	Worked on the parallelization (task cancellation).	wuestholz	2013-07-09
\|
*	Added support in the abstract interpreter for an attribute {:identity}, ↵	Rustan Leino	2013-07-05
\| \| \| \|	which says that a function is an identity function.
*	Did some refactoring in the execution engine.	wuestholz	2013-06-14
\|
*	Worked on improving program snapshot verification.	wuestholz	2013-06-10
\|
*	Worked on improving program snapshot verification.	wuestholz	2013-06-05
\|
*	Added a feature for verifying several program snapshots (incl. result ↵	wuestholz	2013-06-02
\| \| \| \|	caching and prioritization).
*	Staged Houdini	allydonaldson	2013-04-30
\|
*	fixed datatype bug reported by Chris	Unknown	2013-03-05
\| \| \| \|	fixed function body referring to globals bug
*	Refactored code that generates an axiom for a function, and changed the ↵	Rustan Leino	2013-01-17
\| \| \| \|	pretty printing to always reflect when a function body is inlined
*	Allow attributes on procedure formals, function formals, and bound variables	Unknown	2013-01-07
\|
*	Removed old comments about "BASEMOVE" and other constructor calls, where the ↵	Unknown	2013-01-07
\| \| \| \|	conversion from Spec# into C# moved a constructor call
*	Gather set of procedures with irreducible loops.	Unknown	2012-11-18
\|
*	added sound loop unrolling	Yannick Welsch	2012-07-03
\|
*	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.
*	Move block predicator to VCGeneration	Peter Collingbourne	2012-06-18
\|
*	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).
* \|	moved class Macro to Absy	qadeer	2012-06-04
\| \| \| \| \| \| \| \| \| \|	cleanup up DefineMacro Changed SI to use macros for reach info
* \|	1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵	Unknown	2012-06-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change.
* \|	No need for extra attributes in ExtractLoops	akashlal	2012-05-28
\| \|
* \|	Merge	Unknown	2012-05-25
\|\ \
* \| \|	Adding an option for deterministicExtractLoops, that uses an alternate way ↵	Unknown	2012-05-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	to extract loops into procedures. Unsound for concurrency. Added a test in extractLoops directory.
\| * \|	more refactoring in stratified inlining	qadeer	2012-05-24
\|/ /
* \|	removed lazy inlining	qadeer	2012-04-28
\| \|
* \|	more type checking for datatypes	qadeer	2012-03-18
\|/
*	Boogie: output number of proof obligations (asserts) along with timing ↵	Rustan Leino	2012-01-09
\| \| \| \|	information when using the /trace option
*	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
*	Merge	Rustan Leino	2011-12-07
\|\
\| *	Merge	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
\|/
*	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
\|/
*	Debugging output for stratified inlining. Emit attribute on Ensures while	Unknown	2011-11-16
\| \| \| \|	printing it.
*	moved the addition of selectors and testers to program.Resolve	qadeer	2011-11-11
\|
*	deleted unused code	qadeer	2011-11-01
\|
*	Boogie: Get rid of {:inline} attributes on axioms	Michal Moskal	2011-10-27
\|
*	Boogie: removed unreachable or unused code	Rustan Leino	2011-10-27
\|
*	Dafny: Fixed an assertion violation in the "Checked" configuration.	wuestholz	2011-09-20
\|
*	Dafny: Added support for attributes on methods and constructors.	wuestholz	2011-09-16
\|
*	Fixed test failures in the "Checked" configuration.	wuestholz	2011-09-19
\|
*	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
\| \|