diff options
| author |  rustanleino <unknown> | 2009-09-14 20:43:33 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-09-14 20:43:33 +0000 |
| commit | 6fa676b575e1ba70c03b258420f29ad74b821b54 (patch) | |
| tree | 0ead8e60c4413e36e3f59d1dadf8f2ba37ee752c /Test | |
| parent | 23dcb26351cf28a59d6a413194dff2d8faf6c591 (diff) | |
Dafny:
* Added DeclType(f)==C axioms, which for each field f says which class declares it.
Boogie:
* Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
Diffstat (limited to 'Test')
0 files changed, 0 insertions, 0 deletions