

@2877

9 years 
garnier 
Correction of a bug in my former bug correction.



@2857

9 years 
garnier 
CL to CM: some invariants strengthened.



@2850

9 years 
garnier 
Progress on CL to CM. Some more cases closed modulo some critical …



@2838

9 years 
garnier 
Closing some more cases



@2825

9 years 
garnier 
Progress, Clight to Cminor



@2822

9 years 
garnier 
A consitent proof state for Clight to Cminor, with some progress (and …



@2802

9 years 
sacerdot 
New file Clight_classified_system with the classified system for …



@2737

9 years 
garnier 
Commit of current proof state for Clight to Cminor translation.



@2734

9 years 
mckinna 
yet another puzzling automation failure, in the repaired case:
"" …



@2722

9 years 
campbell 
It's easier to keep the real function identifier in frontend …



@2706

9 years 
mckinna 
repaired contentious broken automation
at end of subgoal 9 of case (* …



@2701

9 years 
sacerdot 
Automation failure fixed by replacing with hand made proof.



@2699

9 years 
mckinna 
simplified dependencies somewhat



@2698

9 years 
mckinna 
simplified dependencies



@2692

9 years 
garnier 
Add some more constraints in clight_cminor_data.



@2686

9 years 
mckinna 
two minor modifications to assist disambiguation of "lookup"
file …



@2682

9 years 
campbell 
Don't apply inv in after_n_steps to last state.



@2680

9 years 
mckinna 
proofs which previously succeeded fail, thanks to fold on positive_map …



@2677

9 years 
campbell 
Retain the pointer for the function called in frontend call states
so …



@2668

9 years 
campbell 
Intermediate measurable proof checkin before I change its traces again.



@2667

9 years 
garnier 
Clight to Cminor, statements: some cases down. Subset of the …



@2654

9 years 
garnier 
Memory injections in a coherent state.



@2645

9 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2619

9 years 
campbell 
Update some test cases.



@2608

9 years 
garnier 
Regions are no more stored in blocks. block_region now tests the id, …



@2601

9 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2600

9 years 
garnier 
Memory injections are now only defined relatively to block ids, not …



@2598

9 years 
garnier 
Tentative, partial draft for the definition of ClightCminor …



@2597

9 years 
campbell 
Some work in progress on measurable subtrace preservation.



@2594

9 years 
garnier 
Some fixes in memory injections, and some holes filled.



@2591

9 years 
garnier 
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …



@2588

9 years 
garnier 
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …



@2582

9 years 
garnier 
Some progress on CL to CM.



@2578

9 years 
garnier 
Progress on CL to CM, fixed some stuff in memory injections.



@2576

9 years 
campbell 
Add conditional test case that also uses switch removal.



@2574

9 years 
campbell 
Update labelling simulation proofs due to some changes elsewhere.



@2572

9 years 
garnier 
Progress on toCminorCorrectness.



@2569

9 years 
campbell 
Fix Clight semantics for ptr + char. (Compiler works anyway.)



@2568

9 years 
campbell 
Relax some Clight type checks to Cminor type checks to avoid …



@2565

9 years 
garnier 
Cl to Cm progress.



@2560

9 years 
garnier 
Fix in trace gen for CL



@2554

9 years 
garnier 
Proof of expression translation correctness "mostly" done for CL to …



@2545

9 years 
garnier 
Comitting current progress of CL to CM



@2535

9 years 
campbell 
Add the trivial C program with check that there's a measurable subtrace.



@2533

9 years 
campbell 
Some fall out from removing floats.



@2527

9 years 
garnier 
Progress on CL to CM.



@2510

9 years 
garnier 
Some progress on the Cl > Cm front



@2505

9 years 
mckinna 
Cleaned up compiler.ma; some refactoring/additional code needed in …



@2500

9 years 
garnier 
Continuing work on simulation in Clight/Cminor?



@2496

9 years 
garnier 
Some tentative work on the simulation proof for expressions, in order …



@2489

9 years 
campbell 
Conjecture some Clight/Cminor? simulation results.



@2488

9 years 
garnier 
glitch fixed



@2487

9 years 
campbell 
Set up "after_n_steps" to enforce an invariant on states.



@2483

9 years 
garnier 
Memory injections for Clight to Cminor, partially axiomatized.



@2471

9 years 
campbell 
Tame global environments a little.



@2469

9 years 
campbell 
Fix up opaque type errors from recent changes.



@2468

9 years 
garnier 
Floats are gone from the frontend. Some trace amount might remain in …



@2466

9 years 
campbell 
Show how global environments in clight to cminor pass match up.



@2465

9 years 
campbell 
Remove obsolete comment (runtime functions should be implemented later …



@2460

9 years 
campbell 
Rest of variable characterisation.



@2458

9 years 
campbell 
Clight to Cminor allocates stack variables to disjoint regions within …



@2450

9 years 
garnier 
Minor typo



@2449

9 years 
garnier 
Documentation added.



@2448

9 years 
garnier 
Comitting current state of switch removal.



@2441

9 years 
garnier 
Moved general stuff on memories from switchRemoval to MemProperties?, …



@2438

9 years 
garnier 
Sync of the w.i.p. for switch removal.



@2433

9 years 
campbell 
Tidy up Clight pointer comparison.



@2429

9 years 
garnier 
Restrict semantics of pointer comparison to what CompCert? does  i.e. …



@2428

9 years 
campbell 
Tighten requirements on switch statements in Clight to only give …



@2407

9 years 
campbell 
Sigh, continue in for loops was broken too.



@2399

9 years 
campbell 
Fill in some details about the statement of correctness.



@2395

9 years 
campbell 
Proper handling of comparison of pointers offtheend of an object.
We …



@2393

9 years 
campbell 
A pointer comparison test case that illustrates a bug.



@2392

9 years 
campbell 
Labelling translations of && and  need a lot of cost labelling to …



@2391

9 years 
campbell 
Revert "Put the postloop cost label into the Clight while statement …



@2389

9 years 
campbell 
Fix dowhile statements, and carefully arrange the translation so that …



@2388

9 years 
campbell 
Example of each type of control flow statement, plus minor fix to …



@2387

9 years 
garnier 
Revamped memory extensions, proved stuff on freeing blocks and on …



@2386

9 years 
garnier 
Implementation of constructive finite sets based on lists. Various …



@2385

9 years 
campbell 
Minor housekeeping.



@2384

9 years 
campbell 
Move Matita pretty printers into place.



@2353

9 years 
campbell 
Put the postloop cost label into the Clight while statement to get …



@2338

9 years 
campbell 
Use much nicer definition for making several steps in the labelling …



@2332

9 years 
garnier 
Some progress on switch removal. Small fix in the definition of free, …



@2328

9 years 
campbell 
Cut down the notion of a Clight labelled state to those where we pick …



@2326

9 years 
campbell 
More accurate notion of labelled states in Clight.



@2325

9 years 
campbell 
Fill out some Clight bits and pieces in correctness.ma.



@2319

9 years 
campbell 
Generate perprogram cost labels rather than perfunction ones, and …



@2312

9 years 
garnier 
Memory injections, to be revised



@2304

9 years 
garnier 
Strengthened proof of associativity of bitvector addition. Some more …



@2302

9 years 
garnier 
Finally proved associativity of addition on bitvectors. Rejoice.



@2298

9 years 
garnier 
WIP: converting switch removal from Z to bitvectors. Does not compile, …



@2271

9 years 
garnier 
Proof of correction for the semantics of expressions under memory …



@2263

9 years 
garnier 
Finished proving semantics preservation under memory injections for …



@2255

9 years 
garnier 
Had to modify the definition of memory injections to prove that …



@2253

9 years 
campbell 
Cminor to RTLabs is now a total function.



@2252

9 years 
campbell 
Use the return statement invariant. Restructure the invariants for …



@2251

9 years 
campbell 
Add new invariant to Cminor that return typs should be respected.



@2250

9 years 
campbell 
Tidy up Clight to Cminor pass a bit.



@2249

9 years 
campbell 
Tweak Cminor invariant to be slightly more readable/extendable.


