Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
source:
src
/
Clight
/
toCminorCorrectness.ma
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2737
7 years
garnier
Commit of current proof state for Clight to Cminor translation.
(edit)
@2667
7 years
garnier
Clight to Cminor, statements: some cases down. Subset of the …
(edit)
@2601
7 years
sacerdot
Extraction to ocaml is now working, with a couple of bugs left. One …
(edit)
@2598
7 years
garnier
Tentative, partial draft for the definition of Clight-Cminor …
(edit)
@2597
7 years
campbell
Some work in progress on measurable subtrace preservation.
(edit)
@2591
7 years
garnier
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
(edit)
@2588
7 years
garnier
modified
Cexec/Csem?
semantics: . force andbool and orbool types to be …
(edit)
@2582
7 years
garnier
Some progress on CL to CM.
(edit)
@2578
7 years
garnier
Progress on CL to CM, fixed some stuff in memory injections.
(edit)
@2572
7 years
garnier
Progress on toCminorCorrectness.
(edit)
@2569
7 years
campbell
Fix Clight semantics for ptr + char. (Compiler works anyway.)
(edit)
@2568
7 years
campbell
Relax some Clight type checks to Cminor type checks to avoid …
(edit)
@2565
7 years
garnier
Cl to Cm progress.
(edit)
@2554
7 years
garnier
Proof of expression translation correctness "mostly" done for CL to …
(edit)
@2545
7 years
garnier
Comitting current progress of CL to CM
(edit)
@2527
7 years
garnier
Progress on CL to CM.
(edit)
@2510
7 years
garnier
Some progress on the Cl -> Cm front
(edit)
@2500
7 years
garnier
Continuing work on simulation in
Clight/Cminor?
(edit)
@2496
7 years
garnier
Some tentative work on the simulation proof for expressions, in order …
(edit)
@2489
8 years
campbell
Conjecture some
Clight/Cminor?
simulation results.
(edit)
@2471
8 years
campbell
Tame global environments a little.
(edit)
@2466
8 years
campbell
Show how global environments in clight to cminor pass match up.
(edit)
@2460
8 years
campbell
Rest of variable characterisation.
(add)
@2458
8 years
campbell
Clight to Cminor allocates stack variables to disjoint regions within …
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog