|
|
|
@3178
|
8 years |
campbell |
Some progress on Callstate steps in Clight to Cminor.
Note that some …
|
|
|
|
@3170
|
8 years |
mckinna |
removed redundant dependencies
|
|
|
|
@3165
|
8 years |
campbell |
A little bit of progress on Callstate case.
|
|
|
|
@3155
|
8 years |
campbell |
Now have proof that the initial states are in simulation for clight to …
|
|
|
|
@3055
|
8 years |
campbell |
Start getting partial Clight to Cminor proof in shape for …
|
|
|
|
@3054
|
8 years |
campbell |
Put missing typ check in; adjust proof because I did it a little …
|
|
|
|
@3036
|
8 years |
garnier |
Fixing some problems, progress, etc
|
|
|
|
@2857
|
8 years |
garnier |
CL to CM: some invariants strengthened.
|
|
|
|
@2850
|
8 years |
garnier |
Progress on CL to CM. Some more cases closed modulo some critical …
|
|
|
|
@2838
|
8 years |
garnier |
Closing some more cases
|
|
|
|
@2825
|
8 years |
garnier |
Progress, Clight to Cminor
|
|
|
|
@2822
|
8 years |
garnier |
A consitent proof state for Clight to Cminor, with some progress (and …
|
|
|
|
@2737
|
8 years |
garnier |
Commit of current proof state for Clight to Cminor translation.
|
|
|
|
@2667
|
8 years |
garnier |
Clight to Cminor, statements: some cases down. Subset of the …
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2598
|
8 years |
garnier |
Tentative, partial draft for the definition of Clight-Cminor …
|
|
|
|
@2597
|
8 years |
campbell |
Some work in progress on measurable subtrace preservation.
|
|
|
|
@2591
|
8 years |
garnier |
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
|
|
|
|
@2588
|
8 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
|
@2582
|
8 years |
garnier |
Some progress on CL to CM.
|
|
|
|
@2578
|
8 years |
garnier |
Progress on CL to CM, fixed some stuff in memory injections.
|
|
|
|
@2572
|
8 years |
garnier |
Progress on toCminorCorrectness.
|
|
|
|
@2569
|
8 years |
campbell |
Fix Clight semantics for ptr + char. (Compiler works anyway.)
|
|
|
|
@2568
|
8 years |
campbell |
Relax some Clight type checks to Cminor type checks to avoid …
|
|
|
|
@2565
|
8 years |
garnier |
Cl to Cm progress.
|
|
|
|
@2554
|
8 years |
garnier |
Proof of expression translation correctness "mostly" done for CL to …
|
|
|
|
@2545
|
8 years |
garnier |
Comitting current progress of CL to CM
|
|
|
|
@2527
|
8 years |
garnier |
Progress on CL to CM.
|
|
|
|
@2510
|
8 years |
garnier |
Some progress on the Cl -> Cm front
|
|
|
|
@2500
|
8 years |
garnier |
Continuing work on simulation in Clight/Cminor?
|
|
|
|
@2496
|
8 years |
garnier |
Some tentative work on the simulation proof for expressions, in order …
|
|
|
|
@2489
|
8 years |
campbell |
Conjecture some Clight/Cminor? simulation results.
|
|
|
|
@2471
|
8 years |
campbell |
Tame global environments a little.
|
|
|
|
@2466
|
8 years |
campbell |
Show how global environments in clight to cminor pass match up.
|
|
|
|
@2460
|
8 years |
campbell |
Rest of variable characterisation.
|
|
|
|
@2458
|
8 years |
campbell |
Clight to Cminor allocates stack variables to disjoint regions within …
|
