source: src/Clight/toCminorCorrectnessExpr.ma

Revision Log Mode:


Legend:

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