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: 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
*
Chalice: Update reference output for all test-cases due to recent change in t...
stefanheule
2012-09-11
*
Chalice: Adapt test scripts to not output timing information.
stefanheule
2012-09-11
*
Chalice: New command line parameter /time:<n> that allows to output timing in...
stefanheule
2012-09-11
*
Chalice: implemented automatic trigger-finding for quantifiers in user-suppli...
Unknown
2012-09-11
*
Chalice: added findFunctionAppsContaining(..) to Expression, which finds all ...
Unknown
2012-09-08
*
Chalice: implemented the final cases of the "inside" feature for predicates. ...
Unknown
2012-09-08
*
Chalice: implemented "inside" information for all cases which translate to st...
Unknown
2012-09-06
*
Chalice: added "inside" knowledge of predicate instance nesting to unfold sta...
Unknown
2012-09-06
*
Chalice: first part of implementation of tracking which predicate instances o...
Unknown
2012-09-06
*
Chalice: Merge
Unknown
2012-09-05
|
\
*
|
Chalice: support for static functions. Functions declared "static" are axioma...
Unknown
2012-09-05
|
*
Chalice: Remove accidental changes to chalice.bat.
stefanheule
2012-09-05
|
/
*
Chalice: adopted triggering/axioms used for "recursive" functions for all fun...
Unknown
2012-09-04
*
Chalice: reapplied changes from changeset
Unknown
2012-09-03
*
reapplied changes from changeset:
Unknown
2012-09-03
*
Chalice: added list segment example
Unknown
2012-09-03
*
Chalice: reremoved implementation of (unuses) UpdateSecMask, as was previousl...
Unknown
2012-09-03
*
Chalice: reapplied changes from changeset
Unknown
2012-09-03
*
Reapplied changes from previous update
Unknown
2012-09-03
*
Reverted Prelude.scala and Translator.scala to those from version 96adb1c351bd
Unknown
2012-09-03
*
New attempt, back to predicate masks that start off empty and gradually get p...
Unknown
2012-08-09
*
Intermediate version of implementation with two masks per predicate. #m_calc ...
Unknown
2012-08-09
*
Added variant of list reverse example (see tests/examples/list-reverse.chalic...
Unknown
2012-07-26
*
Automatic merge.
stefanheule
2012-07-26
|
\
*
|
Experimental version with weaker triggering for function definition axiom (sh...
Unknown
2012-07-25
*
|
Chalice: Fix bug in PrettyPrinter reported by danieljost (http://boogie.codep...
stefanheule
2012-06-20
|
*
Chalice:
stefanheule
2012-06-09
|
*
Chalice: add predicate instance to the "folded predicate list" at every inhal...
stefanheule
2012-06-08
|
*
Chalice: Correctly implement that on unfolds we assume that for all locations...
stefanheule
2012-06-08
|
*
Backed out changeset: d5b3896659ef
stefanheule
2012-06-08
[next]