|
|
|
@2699
|
8 years |
mckinna |
simplified dependencies somewhat
|
|
|
|
@2680
|
8 years |
mckinna |
proofs which previously succeeded fail, thanks to fold on positive_map …
|
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2588
|
8 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
|
@2510
|
8 years |
garnier |
Some progress on the Cl -> Cm front
|
|
|
|
@2488
|
8 years |
garnier |
glitch fixed
|
|
|
|
@2487
|
8 years |
campbell |
Set up "after_n_steps" to enforce an invariant on states.
|
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
|
@2450
|
8 years |
garnier |
Minor typo
|
|
|
|
@2449
|
8 years |
garnier |
Documentation added.
|
|
|
|
@2448
|
8 years |
garnier |
Comitting current state of switch removal.
|
|
|
|
@2441
|
8 years |
garnier |
Moved general stuff on memories from switchRemoval to MemProperties?, …
|
|
|
|
@2438
|
8 years |
garnier |
Sync of the w.i.p. for switch removal.
|
|
|
|
@2391
|
8 years |
campbell |
Revert "Put the post-loop cost label into the Clight while statement …
|
|
|
|
@2387
|
8 years |
garnier |
Revamped memory extensions, proved stuff on freeing blocks and on …
|
|
|
|
@2353
|
8 years |
campbell |
Put the post-loop cost label into the Clight while statement to get …
|
|
|
|
@2332
|
8 years |
garnier |
Some progress on switch removal. Small fix in the definition of free, …
|
|
|
|
@2304
|
8 years |
garnier |
Strengthened proof of associativity of bitvector addition. Some more …
|
|
|
|
@2302
|
8 years |
garnier |
Finally proved associativity of addition on bitvectors. Rejoice.
|
|
|
|
@2298
|
8 years |
garnier |
WIP: converting switch removal from Z to bitvectors. Does not compile, …
|
|
|
|
@2271
|
8 years |
garnier |
Proof of correction for the semantics of expressions under memory …
|
|
|
|
@2263
|
8 years |
garnier |
Finished proving semantics preservation under memory injections for …
|
|
|
|
@2255
|
8 years |
garnier |
Had to modify the definition of memory injections to prove that …
|
|
|
|
@2234
|
8 years |
garnier |
Progress on proving semantics preservation under memory injections.
|
|
|
|
@2227
|
9 years |
garnier |
* New version of the switch removal algorithm, described at the top of …
|
|
|
|
@2076
|
9 years |
garnier |
First steps towards a simulation proof for switch removal.
|
|
|
|
@2016
|
9 years |
garnier |
Slight change in simplification strategy to better match the semantics
|
|
|
|
@1915
|
9 years |
garnier |
Correction of a typo in switchRemoval.
|
|
|
|
@1883
|
9 years |
campbell |
Ilias' switch removal code, plus a test.
|
