|
|
|
@2182
|
9 years |
tranquil |
updated linearisation pass
|
|
|
|
@2155
|
9 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
|
@2111
|
9 years |
sacerdot |
Cleanup: lemmas/theorems/axioms moved to the right places.
|
|
|
|
@1949
|
9 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
|
@1928
|
9 years |
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
|
|
@1908
|
9 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1631
|
9 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
|
@1627
|
9 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1562
|
9 years |
mulligan |
new version of assembly, fixed conflict in positivemap.ma, changed …
|
|
|
|
@1535
|
9 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
|
@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 …
|
|
|
|
@1316
|
9 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1092
|
9 years |
campbell |
Some minor definitions for identifiers and lists.
|
|
|
|
@1077
|
10 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1072
|
10 years |
campbell |
Use not equals form of showing entry/exit labels.
|
|
|
|
@1070
|
10 years |
campbell |
Show that entry and exit labels are in the RTLabs graph.
|
|
|
|
@1068
|
10 years |
mulligan |
rtlabs translation complete subject to axioms
|
|
|
|
@1058
|
10 years |
campbell |
Evict CompCert? Maps interface in favour of BitVectorTries?.
|
|
|
|
@1057
|
10 years |
mulligan |
changes from today
|
|
|
|
@1056
|
10 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
|
@1055
|
10 years |
mulligan |
changes to how identifiers are generated
|
|
|
|
@1053
|
10 years |
mulligan |
changes
|
|
|
|
@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 …
|
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@779
|
10 years |
campbell |
Add merging of tries and identifier sets (based on Dominic's earlier …
|
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@753
|
10 years |
mulligan |
Work from today.
|
|
|
|
@738
|
10 years |
campbell |
Use lower case names for identifiers for consistency with CompCert? …
|
|
|
|
@737
|
10 years |
campbell |
Use more abstract identifiers in Clight / RTLabs.
|
|
|
|
@736
|
10 years |
campbell |
Extra type safety for identifiers.
|
