|
|
|
@2025
|
8 years |
campbell |
Silly typo and old comment.
|
|
|
|
@1999
|
8 years |
campbell |
Make back-end use the main global envs.
|
|
|
|
@1988
|
8 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1986
|
8 years |
campbell |
Get rid of unused abstraction of Globalenvs.
|
|
|
|
@1920
|
8 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
|
@1882
|
8 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1880
|
8 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
|
@1878
|
8 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1874
|
8 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1872
|
8 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1713
|
8 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
|
@1681
|
8 years |
campbell |
Checkpoint of stack preservation work in RTLabs.
|
|
|
|
@1680
|
8 years |
campbell |
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …
|
|
|
|
@1655
|
8 years |
campbell |
Update Cminor and RTLabs semantics to use new monad definitions.
|
|
|
|
@1601
|
8 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1583
|
8 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
|
@1559
|
8 years |
campbell |
Add a notion of flat traces with evidence for RTLabs.
|
|
|
|
@1535
|
8 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
|
@1369
|
8 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
|
@1238
|
8 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
|
@1139
|
8 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@1123
|
8 years |
sacerdot |
Added comment about missing alignment of data in memory.
|
|
|
|
@961
|
9 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@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 …
|
|
|
|
@879
|
9 years |
campbell |
Refine "AST" types to include size/signedness information.
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@762
|
9 years |
campbell |
Make naming of RTLabs files more uniform
|
|
copied from src/RTLabs/RTLabs-sem.ma:
|
|
|
|
@761
|
9 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
