source: src/Clight/toCminorCorrectnessExpr.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2822   8 years garnier A consitent proof state for Clight to Cminor, with some progress (and …
(edit) @2692   8 years garnier Add some more constraints in clight_cminor_data.
(edit) @2667   8 years garnier Clight to Cminor, statements: some cases down. Subset of the …
(edit) @2608   8 years garnier Regions are no more stored in blocks. block_region now tests the id, …
(edit) @2601   8 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
(edit) @2600   8 years garnier Memory injections are now only defined relatively to block ids, not …
(add) @2591   8 years garnier Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
Note: See TracRevisionLog for help on using the revision log.