|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1705
|
9 years |
campbell |
Checkpoint RTLabs labelling soundness work.
|
|
|
|
@1680
|
9 years |
campbell |
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …
|
|
|
|
@1675
|
9 years |
campbell |
Some work on sound labelled for RTLabs.
|
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
|
@1369
|
9 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
|
@1316
|
9 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1307
|
9 years |
mulligan |
adding translate_cst
|
|
|
|
@1224
|
9 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1147
|
9 years |
campbell |
Remove some obsolete commented out code, update a couple of comments.
|
|
|
|
@1139
|
9 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@1116
|
9 years |
sacerdot |
Some comments.
|
|
|
|
@1071
|
10 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
|
@1070
|
10 years |
campbell |
Show that entry and exit labels are in the RTLabs graph.
|
|
|
|
@1056
|
10 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
|
@1051
|
10 years |
mulligan |
removed superfluous addressing mode code from RTLabs/syntax.ma
|
|
|
|
@1046
|
10 years |
mulligan |
syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
|
|
|
|
@1045
|
10 years |
mulligan |
resolved conflict in rtlabs
|
|
|
|
@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 …
|
|
|
|
@878
|
10 years |
campbell |
Removal of manually inserted record projections.
|
|
|
|
@816
|
10 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@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
|
|
copied from src/RTLabs/RTLabs-syntax.ma:
|
|
|
|
@750
|
10 years |
campbell |
Track some of the changes to the prototype in RTLabs.
Just one …
|
