debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
\| \| \| * \| \|	Boogie: improved parser makefile	Unknown	2012-09-19
\| \| \| \| \| \|
\| \| \| \| \| *	Not reusing RelOp parser in CalcOp to avoid the conflict between !in and !	Nadia Polikarpova	2012-09-19
\| \| \| \| \| \|
\| \| \| \| \| *	Well-formedness check for calc lines	Nadia Polikarpova	2012-09-19
\| \| \| \| \| \|
\| \| \| \| \| *	Allow multiple calc/block statements in a hint. Removed the empty calc test ↵	Nadia Polikarpova	2012-09-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	from dafny2/Calculations, as it actually belongs in dafny0.
\| \| * \| \| \|	Chalice: Fix bug of computing the function height.	stefanheule	2012-09-19
\| \| \| \| \| \|
\| \| * \| \| \|	Merge	stefanheule	2012-09-19
\| \| \|\ \ \ \ \| \| \|/ / / / \| \|/\| \| \| \|
\| \| \| \| \| *	Made verification error message more explicit	Nadia Polikarpova	2012-09-19
\| \| \| \| \| \|
\| \| \| \| \| *	Allow empty calc statements	Nadia Polikarpova	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).
\| \| * \| \| \|	Merge	Nadia Polikarpova	2012-09-17
\| \| \|\ \ \ \ \| \| \|/ / / / \| \|/\| \| \| \|
\| \| * \| \| \|	Allow custom operators on a line	Nadia Polikarpova	2012-09-17
\| \| \| \| \| \|
\| * \| \| \| \|	During dualisation,	Unknown	2012-09-17
\| \| \|_\|_\|/ \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	x := y; now becomes x$1 := y$1; x$2 := y$2; instead of x$1, x$2 := y$1, y$2; This is to make way for further changes.
\| \| * \| \|	Allow several calculation operators (for the whole calculation)	Nadia Polikarpova	2012-09-16
\| \| \| \| \|
\| \| * \| \|	Allowing calc as hint (without braces)	Nadia Polikarpova	2012-09-16
\| \| \| \| \|
\| \| * \| \|	Renamed terms into lines (according to the proposal), fixed some contracts	Nadia Polikarpova	2012-09-16
\| \| \| \| \|
\| \| * \| \|	Added the new keyword (calc) to Util	Nadia Polikarpova	2012-09-16
\| \| \| \| \|
\| * \| \| \|	Added creation of source variable pre- and post- conditions.	Egor Kyshtymov	2012-09-16
\|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Changed style of error messages. Cleaned up error reporting code.
\| * \| \|	Error reporting for calculation steps	Nadia Polikarpova	2012-09-14
\| \| \| \|
\| * \| \|	Calc statements: Renamed Steps into Terms; introduced Steps (expressions ↵	Nadia Polikarpova	2012-09-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	t<i> op t<i + 1>), generated during resolution; first version of the translation
\| \| \| *	Chalice: Make the triggers for functions so it depends on all dependend ↵	stefanheule	2012-09-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	predicate triggers (avoiding matching loops).
\| * \| \|	Merge	Nadia Polikarpova	2012-09-14
\| \|\ \ \ \| \|/ / / \|/\| \| \|
\| * \| \|	Pretty-print calc statements	Nadia Polikarpova	2012-09-14
\| \| \| \|
\| \| \| *	Chalice: Extend one test case with more complete specification.	stefanheule	2012-09-13
\| \| \| \|
\| \| \| *	Chalice: Allow the postcondition axiom to be used when checking function ↵	stefanheule	2012-09-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	specifications in certain well-defined cases.
\| * \| \|	Resolve and clone calc statements; fixed a small grammar bug	Nadia Polikarpova	2012-09-13
\| \| \| \|
\| * \| \|	Added calc statement to the AST and the grammar (first attempt)	Nadia Polikarpova	2012-09-13
\| \| \| \|
\| \| \| *	Chalice: Merge the two definitional axioms (was previously necessary to work ↵	stefanheule	2012-09-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	around a z3 bug that has been fixed).
\| \| \| *	Chalice: Update reference file for a test (a recent improvement makes the ↵	stefanheule	2012-09-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	verifier more complete). Also remove an old comment from that test.
\| \| \| *	Chalice: Remove CanAssumeFunctionDefs from framing axiom, as it is not ↵	stefanheule	2012-09-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	needed for soundness.
\| \| \| *	Chalice: Use the height of functions to increase the expressiveness of the ↵	stefanheule	2012-09-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	postcondition axiom.
\| \| \| *	Chalice: Remove debug output.	stefanheule	2012-09-13
\| \| \| \|
\| \| \| *	Chalice: Compute the 'height' for functions (based on the condensation of ↵	stefanheule	2012-09-13
\| \| \|/ \| \| \| \| \| \| \| \| \|	the call graph).
* \| \|	Merge	Unknown	2012-09-12
\|\ \ \
* \| \| \|	Dafny: clone and merge attributes in refinements	Unknown	2012-09-12
\| \| \| \|
* \| \| \|	Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ↵	Unknown	2012-09-12
\| \|/ / \|/\| \| \| \| \| \| \| \|	and axiomatize [][..0] == [] == [][0..]
\| \| *	Chalice: Test case for permissions in function postconditions.	stefanheule	2012-09-12
\| \| \|
\| \| *	Chalice: Disallow accessibility predicates in function postconditions.	stefanheule	2012-09-12
\| \| \|
\| * \|	Updated test 'livevars' that would fail with Z3 4.1 (alternative error trace).	wuestholz	2012-09-12
\| \| \|