|
|
|
@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
|
|
|
|
@1067
|
8 years |
mulligan |
more smaller changes
|
|
|
|
@1066
|
8 years |
mulligan |
changes from today
|
|
|
|
@1064
|
8 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
|
@1063
|
8 years |
mulligan |
changes from today
|
|
|
|
@1062
|
8 years |
mulligan |
separated jmeq and coercions from foldstuff.ma in order to fix the …
|
|
|
|
@1061
|
8 years |
mulligan |
more work, bug found, ridiculous map3 function with dep. types added
|
|
|
|
@1060
|
8 years |
mulligan |
work from this morning and yesterday
|
|
|
|
@1059
|
8 years |
mulligan |
work from today, bit of a mess at the moment
|
|
|
|
@1057
|
8 years |
mulligan |
changes from today
|
|
|
|
@1056
|
8 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
|
@1053
|
8 years |
mulligan |
changes
|
|
|
|
@1052
|
8 years |
mulligan |
removed offsets after reading cerco mailing list
|
|
|
|
@1051
|
8 years |
mulligan |
removed superfluous addressing mode code from RTLabs/syntax.ma
|
|
|
|
@1050
|
8 years |
mulligan |
adding dependent types to map datastructure to remove all option …
|
|
|
|
@1049
|
8 years |
mulligan |
more stuff added
|
|
|
|
@1047
|
8 years |
mulligan |
more work from today
|
|
|
|
@1046
|
8 years |
mulligan |
syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
|
|
|
|
@1045
|
8 years |
mulligan |
resolved conflict in rtlabs
|
|
|
|
@967
|
8 years |
campbell |
Update RTLabs pretty printer and examples.
|
|
|
|
@961
|
8 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@898
|
9 years |
campbell |
Update pretty printers and examples.
|
|
|
|
@888
|
9 years |
campbell |
Use simplified conditionals in RTLabs, following the prototype.
|
|
|
|
@887
|
9 years |
campbell |
Start bringing RTLabs into line with the prototype compiler:
- a …
|
|
|
|
@882
|
9 years |
campbell |
Fix up fragile proofs for current version of matita.
|
|
|
|
@879
|
9 years |
campbell |
Refine "AST" types to include size/signedness information.
|
|
|
|
@878
|
9 years |
campbell |
Removal of manually inserted record projections.
|
|
|
|
@816
|
9 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@799
|
9 years |
mulligan |
more changes.
|
|
|
|
@797
|
9 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@795
|
9 years |
mulligan |
Changes from this morning.
|
|
|
|
@793
|
9 years |
mulligan |
Work from today on rtlabs -> rtl pass.
|
|
|
|
@789
|
9 years |
mulligan |
More work on rtlabs -> rtl pass.
|
|
|
|
@775
|
9 years |
campbell |
A few useful definitions for when RTLabs programs fail.
|
|
|
|
@774
|
9 years |
campbell |
Separate out the different forms of addition and subtraction in the …
|
|
|
|
@766
|
9 years |
campbell |
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …
|
|
|
|
@765
|
9 years |
campbell |
Remove superfluous register in RTLabs return statements.
Also fix up …
|
|
|
|
@764
|
9 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
|
@762
|
9 years |
campbell |
Make naming of RTLabs files more uniform
|
|
|
|
@761
|
9 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
|
@751
|
9 years |
campbell |
Initial version of the Cminor syntax and semantics.
|
|
|
|
@750
|
9 years |
campbell |
Track some of the changes to the prototype in RTLabs.
Just one …
|
|
|
|
@747
|
9 years |
campbell |
Merge the two AST files together (although some definitions still need …
|
|
|
|
@744
|
9 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@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.
|
|
|
|
@731
|
9 years |
campbell |
Common definition for animation semantics, and factor out IO definitions.
|
|
|
|
@729
|
9 years |
campbell |
Pretty ugly printer for RTLabs programs.
|
|
|
|
@727
|
9 years |
campbell |
Enough fixes to let an RTLabs program run.
|
|
|
|
@726
|
9 years |
campbell |
Change identifiers to Words in Clight and RTLabs semantics.
|
|
|
|
@720
|
9 years |
campbell |
Sort out cost labels.
|
|
|
|
@718
|
9 years |
campbell |
Add an AST type (i.e., intermediate language type) for pointers.
|
|
|
|
@710
|
9 years |
campbell |
Start of way to import RTLabs from prototype compiler.
|
|
|
|
@702
|
9 years |
campbell |
Refine small-step executable semantics abstraction a little.
Some …
|
|
|
|
@695
|
9 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
copied from src/Clight/RTLabs:
|
|
|
|
@694
|
9 years |
campbell |
Start moving Clight into common directory.
|
