

@2103

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



@2033

7 years 
sacerdot 
Daemon reverted.



@2032

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



@1993

7 years 
campbell 
Make frontend memory model only depend on the general definitions by …



@1988

7 years 
campbell 
Abstraction of the memory contents in the memory models is no longer …



@1986

7 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1884

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



@1878

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



@1874

7 years 
campbell 
First cut at using backend memory model throughout.
Note the …



@1872

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



@1713

8 years 
campbell 
Add a distinguished final state to the frontend languages to match up …



@1680

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



@1655

8 years 
campbell 
Update Cminor and RTLabs semantics to use new monad definitions.



@1633

8 years 
campbell 
Update Cminor pretty printer and examples.



@1631

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



@1626

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



@1611

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



@1610

8 years 
sacerdot 
Ported to new lib.



@1608

8 years 
sacerdot 
Porting to new library still in progress.



@1605

8 years 
sacerdot 
Porting to last standard library of Matita.



@1603

8 years 
sacerdot 
More proofs ported to new lib.



@1599

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



@1521

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



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



@1464

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



@1410

8 years 
campbell 
Remove a few old workarounds.



@1401

8 years 
ricciott 
Changes concerning the new behavior of destruct.



@1369

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



@1352

8 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1351

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



@1316

8 years 
campbell 
Merge in idlookupbranch to trunk.



@1238

8 years 
campbell 
Update Cminor and RTLabs to fit SmallstepExec? changes.



@1226

8 years 
campbell 
Adjust pretty printers for change in program records, try a test of each.



@1224

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



@1157

8 years 
campbell 
Update pretty printers and examples.



@1147

8 years 
campbell 
Remove some obsolete commented out code, update a couple of comments.



@1139

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



@1072

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



@1070

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



@1056

8 years 
campbell 
Switch to delayed identifier error scheme.



@966

8 years 
campbell 
Update Cminor pretty printer and some examples.



@961

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



@898

8 years 
campbell 
Update pretty printers and examples.



@888

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



@887

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



@886

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



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



@879

8 years 
campbell 
Refine "AST" types to include size/signedness information.



@878

8 years 
campbell 
Removal of manually inserted record projections.



@816

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



@797

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



@790

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



@780

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



@776

8 years 
campbell 
Fix up some minor null pointer issues in Clight.
Add corresponding …



@772

8 years 
campbell 
Implement proper support for RTLabs addressing modes.



@771

8 years 
campbell 
Implement switch statements in Cminor > RTLabs phase



@770

8 years 
campbell 
Clight and Cminor examples for switch statement.



@768

8 years 
campbell 
Make Cminor tests test translation to RTLabs.



@767

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



@766

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



@764

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



@761

8 years 
campbell 
Enforce the use of declared identifiers/registers in Cminor/RTLabs.



@760

8 years 
campbell 
Fix tailcall continuations in Cminor.



@758

8 years 
campbell 
Implement replacement of global var initialisation data by code in Cminor.



@751

8 years 
campbell 
Initial version of the Cminor syntax and semantics.
