|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@1884
|
9 years |
campbell |
Syntax changes to fit Paolo's commit.
|
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1871
|
9 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 front-end 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 id-lookup-branch 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
|
10 years |
campbell |
Implement stack allocation for parameters whose address is taken.
|
|
|
|
@962
|
10 years |
campbell |
Casts should use source type's signedness, not the target's.
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@886
|
10 years |
campbell |
Put types into parameter and variable lists in Cminor.
Temporarily …
|
|
|
|
@882
|
10 years |
campbell |
Fix up fragile proofs for current version of matita.
|
|
|
|
@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 …
|
