

@2468

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



@2439

7 years 
campbell 
Get a proper reverse mapping of function blocks to identifiers by …



@2319

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



@2286

7 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2176

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



@2105

7 years 
campbell 
Show some results about globalenvs and program transformations.



@2103

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



@1920

8 years 
campbell 
Most of the labelling simulation. Still need to sort out switch …



@1882

8 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1873

8 years 
campbell 
Fix up earlier frontend value conversion work.



@1872

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



@1640

8 years 
tranquil 
* finished fork of semantics.ma
* unification of Errors under the …



@1516

8 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1465

8 years 
sacerdot 
Dead code removed.



@1401

8 years 
ricciott 
Changes concerning the new behavior of destruct.



@1368

8 years 
sacerdot 
A bug in the clear tactic makes the previous (correct) commit wrong. …



@1367

8 years 
sacerdot 
Proof improvement, still somehow a bit slow.



@1353

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



@1350

8 years 
sacerdot 
Porting to latest destruct tactic.
Note: the tactics has a few …



@1268

8 years 
sacerdot 
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …



@1225

8 years 
campbell 
Missing ; in proof



@1224

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



@1213

8 years 
sacerdot 
1) New values (joint/BEValues.ma) and memory model for the backends
…



@1139

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



@1064

8 years 
mulligan 
changes from today, nearly complete rtlabs translation pass



@1060

8 years 
mulligan 
work from this morning and yesterday



@1059

8 years 
mulligan 
work from today, bit of a mess at the moment



@1057

8 years 
mulligan 
changes from today



@1052

8 years 
mulligan 
removed offsets after reading cerco mailing list



@1047

8 years 
mulligan 
more work from today



@1046

8 years 
mulligan 
syntax of rtlabs was wrong: cast not const. more added to rtlabs > …



@1045

8 years 
mulligan 
resolved conflict in rtlabs



@985

8 years 
sacerdot 
1) Major refactoring: proofs moved where they should be.
2) New …



@961

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



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



@879

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



@849

9 years 
sacerdot 
…



@795

9 years 
mulligan 
Changes from this morning.



@793

9 years 
mulligan 
Work from today on rtlabs > rtl pass.



@764

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



@757

9 years 
mulligan 
Lots more fixing to get both front and backends using same conventions …



@747

9 years 
campbell 
Merge the two AST files together (although some definitions still need …



@722

9 years 
mulligan 
Committing changes from today. Several files do not typecheck.



@714

9 years 
mulligan 
Work on translation from LTL to LIN.



@699

9 years 
mulligan 
More or less finished formalisation of LIN.



@698

9 years 
mulligan 
Commit with changes to files to get our files to typecheck.



@691

9 years 
mulligan 
More movement of files within the repository.


copied from Deliverables/D4.24.3/common/AST.ma:



@491

9 years 
mulligan 
Initial commit of (part)formalisation of LIN intermediate language.
