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