debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Support for "do_not_predicate" in predication of requires and ensures	Unknown	2012-12-20
\|
*	A simplification to predication of requires and ensures.	Unknown	2012-11-29
\|
*	Fixes to uniformity analysis.	Unknown	2012-11-29
\|
*	Fix for parsing error in MAXSAT computation in ↵	Unknown	2012-10-08
\| \| \| \|	ProverInterface::CheckAssumptions.
*	Boogie build failed	CodeplexBot	2012-10-05
\|
*	deleted unnecessary files	Unknown	2012-10-04
\|
*	Dafny: fixed merge	Rustan Leino	2012-10-04
\|
*	Merge	Rustan Leino	2012-10-04
\|\
* \|	Dafny: complete implementation of iterators	Rustan Leino	2012-10-03
\| \|
\| *	Boogie build failed	CodeplexBot	2012-10-04
\| \|
* \|	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
\| \| \|
\| \| *	Chalice: Two new test-cases for recently fixed problems.	stefanheule	2012-10-01
\| \| \|
\| \| *	Chalice: Disallow unfolding expressions in postconditions.	stefanheule	2012-10-01
\| \| \|
\| \| *	Chalice: Fix bug in detecting permissions in postconditions.	stefanheule	2012-10-01
\| \| \|
\| \| *	Chalice: Let the trigger for the function postcondition axiom be more ↵	stefanheule	2012-10-01
\| \| \| \| \| \| \| \| \| \| \| \|	permissive.
\| \| *	Updated the 'PrepareBoogieZip.bat' script.	wuestholz	2012-10-01
\| \| \|
\| \| *	Merge	stefanheule	2012-09-30
\| \| \|\
\| \| * \|	Chalice: Use new 'mod' and 'div' operators of Boogie for division and modulo.	stefanheule	2012-09-30
\| \| \| \|
\| \| * \|	Chalice: Remove superfluous comment.	stefanheule	2012-09-30
\| \| \| \|
\| \| * \|	Chalice: Clean up /percentageSupport command line option to adapt to the ↵	stefanheule	2012-09-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	usage of reals for permissions.
\| \| * \|	Chalice: Activate the test-case tests/permission-model/scaling.chalice that ↵	stefanheule	2012-09-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	was previously disabled due to performance problems.
\| \| * \|	Chalice: Fix some problems related to the use of reals in Boogie.	stefanheule	2012-09-30
\| \| \| \|
* \| \| \|	Dafny: fixed compilation issue (a datatype is now allowed to be called "d")	Rustan Leino	2012-09-29
\| \| \| \|
\| \| * \|	Chalice: Further changes to make permissions use the Boogie type real.	stefanheule	2012-09-29
\| \| \| \|
\| \| * \|	Chalice: Make permissions use the Boogie type real.	stefanheule	2012-09-29
\| \| \| \|
\| \| * \|	Chalice: Extend the Boogie AST with real literals.	stefanheule	2012-09-29
\| \| \| \|
\| \| \| *	Merge	Nadia Polikarpova	2012-09-29
\| \| \| \|\
\| \| * \| \|	Chalice (Adapt to real support in Boogie): Axiomatization of division is no ↵	stefanheule	2012-09-29
\| \| \| \|/ \| \| \|/\| \| \| \| \| \| \| \| \|	longer needed (and in fact, results in a Boogie parse error).
\| \| * \|	Boogie: updated syntax highlighting ("real")	Unknown	2012-09-28
\| \| \| \|
\| \| * \|	Dafny: removed div/mod axioms, since Boogie now interprets div/mod	Unknown	2012-09-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support
\| \| * \|	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.
\| \| * \|	Boogie build succeeded, 2 test(s) failed	CodeplexBot	2012-09-28
\| \| \| \|
\| \| * \|	Dafny: Removed assembly reference to 'AIFramework'.	wuestholz	2012-09-28
\| \| \| \|
\| \| * \|	Fixed the build.	wuestholz	2012-09-28
\| \| \| \|
\| \| * \|	Chalice: Add a test-case for a recently fixed issue.	stefanheule	2012-09-28
\| \| \| \|
\| \| * \|	Boogie build failed	CodeplexBot	2012-09-28
\| \| \| \|
\| \| * \|	Merge	Unknown	2012-09-27
\| \| \|\ \