debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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)
*	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
\|
*	Merge	Unknown	2012-09-24
\|\
* \|	Fixed issue with uniformity analysis and block merging. Uniformity analysis	Unknown	2012-09-24
\| \| \| \| \| \| \| \|	now enabled by default.
\| *	Merge	stefanheule	2012-09-24
\| \|\
\| * \|	Chalice: New regression test-case.	stefanheule	2012-09-24
\| \| \|
\| * \|	Chalice: Fix type-checker incompleteness.	stefanheule	2012-09-24
\| \| \|
\| * \|	Chalice: Add new regression test case.	stefanheule	2012-09-24
\| \| \|
\| * \|	Chalice: Improve code to generate triggers for framing axiom.	stefanheule	2012-09-24
\| \| \|
\| * \|	Chalice: Fix triggers for framing axiom of known-folded locations.	stefanheule	2012-09-24
\| \| \|
\| \| *	Merge	Egor Kyshtymov	2012-09-24
\| \|/\| \|/\| \|
\| \| *	Added detailed trace functionality.	Egor Kyshtymov	2012-09-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Improved error reporting. Tidied up code.
* \| \|	Merge	Unknown	2012-09-24
\|\ \ \
* \| \| \|	Support for barrier invariants.	Unknown	2012-09-24
\| \| \| \|
\| * \| \|	Merge	Unknown	2012-09-24
\| \|\ \ \
\| * \| \| \|	added output for a test case	Unknown	2012-09-24
\| \| \| \| \|
\| \| * \| \|	DafnyExtension: adding some missing keywords (for imports)	Unknown	2012-09-21
\| \|/ / / \|/\| \| \|
\| \| * \|	Chalice: Fix soundness issue about when it is sound to keep knowledge about ↵	stefanheule	2012-09-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	predicate permission masks.
\| \| * \|	Chalice: Alternative approach to frame known-folded locations; use ↵	stefanheule	2012-09-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	quantification instead of explicit enumeration of locations.
* \| \| \|	Fixed a bug with empty big blocks.	Unknown	2012-09-21
\| \| \| \|
* \| \| \|	Merge	Unknown	2012-09-21
\|\\| \| \|
* \| \| \|	Added support for invariants about shared state.	Unknown	2012-09-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Reworked implementation of barriers. Started on support for barrier invariants.
\| * \| \|	Merge	Unknown	2012-09-21
\| \|\\| \|
\| * \| \|	Added linked list Chalice example	Unknown	2012-09-21
\| \| \| \|
\| \| * \|	Chalice: Update release script to adapt to new scala version.	stefanheule	2012-09-21
\| \| \| \|
\| \| * \|	Merge	stefanheule	2012-09-20
\| \| \|\ \
\| \| * \| \|	Chalice: New regression tests for fixed workitems 10189 and 10208.	stefanheule	2012-09-20
\| \| \| \| \|
\| \| * \| \|	Chalice: New regression test case from workitem 10221.	stefanheule	2012-09-20
\| \|/ / /
\| \| * \|	Merge	Unknown	2012-09-19
\| \| \|\ \ \| \| \|/ / \| \|/\| \|
\| \| * \|	Boogie: improved parser makefile	Unknown	2012-09-19
\| \| \| \|
\| * \| \|	Chalice: Fix bug of computing the function height.	stefanheule	2012-09-19
\| \| \| \|
\| * \| \|	Merge	stefanheule	2012-09-19
\| \|\ \ \ \| \|/ / / \|/\| \| \|
* \| \| \|	When uniformity analysis is disabled, no procedures (even the kernel entry	Unknown	2012-09-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	point) will be regarded as uniform. This simplification avoids various edge cases.
\| * \| \|	Chalice: Use the framing function instead of the limited function in ↵	stefanheule	2012-09-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	triggers to make them more permissive (and for instance fix a recent test failure).
* \| \| \|	Merge	Unknown	2012-09-18
\|\ \ \ \
* \| \| \| \|	Uniformity analysis. Patch by Peter Collingbourne.	Unknown	2012-09-18
\| \| \| \| \|
\| \| * \| \|	Chalice: Added a test case (general-tests/triggers) to test the ↵	Unknown	2012-09-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	trigger-generation feature
\| \| * \| \|	Chalice: Updated linkedlist.chalice to include quantified specification, but ↵	Unknown	2012-09-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	now the test does not pass.. this is a problem with triggering the framing axiom, if the way the function is mentioned in a state is under a quantifier... but it's about to be fixed :)
\| \| * \| \|	Chalice: Updated trigger generation to duplicate the entire quantifier in ↵	Unknown	2012-09-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	cases where different numbers of extra boolean variables are needed to generate different trigger sets. In this case, the resulting quantified assertions are conjoined together in the result.
\| * \| \| \|	Dafny: Updated a test that would take a long time (almost 2h) to verify with ↵	wuestholz	2012-09-18
\| \| \|/ / \| \|/\| \| \| \| \| \| \| \| \| \|	Z3 4.1.
\| \| * \|	Chalice: modified trigger generation for quantifiers to include the use of ↵	Unknown	2012-09-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	additional boolean variables to replace any sub-expressions that would be problematic in a candidate trigger (logical operators and comparison operators are forbidden). These extra variables are used in the triggers but not in the bnody of the quantifier. However, they need to be quantified over as well, and this creates a problem if different trigger sets employ different sets of extra variables. For the moment, the implementation groups all of the trigger sets by the sets of extra variables they use, and only outputs the first (in practice, often the only) such group. Hopefully this will be improved on soon.
* \| \| \|	Dualisation modified so that global arrays are not dualised, and group-shared	Unknown	2012-09-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	arrays are turned into 2D maps with first index type bool. Thread 1 always indexes into "true", while threads 2 indexes into "samegroup" (a formula which is true iff threads 1 and 2 are in the same group). Thus if the threads are in different groups they operate on different shared arrays, but if they are in the same group they operate on the same shared array. This paves the way for implementing support for barrier invariants.
\| * \| \|	Dafny: some test cases for "calc" (very cool!)	Unknown	2012-09-17
\| \| \| \|
\| \| * \|	Automatic Merge	Unknown	2012-09-17
\| \| \|\ \
\| \| * \| \|	Chalice: modified Tr() to only generate a real list of statements when it's ↵	Unknown	2012-09-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	going to be used (otherwise Nil is passed).