source: src/Clight/label.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3030   7 years campbell Break up front-end for correctness proof. Use let rec to prevent …
(edit) @3021   7 years campbell Replace clight_clock_after with a more sensible definition that uses …
(edit) @2588   7 years garnier modified Cexec/Csem? semantics: . force andbool and orbool types to be …
(edit) @2505   7 years mckinna Cleaned up compiler.ma; some refactoring/additional code needed in …
(edit) @2399   7 years campbell Fill in some details about the statement of correctness.
(edit) @2392   7 years campbell Labelling translations of && and || need a lot of cost labelling to …
(edit) @2391   7 years campbell Revert "Put the post-loop cost label into the Clight while statement …
(edit) @2353   7 years campbell Put the post-loop cost label into the Clight while statement to get …
(edit) @2319   7 years campbell Generate per-program cost labels rather than per-function ones, and …
(edit) @2103   7 years campbell Make transform_*program take a more general transformation to make …
(edit) @1888   8 years campbell Show that labelling of expressions works ... after fixing it to match …
(edit) @1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
(edit) @1224   8 years sacerdot Type of programs in common/AST made more dependent. In particular, the …
(edit) @1056   8 years campbell Switch to delayed identifier error scheme.
(edit) @961   8 years campbell Use precise bitvector sizes throughout the front end, rather than …
(add) @781   9 years campbell Implement labelling pass for Clight.
Note: See TracRevisionLog for help on using the revision log.