index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Chalice
Commit message (
Expand
)
Author
Age
*
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 permiss...
stefanheule
2012-10-01
*
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 usag...
stefanheule
2012-09-30
*
Chalice: Activate the test-case tests/permission-model/scaling.chalice that w...
stefanheule
2012-09-30
*
Chalice: Fix some problems related to the use of reals in Boogie.
stefanheule
2012-09-30
*
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
*
Chalice (Adapt to real support in Boogie): Axiomatization of division is no l...
stefanheule
2012-09-29
*
Chalice: Add a test-case for a recently fixed issue.
stefanheule
2012-09-28
*
Chalice: changed quantifier triggering to use #limited#trigger versions of fu...
Unknown
2012-09-27
*
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
|
*
added output for a test case
Unknown
2012-09-24
*
|
Chalice: Fix soundness issue about when it is sound to keep knowledge about p...
stefanheule
2012-09-21
*
|
Chalice: Alternative approach to frame known-folded locations; use quantifica...
stefanheule
2012-09-21
|
*
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
*
|
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
|
/
*
Chalice: Fix bug of computing the function height.
stefanheule
2012-09-19
*
Chalice: Use the framing function instead of the limited function in triggers...
stefanheule
2012-09-19
*
Chalice: Added a test case (general-tests/triggers) to test the trigger-gener...
Unknown
2012-09-18
*
Chalice: Updated linkedlist.chalice to include quantified specification, but ...
Unknown
2012-09-18
*
Chalice: Updated trigger generation to duplicate the entire quantifier in cas...
Unknown
2012-09-18
*
Chalice: modified trigger generation for quantifiers to include the use of ad...
Unknown
2012-09-18
*
Automatic Merge
Unknown
2012-09-17
|
\
*
|
Chalice: modified Tr() to only generate a real list of statements when it's g...
Unknown
2012-09-17
|
*
Chalice: Make the triggers for functions so it depends on all dependend predi...
stefanheule
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 spec...
stefanheule
2012-09-13
|
*
Chalice: Merge the two definitional axioms (was previously necessary to work ...
stefanheule
2012-09-13
|
*
Chalice: Update reference file for a test (a recent improvement makes the ver...
stefanheule
2012-09-13
|
*
Chalice: Remove CanAssumeFunctionDefs from framing axiom, as it is not needed...
stefanheule
2012-09-13
|
*
Chalice: Use the height of functions to increase the expressiveness of the po...
stefanheule
2012-09-13
|
*
Chalice: Remove debug output.
stefanheule
2012-09-13
|
*
Chalice: Compute the 'height' for functions (based on the condensation of the...
stefanheule
2012-09-13
|
/
*
Chalice: Test case for permissions in function postconditions.
stefanheule
2012-09-12
*
Chalice: Disallow accessibility predicates in function postconditions.
stefanheule
2012-09-12
*
Chalice: Switch to latest Scala release (there seems to be a compiler bug wit...
stefanheule
2012-09-12
*
Chalice: Also add time information for reg_test, reg_test_all and runalltests.
stefanheule
2012-09-11
[next]