

@3054

7 years 
campbell 
Put missing typ check in; adjust proof because I did it a little …



@2953

7 years 
campbell 
Fix silly label handling bug I realised was there during my talk…



@2877

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



@2822

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



@2686

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



@2645

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



@2601

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



@2588

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



@2582

7 years 
garnier 
Some progress on CL to CM.



@2572

7 years 
garnier 
Progress on toCminorCorrectness.



@2568

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



@2565

7 years 
garnier 
Cl to Cm progress.



@2554

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



@2533

7 years 
campbell 
Some fall out from removing floats.



@2510

7 years 
garnier 
Some progress on the Cl > Cm front



@2496

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



@2469

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



@2468

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



@2465

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



@2407

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



@2391

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



@2389

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



@2353

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



@2252

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



@2251

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



@2250

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



@2249

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



@2232

7 years 
campbell 
Remove unused block structure in Cminor.



@2176

7 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@1884

8 years 
campbell 
Syntax changes to fit Paolo's commit.



@1878

8 years 
campbell 
Enforce typing of constants in frontend, plus binops for RTLabs.



@1872

8 years 
campbell 
Make binary operations in Cminor/RTLabs properly typed.
A few extra …



@1871

8 years 
campbell 
Change Clight to Cminor compilation to use gotos rather than loops, …



@1631

8 years 
campbell 
Use fact that type environments in Cminor have distinct variables to …



@1630

8 years 
campbell 
Remainder of freshness in Clight to Cminor pass.



@1629

8 years 
campbell 
Sort out most of the fresh names stuff in Clight to Cminor.



@1627

8 years 
campbell 
Add some notions of freshness, and start using them for temporary …



@1626

8 years 
campbell 
Add extra type safety in front end. NB: critical freshness parts …



@1612

8 years 
sacerdot 
All library ported to new Matita lib (finally).



@1608

8 years 
sacerdot 
Porting to new library still in progress.



@1605

8 years 
sacerdot 
Porting to last standard library of Matita.



@1516

8 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

8 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1369

8 years 
campbell 
Put type information into frontend unary ops.
Slight change to …



@1351

8 years 
campbell 
Tidy up some loose ends from the invariants branch merge.



@1316

8 years 
campbell 
Merge in idlookupbranch to trunk.



@1224

8 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1207

8 years 
campbell 
Second part of fixing temporaries in Clight to Cminor stage.



@1206

8 years 
campbell 
First stage of fixing temporary generation in Clight/toCminor.ma.



@1194

8 years 
campbell 
Remove old, commented out code.



@1139

8 years 
campbell 
Shift init_data out of generic program record so that it only appears …



@1078

8 years 
campbell 
Implement stack allocation for parameters whose address is taken.



@962

8 years 
campbell 
Casts should use source type's signedness, not the target's.



@961

8 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@886

8 years 
campbell 
Put types into parameter and variable lists in Cminor.
Temporarily …



@882

8 years 
campbell 
Fix up fragile proofs for current version of matita.



@881

8 years 
campbell 
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.



@880

8 years 
campbell 
Add type information into Cminor.
As a result, the Clight to Cminor …



@816

8 years 
campbell 
Clight to Cminor compilation, modulo switch statements, temporary …
