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: Code cleanup.
stefanheule
2012-02-25
|
*
Chalice: Change the Chalice function triggering mechanism to use a function p...
stefanheule
2012-02-25
|
*
Chalice: Do not remove permission from the secondary mask during the exhale t...
stefanheule
2012-02-25
|
*
Chalice: Change the Boogie encoding of Chalice functions to only depend on th...
stefanheule
2012-02-25
|
*
Chalice: Correct axioms with new trigger mechanism (with trigger f we have f ...
stefanheule
2012-02-25
|
*
Chalice: Change trigger function to only take a single argument.
stefanheule
2012-02-25
|
*
Chalice: Add trigger to 'limited axiom' instead of the definining axiom.
stefanheule
2012-02-25
|
*
Chalice: use canread instead of canreadforsure in function axiom
stefanheule
2012-02-25
|
*
Chalice: add axiom relating different triggers.
stefanheule
2012-02-25
|
*
Chalice: partly solve problem with triggers and quantified variables
stefanheule
2012-02-25
|
*
Chalice: first try at triggers for functions
stefanheule
2012-02-25
|
*
Chalice: update reference output of AssocitationList (to remove bogus fail)
stefanheule
2012-02-25
|
*
Chalice: update reference output to new error messages.
stefanheule
2012-02-25
|
*
Chalice: add missing well-formedness assumption.
stefanheule
2012-02-25
|
*
Chalice: Backed out changeset: a0fdb50e36b44bc939eb44e940b90975ffeaa781
stefanheule
2012-02-25
|
*
Chalice: the secondary mask was not saved using CallSecMask at a fork
stefanheule
2012-02-25
|
*
Chalice: use correct mask and secmask in translation during exhale
stefanheule
2012-02-25
|
*
Chalice: missing well-formedness assumption
stefanheule
2012-02-25
|
*
Chalice: another invalid use of etran instead of this
stefanheule
2012-02-25
|
*
Chalice: using this instead of etran inside of the ExpressionTranslator itsel...
stefanheule
2012-02-25
|
*
Chalice: no havoc during unfolding expressions
stefanheule
2012-02-25
|
*
Chalice: remove assertion that we have enought permission when updating the s...
stefanheule
2012-02-25
|
*
Chalice: Remove assumption IsGoodMask when updating the secondary mask.
stefanheule
2012-02-25
|
*
Chalice: do not assume IsGoodMask(sm)
stefanheule
2012-02-25
|
*
Chalice: ordering of picking a new version and checking against
stefanheule
2012-02-25
|
*
Chalice: Change position where we record the version and receiver of a predic...
stefanheule
2012-02-25
|
*
Chalice: reset auxilary information for while loops
stefanheule
2012-02-25
|
*
Chalice: add conditional variables to auxilary information
stefanheule
2012-02-25
|
*
Chalice: do not havoc during unfold's exhale
stefanheule
2012-02-25
|
*
Chalice: Backed out changeset: 5724b933941338bebb239272f6c90da6f3415f08
stefanheule
2012-02-25
|
*
Chalice: change order of unfold treatment; first inhale predicate body, then ...
stefanheule
2012-02-25
|
*
Chalice: reset state of predicate information after definedness check
stefanheule
2012-02-25
|
*
Chalice: more to handle unfolding
stefanheule
2012-02-25
|
*
Chalice: start to handle unfolding
stefanheule
2012-02-25
|
*
Chalice: reset currentConditions in fpi.reset
stefanheule
2012-02-25
|
*
Chalice: Backed out changeset: ae8ad67b7ed3 (invalid attempt to account for u...
stefanheule
2012-02-25
|
*
Chalice: remove stack dump
stefanheule
2012-02-25
|
*
Chalice: change location of stack trace dump.
stefanheule
2012-02-25
|
*
Chalice: first try for unfolding
stefanheule
2012-02-25
|
*
Chalice: add assumption that receivers of nested predicates are different
stefanheule
2012-02-25
|
*
Chalice: the folded predicate should only be recorded when the exhale for the...
stefanheule
2012-02-25
|
*
Chalice: correctly introduce a temporary secondary mask
stefanheule
2012-02-25
|
*
Chalice: include an exhale mask again for exhale
stefanheule
2012-02-25
|
*
Chalice: better bound on recursion for predicates
stefanheule
2012-02-25
|
*
Chalice: only one if conditional, as we want if-elseif-elseif behaviour, and ...
stefanheule
2012-02-25
|
*
Chalice: do not use a exhaleheap when recursing
stefanheule
2012-02-25
|
*
Chalice: add code to update secondary mask based on the folded predicates
stefanheule
2012-02-25
|
*
Chalice: introduce BoogieExpr to allow boogie expressions in the Chalice AST
stefanheule
2012-02-25
|
*
Chalice: begging of a method UpdateSecMask that decrements (recursively) the ...
stefanheule
2012-02-25
|
*
Chalice: start using FoldedPredicatesInfo and change exhale to transfer permi...
stefanheule
2012-02-25
[prev]
[next]