

@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

8 years 
garnier 
Progress on toCminorCorrectness.



@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 …



@2533

8 years 
campbell 
Some fall out from removing floats.



@2510

8 years 
garnier 
Some progress on the Cl > Cm front



@2496

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



@2469

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



@2468

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



@2465

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



@2407

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



@2391

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



@2389

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



@2353

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



@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.



@2232

8 years 
campbell 
Remove unused block structure in Cminor.



@2176

8 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

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



@1630

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



@1629

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



@1627

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



@1626

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



@1612

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



@1608

9 years 
sacerdot 
Porting to new library still in progress.



@1605

9 years 
sacerdot 
Porting to last standard library of Matita.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1369

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



@1351

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



@1316

9 years 
campbell 
Merge in idlookupbranch to trunk.



@1224

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



@1207

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



@1206

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



@1194

9 years 
campbell 
Remove old, commented out code.



@1139

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



@1078

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



@962

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



@961

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



@886

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



@882

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



@881

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



@880

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



@816

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