

@3046

7 years 
campbell 
Main part of combined switch removal and labelling proof.



@3044

7 years 
campbell 
Start showing combination of switch removal and labelling is OK.
Fix …



@2734

7 years 
mckinna 
yet another puzzling automation failure, in the repaired case:
"" …



@2722

7 years 
campbell 
It's easier to keep the real function identifier in frontend …



@2706

7 years 
mckinna 
repaired contentious broken automation
at end of subgoal 9 of case (* …



@2701

7 years 
sacerdot 
Automation failure fixed by replacing with hand made proof.



@2699

7 years 
mckinna 
simplified dependencies somewhat



@2680

7 years 
mckinna 
proofs which previously succeeded fail, thanks to fold on positive_map …



@2677

7 years 
campbell 
Retain the pointer for the function called in frontend call states
so …



@2608

7 years 
garnier 
Regions are no more stored in blocks. block_region now tests the id, …



@2588

7 years 
garnier 
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …



@2510

7 years 
garnier 
Some progress on the Cl > Cm front



@2488

7 years 
garnier 
glitch fixed



@2487

7 years 
campbell 
Set up "after_n_steps" to enforce an invariant on states.



@2468

7 years 
garnier 
Floats are gone from the frontend. Some trace amount might remain in …



@2450

7 years 
garnier 
Minor typo



@2449

7 years 
garnier 
Documentation added.



@2448

7 years 
garnier 
Comitting current state of switch removal.



@2441

7 years 
garnier 
Moved general stuff on memories from switchRemoval to MemProperties?, …



@2438

7 years 
garnier 
Sync of the w.i.p. for switch removal.



@2391

7 years 
campbell 
Revert "Put the postloop cost label into the Clight while statement …



@2387

7 years 
garnier 
Revamped memory extensions, proved stuff on freeing blocks and on …



@2353

7 years 
campbell 
Put the postloop cost label into the Clight while statement to get …



@2332

7 years 
garnier 
Some progress on switch removal. Small fix in the definition of free, …



@2304

7 years 
garnier 
Strengthened proof of associativity of bitvector addition. Some more …



@2302

7 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

8 years 
garnier 
* New version of the switch removal algorithm, described at the top of …



@2076

8 years 
garnier 
First steps towards a simulation proof for switch removal.



@2016

8 years 
garnier 
Slight change in simplification strategy to better match the semantics



@1915

8 years 
garnier 
Correction of a typo in switchRemoval.



@1883

8 years 
campbell 
Ilias' switch removal code, plus a test.
