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
/
Resolver.scala
Commit message (
Collapse
)
Author
Age
*
Chalice: Disallow unfolding expressions in postconditions.
stefanheule
2012-10-01
|
*
Chalice: Fix bug in detecting permissions in postconditions.
stefanheule
2012-10-01
|
*
Chalice: Fix type-checker incompleteness.
stefanheule
2012-09-24
|
*
Chalice: Fix bug of computing the function height.
stefanheule
2012-09-19
|
*
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).
*
Chalice: Disallow accessibility predicates in function postconditions.
stefanheule
2012-09-12
|
*
Chalice: support for static functions. Functions declared "static" are ↵
Unknown
2012-09-05
|
|
|
|
axiomatised without a receiver. However, calls of such functions still syntactically require a receiver for now (which is ignored).
*
Chalice: Disallow 'waitlevel' in predicates.
stefanheule
2012-06-03
|
*
Chalice: Fix resolver bug, and add a test case for it.
stefanheule
2012-03-13
|
*
Chalice: Temporarily mark refinment extension as unsupported.
stefanheule
2012-03-09
|
*
Semi-automatic merge.
stefanheule
2012-02-25
|
\
*
|
Chalice: Code cleanup.
stefanheule
2012-02-25
|
|
*
|
Chalice: first try at triggers for functions
stefanheule
2012-02-25
|
|
*
|
Chalice: introduce BoogieExpr to allow boogie expressions in the Chalice AST
stefanheule
2012-02-25
|
|
|
*
Chalice: partial fixes to the broken refinement extension regression tests.
Kuat Yessenov
2011-12-21
|
|
|
*
Chalice: Disallow credit expressions in the specification of functions.
stefanheule
2011-08-12
|
/
*
Chalice: Chalice is now built using sbt (simple built tool).
stefanheule
2011-08-02