adding allocation range ghost state.
Merge request reports
Activity
added 5 commits
-
c1ee58be...fa57fa4d - 4 commits from branch
master - 364129b4 - [broken] adding allocation range ghost state.
-
c1ee58be...fa57fa4d - 4 commits from branch
added 1 commit
- 636a17d3 - [broken] adding allocation range ghost state.
added 1 commit
- be14009a - Fixing a first example + lemmas for adequacy.
added 1 commit
- d3bdd9c5 - More LocInBounds instances and proofs going through.
added 1 commit
- 14610af1 - Changed Optionable and add infrastructure to prove loc_in_bounds.
added 19 commits
-
edefcbb0...6e747174 - 8 commits from branch
master - f22ee9ff - [broken] adding allocation range ghost state.
- 67bb3298 - slight refactoring and cleanup
- e1486cd5 - Handling of loc_in_bounds in [array.v].
- a56572c5 - Handling of loc_in_bounds in [struct.v].
- 6d57047b - Fixing a first example + lemmas for adequacy.
- 33f9cbc1 - Partial fix for adequacy.
- 5ff9ab5b - More LocInBounds instances and proofs going through.
- 3a2203b6 - fix the admitted in adequacy
- a9d8371c - More LocInBounds instances.
- aaf11318 - Changed Optionable and add infrastructure to prove loc_in_bounds.
- 6b915f0c - fix adequacy
Toggle commit list-
edefcbb0...6e747174 - 8 commits from branch
mentioned in commit dc744bb2
Please register or sign in to reply