source: src/RTLabs @ 3031

Name Size Rev Age Author Last Change
../
test 1226   8 years campbell Adjust pretty printers for change in program records, try a test of each.
CostCheck.ma 27.4 KB 3022   7 years campbell Make a couple of tests monadic for easier inversion.
CostInj.ma 5.2 KB 3022   7 years campbell Make a couple of tests monadic for easier inversion.
CostMisc.ma 3.8 KB 2313   7 years campbell RTLabs cost checker correct.
CostSpec.ma 3.2 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
debug.ma 1.8 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
import.ma 10.1 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
MeasurableToStructured.ma 30.5 KB 3031   7 years campbell Tidy up RTLabs preclassified_system definitions.
RTLabs_abstract.ma 16.0 KB 3031   7 years campbell Tidy up RTLabs preclassified_system definitions.
RTLabs_classified_system.ma 1.2 KB 3031   7 years campbell Tidy up RTLabs preclassified_system definitions.
RTLabs_partial_traces.ma 101.0 KB 2923   7 years campbell Remove some leftovers.
RTLabs_semantics.ma 17.9 KB 2936   7 years campbell Disable initialisation code generation in Cminor, propogate init data …
RTLabs_syntax.ma 3.7 KB 2992   7 years campbell Add "only one return" invariant to RTLabs functions.
RTLabs_traces.ma 126.2 KB 2895   7 years campbell Match up function id from RTLabs Callstate with shadow stack, use in …
RTLabsToRTL.ma 38.6 KB 3004   7 years tranquil fixed a bug where when doing an asymetrical op, cast initialization …
RTLabsToRTLAxiom.ma 2.4 KB 2946   7 years tranquil main novelties: * there is an in-built stack_usage nat in joint …
Note: See TracBrowser for help on using the repository browser.