

@3049

7 years 
campbell 
Globalenvs and initial states for cast simplification.



@3048

7 years 
campbell 
Improve dependency for cast simplification.



@2722

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



@2677

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



@2588

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



@2468

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



@2441

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



@2428

7 years 
campbell 
Tighten requirements on switch statements in Clight to only give …



@2391

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



@2353

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



@2219

7 years 
campbell 
Speed up cast simplification proof checking a bit.



@2184

7 years 
campbell 
Minor fix ups.



@2176

7 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2103

7 years 
campbell 
Make transform_*program take a more general transformation to make …



@2074

7 years 
garnier 
Prophylactic renaming of a relation



@2032

7 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@2030

7 years 
garnier 
Cast simplification was too conservative, now reasonably aggressive.



@2019

7 years 
campbell 
Split out special induction principle for Clight from soundness file. …



@2011

7 years 
garnier 
Minor cleanup.



@2009

7 years 
garnier 
Proof of simulation completed for singestep executions.



@1974

7 years 
garnier 
Progress on the cast simplification proof.



@1970

7 years 
garnier 
Workinprogress: correction proof for the cast removal on expressions.



@1873

8 years 
campbell 
Fix up earlier frontend value conversion work.



@1872

8 years 
campbell 
Make binary operations in Cminor/RTLabs properly typed.
A few extra …



@1224

8 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1198

8 years 
campbell 
Clight cast removal (NB: quite different from the prototype).
