|
|
@2928
|
8 years |
tranquil |
some sketches about correctness proof
|
|
|
@2875
|
8 years |
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
|
@2852
|
8 years |
mckinna |
Interim commit to re-establish well-typedness after all the recent …
|
|
|
@2802
|
8 years |
sacerdot |
New file Clight_classified_system with the classified system for …
|
|
|
@2774
|
8 years |
sacerdot |
1. the compiler now outputs both the stack cost model and the max …
|
|
|
@2766
|
8 years |
mckinna |
pruned redundant dependency on Clight/Cexec?.ma
|
|
|
@2765
|
8 years |
sacerdot |
1. correctness.ma repaired
2. we used the OC_preclassified_system to …
|
|
|
@2722
|
8 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
@2623
|
8 years |
campbell |
Name change update.
|
|
|
@2596
|
8 years |
campbell |
Use a simpler stack cost map, and then specialise to each semantics.
|
|
|
@2513
|
8 years |
mckinna |
Minor tweaks. Simplified dependencies again.
|
|
|
@2506
|
8 years |
campbell |
Use common definition of measurable.
|
|
|
@2475
|
8 years |
campbell |
Get compiler.ma and correctness.ma checking again. Note that the …
|
|
|
@2412
|
8 years |
campbell |
Tidy up measurable definition a bit more.
|
|
|
@2399
|
8 years |
campbell |
Fill in some details about the statement of correctness.
|
|
|
@2325
|
8 years |
campbell |
Fill out some Clight bits and pieces in correctness.ma.
|
|
|
@2323
|
9 years |
campbell |
Some correctness proof comments.
|
|
|
@2322
|
9 years |
campbell |
Today's correctness groupthink.
|
|
|
@2320
|
9 years |
campbell |
Update compiler and correctness with labelling changes.
|
|
|
@2205
|
9 years |
campbell |
Get correctness.ma type checking again.
|
|
|
@2150
|
9 years |
campbell |
Add labelling result to the correctness file.
|
|
|
@2004
|
9 years |
campbell |
Minor edits from discussion.
|
|
|
@2003
|
9 years |
campbell |
Some discussion of correctness statements.
|
|
|
@2001
|
9 years |
campbell |
Get the compiler to output more.
|
|
|
@1996
|
9 years |
campbell |
Work on correctness from yesterday.
|