|
|
|
@2737
|
8 years |
garnier |
Commit of current proof state for Clight to Cminor translation.
|
|
|
|
@2734
|
8 years |
mckinna |
yet another puzzling automation failure, in the repaired case:
"" …
|
|
|
|
@2722
|
8 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
|
@2706
|
8 years |
mckinna |
repaired contentious broken automation
at end of subgoal 9 of case (* …
|
|
|
|
@2701
|
8 years |
sacerdot |
Automation failure fixed by replacing with hand made proof.
|
|
|
|
@2699
|
8 years |
mckinna |
simplified dependencies somewhat
|
|
|
|
@2698
|
8 years |
mckinna |
simplified dependencies
|
|
|
|
@2692
|
8 years |
garnier |
Add some more constraints in clight_cminor_data.
|
|
|
|
@2686
|
8 years |
mckinna |
two minor modifications to assist disambiguation of "lookup"
file …
|
|
|
|
@2682
|
8 years |
campbell |
Don't apply inv in after_n_steps to last state.
|
|
|
|
@2680
|
8 years |
mckinna |
proofs which previously succeeded fail, thanks to fold on positive_map …
|
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2668
|
8 years |
campbell |
Intermediate measurable proof check-in before I change its traces again.
|
|
|
|
@2667
|
8 years |
garnier |
Clight to Cminor, statements: some cases down. Subset of the …
|
|
|
|
@2654
|
8 years |
garnier |
Memory injections in a coherent state.
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2619
|
8 years |
campbell |
Update some test cases.
|
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2600
|
8 years |
garnier |
Memory injections are now only defined relatively to block ids, not …
|
|
|
|
@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.
|
|
|
|
@2594
|
8 years |
garnier |
Some fixes in memory injections, and some holes filled.
|
|
|
|
@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.
|
|
|
|
@2576
|
8 years |
campbell |
Add conditional test case that also uses switch removal.
|
|
|
|
@2574
|
8 years |
campbell |
Update labelling simulation proofs due to some changes elsewhere.
|
|
|
|
@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.
|
|
|
|
@2560
|
8 years |
garnier |
Fix in trace gen for CL
|
|
|
|
@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
|
|
|
|
@2535
|
8 years |
campbell |
Add the trivial C program with check that there's a measurable subtrace.
|
|
|
|
@2533
|
8 years |
campbell |
Some fall out from removing floats.
|
|
|
|
@2527
|
8 years |
garnier |
Progress on CL to CM.
|
|
|
|
@2510
|
8 years |
garnier |
Some progress on the Cl -> Cm front
|
|
|
|
@2505
|
8 years |
mckinna |
Cleaned up compiler.ma; some refactoring/additional code needed in …
|
|
|
|
@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.
|
|
|
|
@2488
|
8 years |
garnier |
glitch fixed
|
|
|
|
@2487
|
8 years |
campbell |
Set up "after_n_steps" to enforce an invariant on states.
|
|
|
|
@2483
|
8 years |
garnier |
Memory injections for Clight to Cminor, partially axiomatized.
|
|
|
|
@2471
|
8 years |
campbell |
Tame global environments a little.
|
|
|
|
@2469
|
8 years |
campbell |
Fix up opaque type errors from recent changes.
|
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
|
@2466
|
8 years |
campbell |
Show how global environments in clight to cminor pass match up.
|
|
|
|
@2465
|
8 years |
campbell |
Remove obsolete comment (runtime functions should be implemented later …
|
|
|
|
@2460
|
8 years |
campbell |
Rest of variable characterisation.
|
|
|
|
@2458
|
8 years |
campbell |
Clight to Cminor allocates stack variables to disjoint regions within …
|
|
|
|
@2450
|
8 years |
garnier |
Minor typo
|
|
|
|
@2449
|
8 years |
garnier |
Documentation added.
|
|
|
|
@2448
|
8 years |
garnier |
Comitting current state of switch removal.
|
|
|
|
@2441
|
8 years |
garnier |
Moved general stuff on memories from switchRemoval to MemProperties?, …
|
|
|
|
@2438
|
8 years |
garnier |
Sync of the w.i.p. for switch removal.
|
|
|
|
@2433
|
8 years |
campbell |
Tidy up Clight pointer comparison.
|
|
|
|
@2429
|
8 years |
garnier |
Restrict semantics of pointer comparison to what CompCert? does - i.e. …
|
|
|
|
@2428
|
8 years |
campbell |
Tighten requirements on switch statements in Clight to only give …
|
|
|
|
@2407
|
8 years |
campbell |
Sigh, continue in for loops was broken too.
|
|
|
|
@2399
|
8 years |
campbell |
Fill in some details about the statement of correctness.
|
|
|
|
@2395
|
8 years |
campbell |
Proper handling of comparison of pointers off-the-end of an object.
We …
|
|
|
|
@2393
|
8 years |
campbell |
A pointer comparison test case that illustrates a bug.
|
|
|
|
@2392
|
8 years |
campbell |
Labelling translations of && and || need a lot of cost labelling to …
|
|
|
|
@2391
|
8 years |
campbell |
Revert "Put the post-loop cost label into the Clight while statement …
|
|
|
|
@2389
|
8 years |
campbell |
Fix dowhile statements, and carefully arrange the translation so that …
|
|
|
|
@2388
|
8 years |
campbell |
Example of each type of control flow statement, plus minor fix to …
|
|
|
|
@2387
|
8 years |
garnier |
Revamped memory extensions, proved stuff on freeing blocks and on …
|
|
|
|
@2386
|
8 years |
garnier |
Implementation of constructive finite sets based on lists. Various …
|
|
|
|
@2385
|
8 years |
campbell |
Minor housekeeping.
|
|
|
|
@2384
|
8 years |
campbell |
Move Matita pretty printers into place.
|
|
|
|
@2353
|
8 years |
campbell |
Put the post-loop cost label into the Clight while statement to get …
|
|
|
|
@2338
|
8 years |
campbell |
Use much nicer definition for making several steps in the labelling …
|
|
|
|
@2332
|
8 years |
garnier |
Some progress on switch removal. Small fix in the definition of free, …
|
|
|
|
@2328
|
8 years |
campbell |
Cut down the notion of a Clight labelled state to those where we pick …
|
|
|
|
@2326
|
8 years |
campbell |
More accurate notion of labelled states in Clight.
|
|
|
|
@2325
|
8 years |
campbell |
Fill out some Clight bits and pieces in correctness.ma.
|
|
|
|
@2319
|
8 years |
campbell |
Generate per-program cost labels rather than per-function ones, and …
|
|
|
|
@2312
|
8 years |
garnier |
Memory injections, to be revised
|
|
|
|
@2304
|
8 years |
garnier |
Strengthened proof of associativity of bitvector addition. Some more …
|
|
|
|
@2302
|
8 years |
garnier |
Finally proved associativity of addition on bitvectors. Rejoice.
|
|
|
|
@2298
|
8 years |
garnier |
WIP: converting switch removal from Z to bitvectors. Does not compile, …
|
|
|
|
@2271
|
8 years |
garnier |
Proof of correction for the semantics of expressions under memory …
|
|
|
|
@2263
|
8 years |
garnier |
Finished proving semantics preservation under memory injections for …
|
|
|
|
@2255
|
8 years |
garnier |
Had to modify the definition of memory injections to prove that …
|
|
|
|
@2253
|
8 years |
campbell |
Cminor to RTLabs is now a total function.
|
|
|
|
@2252
|
8 years |
campbell |
Use the return statement invariant. Restructure the invariants for …
|
|
|
|
@2251
|
8 years |
campbell |
Add new invariant to Cminor that return typs should be respected.
|
|
|
|
@2250
|
8 years |
campbell |
Tidy up Clight to Cminor pass a bit.
|
|
|
|
@2249
|
8 years |
campbell |
Tweak Cminor invariant to be slightly more readable/extendable.
|
|
|
|
@2234
|
8 years |
garnier |
Progress on proving semantics preservation under memory injections.
|
|
|
|
@2232
|
8 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
|
@2231
|
8 years |
garnier |
Various tiny lemmas used in at least two files in the fornt-end.
|
|
|
|
@2227
|
8 years |
garnier |
* New version of the switch removal algorithm, described at the top of …
|
|
|
|
@2219
|
8 years |
campbell |
Speed up cast simplification proof checking a bit.
|
|
|
|
@2203
|
8 years |
campbell |
A general result about simulations of executions.
|
|
|
|
@2202
|
8 years |
campbell |
Start defining equivalent executions.
|
|
|
|
