|
|
|
@2439
|
7 years |
campbell |
Get a proper reverse mapping of function blocks to identifiers by …
|
|
|
|
@2420
|
7 years |
campbell |
Tidy away generic results about folds on positive/identifier maps.
|
|
|
|
@2418
|
7 years |
campbell |
Add a checking function for the uniqueness of cost labels in RTLabs …
|
|
|
|
@2415
|
7 years |
campbell |
Add the ability to map blocks to symbols in preparation for stack space.
|
|
|
|
@2335
|
7 years |
campbell |
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …
|
|
|
|
@2314
|
7 years |
campbell |
Move generic definitions from recent commit to appropriate places.
|
|
|
|
@2307
|
7 years |
campbell |
Half the proofs for sound cost labelling check.
|
|
|
|
@2305
|
7 years |
campbell |
RTLabs cost spec checking function implemented (lacks proof, or much …
|
|
|
|
@2303
|
7 years |
campbell |
Some preliminary checking of cost labelling properties in RTLabs.
|
|
|
|
@2222
|
7 years |
sacerdot |
More robust to possible future changes to the "in match" semantics …
|
|
|
|
@2182
|
7 years |
tranquil |
updated linearisation pass
|
|
|
|
@2155
|
7 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
|
@2111
|
7 years |
sacerdot |
Cleanup: lemmas/theorems/axioms moved to the right places.
|
|
|
|
@1949
|
8 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
|
@1928
|
8 years |
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
|
|
@1908
|
8 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
|
@1882
|
8 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1635
|
8 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1631
|
8 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
|
@1627
|
8 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
|
@1601
|
8 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1562
|
8 years |
mulligan |
new version of assembly, fixed conflict in positivemap.ma, changed …
|
|
|
|
@1535
|
8 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
|
@1516
|
8 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1515
|
8 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1316
|
8 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1092
|
8 years |
campbell |
Some minor definitions for identifiers and lists.
|
|
|
|
@1077
|
8 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1072
|
8 years |
campbell |
Use not equals form of showing entry/exit labels.
|
|
|
|
@1070
|
8 years |
campbell |
Show that entry and exit labels are in the RTLabs graph.
|
|
|
|
@1068
|
8 years |
mulligan |
rtlabs translation complete subject to axioms
|
|
|
|
@1058
|
8 years |
campbell |
Evict CompCert? Maps interface in favour of BitVectorTries?.
|
|
|
|
@1057
|
8 years |
mulligan |
changes from today
|
|
|
|
@1056
|
8 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
|
@1055
|
8 years |
mulligan |
changes to how identifiers are generated
|
|
|
|
@1053
|
8 years |
mulligan |
changes
|
|
|
|
@816
|
9 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@797
|
9 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@782
|
9 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@779
|
9 years |
campbell |
Add merging of tries and identifier sets (based on Dominic's earlier …
|
|
|
|
@761
|
9 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
|
@757
|
9 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@753
|
9 years |
mulligan |
Work from today.
|
|
|
|
@738
|
9 years |
campbell |
Use lower case names for identifiers for consistency with CompCert? …
|
|
|
|
@737
|
9 years |
campbell |
Use more abstract identifiers in Clight / RTLabs.
|
|
|
|
@736
|
9 years |
campbell |
Extra type safety for identifiers.
|
