debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Nice clean re-implementation of AbstractHoudini. And tests	akashlal	2013-04-18
\|
*	refactored og and fixed latest bug reported by chris	Unknown	2013-03-20
\|
*	added mod set checking to the linear type checker	Unknown	2013-03-13
\|
*	removed Test\GPUVerify	Unknown	2013-03-06
\|
*	Merge	Rustan Leino	2013-03-05
\|\
* \|	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \| \| \| \| \|	Codeplex repositories.
* \|	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \| \| \| \| \|	Codeplex repositories.
\| *	fixed datatype bug reported by Chris	Unknown	2013-03-05
\|/ \| \| \|	fixed function body referring to globals bug
*	fixed a bug in og	Unknown	2013-03-04
\|
*	fixed bugs in both parallel calls and linear stuff (reported by Chris)	Unknown	2013-03-03
\| \| \| \|	also added improved error reporting suggested by Chris
*	bug in OG for parallel call	Unknown	2013-03-02
\|
*	added parallel calls	Unknown	2013-03-01
\|
*	removed call forall and * args to calls	Unknown	2013-02-23
\|
*	fixed bugs in typechecking of linear sets	Unknown	2013-02-13
\| \| \| \| \|	added regressions to linear sets removed the need to supply the builtin map operations manually
*	Add another test file	Unknown	2013-02-12
\|
*	fixed another bug reported by ChrisHaw	Unknown	2013-02-12
\| \| \| \|	Added an answer file
*	finished the sample	Unknown	2013-02-05
\|
*	Further bug fixes in OG	Unknown	2013-02-05
\| \| \| \|	Added another sample
*	fixed bug in OG	Unknown	2013-02-01
\| \| \| \|	added another OG sample illustrating rely-guarantee encoding
*	handling old() in stable assertions	Unknown	2013-01-30
\| \| \| \|	bug fix in linear
*	updated answer files	Unknown	2013-01-25
\| \| \| \|	og and linear creates some rearrangement of blocks
*	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
\|
*	bug fix for interaction between inlining and loops	Unknown	2013-01-04
\|
*	More stuff for abstract houdini; updated test case	Unknown	2012-12-10
\|
*	Disengaged Dafny tests	Rustan Leino	2012-11-20
\|
*	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-22
\|\
* \|	include Test/datatypes	Unknown	2012-10-22
\| \|
\| *	Dafny: adjusted Answer file for reordering	Rustan Leino	2012-10-18
\|/
*	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: 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
\| \|
* \|	Dafny: changed iterator body to resolve to implicit fields rather than to ↵	Rustan Leino	2012-10-02
\| \| \| \| \| \| \| \|	the formal in- and yield-parameters
* \|	Dafny: incomplete snapshot of verification of iterators	Rustan Leino	2012-10-02
\| \|
\| *	Merge	Nadia Polikarpova	2012-09-29
\| \|\
\| \| *	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 and Dafny: adjustments to the test suite expected output (and a ↵	Unknown	2012-09-27
\| \| \| \| \| \| \| \| \| \| \| \|	temporary hack in FloydCycleDetect.dfy to be corrected shortly)
\| \| *	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)
\| \| *	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.
* \| \|	Dafny: compile iterators	Rustan Leino	2012-09-26
\| \| \|
* \| \|	Dafny: added test cases for resolving iterators	Rustan Leino	2012-09-25
\| \| \|
* \| \|	Dafny: added iterators; for now, only parsing and resolving (and printing ↵	Rustan Leino	2012-09-25
\| \| \| \| \| \| \| \| \| \| \| \|	and refining), no compilation or verification
\| * \|	Use expression splitting for checking calculation steps	Nadia Polikarpova	2012-09-23
\| \| \|
\| * \|	Bugfix in the translation of calc statements (oops), added more resolution ↵	Nadia Polikarpova	2012-09-21
\| \| \| \| \| \| \| \| \| \| \| \|	and verification tests
\| * \|	Added tests for parsing and resolution of calc statements	Nadia Polikarpova	2012-09-21
\| \| \|