debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Bug fix for ExplainHoudini. Made it robust under timeouts.	Unknown	2012-12-20
\|
*	AbstractHoudini: more fixes, for self-recursion	akashlal	2012-12-16
\| \| \| \|	and Bilateral at the same time.
*	AbstractHoudini: bug fixes	akashlal	2012-12-16
\|
*	AbstractHoudini: support for generating a witness	Unknown	2012-12-15
\|
*	Added some comments	akashlal	2012-12-12
\|
*	Missed checking this in.	akashlal	2012-12-12
\|
*	Merge	akashlal	2012-12-12
\|\
* \|	First implementation of ExplainHoudini	Unknown	2012-12-12
\| \|
\| *	Houdini: allow cross-dependencies between procedures that occurs when assume	Unknown	2012-12-11
\| \| \| \| \| \| \| \|	and assert commands in implementations have existential constants
* \|	More stuff for abstract houdini; updated test case	Unknown	2012-12-10
\|/
*	Bug fix for abstract-houdini	Unknown	2012-12-07
\|
*	Allow richer spec for abs-houdini	Unknown	2012-12-03
\|
*	when a query times out, all asserted candidates are dropped	Unknown	2012-11-25
\|
*	Incorporated contribution 3667, which fixes bug in /z3exe flag ↵	Rustan Leino	2012-11-20
\| \| \| \|	(http://boogie.codeplex.com/SourceControl/network/forks/stefanheule/boogiez3exefix/contribution/3667)
*	Gather set of procedures with irreducible loops.	Unknown	2012-11-18
\|
*	Minor refactorings for integrating corral	Unknown	2012-11-18
\|
*	Added Abstract Houdini: an implementation of Houdini based on abstract domains.	Unknown	2012-11-05
\| \| \| \|	Currently only predicate-abstraction domain is supported.
*	Merge	Unknown	2012-10-18
\|\
* \|	Dafny: added new SoundLoopUnrolling parameter	Unknown	2012-10-18
\| \|
\| *	Fix for parsing error in MAXSAT computation in ↵	Unknown	2012-10-08
\| \| \| \| \| \| \| \|	ProverInterface::CheckAssumptions.
* \|	added sound loop unrolling	Yannick Welsch	2012-07-03
\|/
*	Dafny: fixed merge	Rustan Leino	2012-10-04
\|
*	Merge	Rustan Leino	2012-10-04
\|\
* \|	Dafny: complete implementation of iterators	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: automatically update iterator _new field upon allocations	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: fixed compiler bug in array allocation (reported as boogie:397957)	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: good error locations for yield statements; other iterator ↵	Rustan Leino	2012-10-03
\| \| \| \| \| \| \| \|	improvements / bug fixes
* \|	Dafny: more part of verifying iterators	Rustan Leino	2012-10-03
\| \|
\| *	changed the signing to ..\InterimKey.snk	qadeer	2012-10-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
* \|	Dafny: changed iterator body to resolve to implicit fields rather than to ↵	Rustan Leino	2012-10-02
\| \| \| \| \| \| \| \|	the formal in- and yield-parameters
* \|	Dafny: handle decreases clause for iterators	Rustan Leino	2012-10-02
\| \|
* \|	Dafny: incomplete snapshot of verification of iterators	Rustan Leino	2012-10-02
\| \|
\| *	Fixed GPUVerify solution.	Unknown	2012-10-01
\| \| \| \| \| \| \| \|	Merged recent changes to BoogieDriver into GPUVerifyBoogieDriver.
\| *	Merge	Unknown	2012-10-01
\| \|\
\| * \|	Fix to abstract interpretation to match Boogie.	Unknown	2012-10-01
\| \| \|
* \| \|	Dafny: fixed compilation issue (a datatype is now allowed to be called "d")	Rustan Leino	2012-09-29
\| \| \|
\| \| *	Merge	Nadia Polikarpova	2012-09-29
\| \| \|\
\| \| \| *	Boogie: added /vcsLoad flag as a convenient way to set /vcsCores ↵	Unknown	2012-09-28
\| \| \|/ \| \|/\| \| \| \| \| \| \|	proportionally to the machine's number of cores
\| * \|	Merge	Unknown	2012-09-28
\| \|\ \
\| * \| \|	Fixed bug with uniformity analysis for havoc. Allowed barrier invariants to	Unknown	2012-09-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	support a more expressive class of expressions. Refactored thread id creation functions.
\| \| * \|	Dafny: Removed assembly reference to 'AIFramework'.	wuestholz	2012-09-28
\| \| \| \|
\| \| * \|	Fixed the build.	wuestholz	2012-09-28
\| \| \| \|
\| \| * \|	Boogie: added type 'real' with overloaded arithmetic operations plus real ↵	boehmes	2012-09-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
\| \| * \|	Added BigDec as representation for (floating-point) decimal values	boehmes	2012-09-27
\| \| \| \|
\| \| * \|	Boogie: new syntax for integer division and modulus: use div and mod instead ↵	boehmes	2012-09-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of / and %
\| \| * \|	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.
\| \| * \|	Removed abandoned Isabelle prover backend	boehmes	2012-09-27
\| \|/ /
\| * \|	Barrier invariants can now refer to local variables that are uniform.	Unknown	2012-09-26
\| \| \|
* \| \|	Dafny: compile iterators	Rustan Leino	2012-09-26
\| \| \|