|
|
@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.
|
|
|
@2249
|
9 years |
campbell |
Tweak Cminor invariant to be slightly more readable/extendable.
|
|
|
@2232
|
9 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
@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 …
|
|
|
@1631
|
9 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
@1610
|
9 years |
sacerdot |
Ported to new lib.
|
|
|
@1608
|
9 years |
sacerdot |
Porting to new library still in progress.
|
|
|
@1605
|
9 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
@1599
|
9 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@1401
|
9 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
@1369
|
9 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
@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 …
|
|
|
@1139
|
9 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
@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 …
|
|
|
@758
|
10 years |
campbell |
Implement replacement of global var initialisation data by code in Cminor.
|