index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Chalice
/
src
/
main
/
scala
/
Translator.scala
Commit message (
Expand
)
Author
Age
*
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
*
Chalice: index error
stefanheule
2012-02-25
*
Chalice: start to integrate FoldedPredicatesInfo into etran
stefanheule
2012-02-25
*
Chalice: helper method resetState and more refactorings.
stefanheule
2012-02-25
*
Chalice: more abstraction with a case class Globals.
stefanheule
2012-02-25
*
Chalice: first part of the refactoring for better handling of globals
stefanheule
2012-02-25
*
Chalice: add classes to track predicate information
stefanheule
2012-02-25
*
Chalice: correct axiom for limited functions (use 2nd mask)
stefanheule
2012-02-25
*
Chalice: do not use inhalefrom anymore for predicates (and thus remove inhale...
stefanheule
2012-02-25
*
Chalice: missing updates to SecMask
stefanheule
2012-02-25
*
Chalice: translate the precondition of functions (with permissions) correctly
stefanheule
2012-02-25
*
Chalice: do not use exhalehelper externally
stefanheule
2012-02-25
*
Chalice: rename exhale to exhalehelper and place one comment at a better place.
stefanheule
2012-02-25
*
Chalice: update the predicates version only when we lose complete access to t...
stefanheule
2012-02-25
*
Chalice: add SecMask to "wf" and as a parameter to the (Boogie) function for ...
stefanheule
2012-02-25
*
Chalice: (comment about translatePrecondition)
stefanheule
2012-02-25
*
Chalice: update definition of CanRead to account for the secondary permission...
stefanheule
2012-02-25
*
Chalice: assume IsGoodMask also for SecMask
stefanheule
2012-02-25
*
Chalice: introducing the secondary map (not using it yet)
stefanheule
2012-02-25
*
Chalice: guard the defining axiom for functions by their precondition
stefanheule
2012-02-25
*
Chalice: update framing axiom for preconditions with AccessSeq (only renaming...
stefanheule
2012-02-25
*
Chalice: change definition of combine and replace nostate by heapFragment and...
stefanheule
2012-02-25
*
Chalice: starting to implement versions for predicates (not finished yet)
stefanheule
2012-02-25
*
Chalice: move havocing to exhale
stefanheule
2012-02-25
*
Chalice: Chalice is now built using sbt (simple built tool).
stefanheule
2011-08-02