|
|
|
@2686
|
8 years |
mckinna |
two minor modifications to assist disambiguation of "lookup"
file …
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2588
|
8 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
|
@2582
|
8 years |
garnier |
Some progress on CL to CM.
|
|
|
|
@2572
|
8 years |
garnier |
Progress on toCminorCorrectness.
|
|
|
|
@2568
|
8 years |
campbell |
Relax some Clight type checks to Cminor type checks to avoid …
|
|
|
|
@2565
|
8 years |
garnier |
Cl to Cm progress.
|
|
|
|
@2554
|
8 years |
garnier |
Proof of expression translation correctness "mostly" done for CL to …
|
|
|
|
@2533
|
8 years |
campbell |
Some fall out from removing floats.
|
|
|
|
@2510
|
8 years |
garnier |
Some progress on the Cl -> Cm front
|
|
|
|
@2496
|
8 years |
garnier |
Some tentative work on the simulation proof for expressions, in order …
|
|
|
|
@2469
|
8 years |
campbell |
Fix up opaque type errors from recent changes.
|
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
|
@2465
|
8 years |
campbell |
Remove obsolete comment (runtime functions should be implemented later …
|
|
|
|
@2407
|
8 years |
campbell |
Sigh, continue in for loops was broken too.
|
|
|
|
@2391
|
8 years |
campbell |
Revert "Put the post-loop cost label into the Clight while statement …
|
|
|
|
@2389
|
8 years |
campbell |
Fix dowhile statements, and carefully arrange the translation so that …
|
|
|
|
@2353
|
8 years |
campbell |
Put the post-loop cost label into the Clight while statement to get …
|
|
|
|
@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.
|
|
|
|
@2250
|
9 years |
campbell |
Tidy up Clight to Cminor pass a bit.
|
|
|
|
@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 …
|
|
|
|
@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
|
10 years |
campbell |
Remove old, commented out code.
|
|
|
|
@1139
|
10 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 …
|
