|
|
@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 …
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
@1986
|
9 years |
campbell |
Get rid of unused abstraction of Globalenvs.
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
@1680
|
9 years |
campbell |
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …
|
|
|
@1655
|
9 years |
campbell |
Update Cminor and RTLabs semantics to use new monad definitions.
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
@1605
|
9 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
@1603
|
9 years |
sacerdot |
More proofs ported to new lib.
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@1369
|
9 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
@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.
|
|
|
@1238
|
9 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
@1139
|
10 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 …
|
|
|
@886
|
10 years |
campbell |
Put types into parameter and variable lists in Cminor.
Temporarily …
|
|
|
@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 …
|
|
|
@879
|
10 years |
campbell |
Refine "AST" types to include size/signedness information.
|
|
|
@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 …
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
@760
|
10 years |
campbell |
Fix tailcall continuations in Cminor.
|
|
|
@751
|
10 years |
campbell |
Initial version of the Cminor syntax and semantics.
|