diff options
| author |  kyessenov <unknown> | 2010-08-02 23:23:44 +0000 |
|---|---|---|
| committer | kyessenov <unknown> | 2010-08-02 23:23:44 +0000 |
| commit | 28ce0611b6365509f78549f36f505de5fa41ce32 (patch) | |
| tree | 804d9a2d618f9b477934575f44c656c1f5dfdd90 /Source/BoogieDriver | |
| parent | 09d97a79fe70f1c9b67ee5fac5afc41855ab208a (diff) | |
Chalice:
* 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)
Diffstat (limited to 'Source/BoogieDriver')
0 files changed, 0 insertions, 0 deletions