

@2936

9 years 
campbell 
Disable initialisation code generation in Cminor, propogate init data …



@2924

9 years 
campbell 
Make calls to a known identifier actually use a direct call.



@2601

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



@2390

9 years 
campbell 
Tidy up a corner case when generating RTLabs so that we generate
less …



@2335

9 years 
campbell 
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …



@2319

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



@2292

9 years 
campbell 
More RTLabs invariants.



@2289

9 years 
campbell 
Update alias



@2287

9 years 
campbell 
RTLabs typing for loads and stores.



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



@2232

9 years 
campbell 
Remove unused block structure in Cminor.



@2178

9 years 
campbell 
Shift some notation into utilities.



@2176

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



@2103

9 years 
campbell 
Make transform_*program take a more general transformation to make …



@2033

9 years 
sacerdot 
Daemon reverted.



@2032

9 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@1884

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



@1878

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



@1872

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



@1680

10 years 
campbell 
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …



@1631

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



@1626

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



@1611

10 years 
sacerdot 
All of Cminor now compiles with the latest lib of Matita.



@1605

10 years 
sacerdot 
Porting to last standard library of Matita.



@1603

10 years 
sacerdot 
More proofs ported to new lib.



@1599

10 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1521

10 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1516

10 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1464

10 years 
campbell 
Use unification hints to simplify the graph monotonicity proofs.



@1410

10 years 
campbell 
Remove a few old workarounds.



@1369

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



@1316

10 years 
campbell 
Merge in idlookupbranch to trunk.



@1224

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



@1139

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



@1072

10 years 
campbell 
Use not equals form of showing entry/exit labels.



@1070

10 years 
campbell 
Show that entry and exit labels are in the RTLabs graph.



@1056

10 years 
campbell 
Switch to delayed identifier error scheme.



@961

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



@888

10 years 
campbell 
Use simplified conditionals in RTLabs, following the prototype.



@887

10 years 
campbell 
Start bringing RTLabs into line with the prototype compiler:
 a …



@881

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



@880

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



@816

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



@797

10 years 
campbell 
Add error messages wherever the error monad is used.
Sticks to …



@790

10 years 
campbell 
A little tidying: get rid of requirement for jmeq in Mem.ma, remove …



@780

11 years 
campbell 
Properly update set of registers that are used for pointers in Cminor …



@772

11 years 
campbell 
Implement proper support for RTLabs addressing modes.



@771

11 years 
campbell 
Implement switch statements in Cminor > RTLabs phase



@767

11 years 
campbell 
Use variable shadowing as a poor man's state monad in cminor to rtlabs …



@766

11 years 
campbell 
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …



@764

11 years 
campbell 
Start Cminor to RTLabs phase.
Includes some syntax for matching …
