summaryrefslogtreecommitdiff
path: root/Chalice/examples/iterator2.chalice
Commit message (Collapse)AuthorAge
* Chalice:Gravatar kyessenov2010-08-02
| | | | | | | * change syntax for range: [a..b] instead of [a:b] * add multi-triggers to Boogie bindings * fix unsoundness in frame axiom for functions -- whenever acc(s[*].f,...) is detected in pre-condition, a different encoding to Boogie is applied * add limited functions to translator (disabled since Resolver is not ready yet)
* Chalice: added "exists" quantifier; changed surface syntax for quantifier ↵Gravatar kyessenov2010-07-19
| | | | expressions
* Initial set of files.Gravatar mikebarnett2009-07-15