|
|
|
@3037
|
8 years |
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
|
|
@2975
|
8 years |
tranquil |
* RTL premain fixed
* fixed bug in back end ops (subtracting to a …
|
|
|
|
@2955
|
8 years |
tranquil |
corrected stupid typo
|
|
|
|
@2952
|
8 years |
tranquil |
* corrected all back-end premains to not pass any arguments to the …
|
|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
|
@2783
|
8 years |
piccolo |
modified joint_closed_internal_function definition (added condition on …
|
|
|
|
@2681
|
8 years |
tranquil |
* improvements to the graph translation function
* fixed passes up to LTL
|
|
|
|
@2640
|
8 years |
tranquil |
updated RTL and RTLabs to RTL translation
|
|
|
|
@2490
|
8 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
|
@2286
|
8 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@1348
|
9 years |
sacerdot |
…
|
|
|
|
@1322
|
9 years |
sacerdot |
address => stack_address
|
|
|
|
@1280
|
9 years |
sacerdot |
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …
|
|
|
|
@1278
|
9 years |
sacerdot |
oppargs requires two more arguments. RTLtoERTL to be fixed since it …
|
|
|
|
@1275
|
9 years |
sacerdot |
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …
|
|
|
|
@1270
|
9 years |
sacerdot |
Making RTL syntax an instance of Joint.
|
|
|
|
@1239
|
9 years |
sacerdot |
RTLAbstoRTL ported to new datatypes.
Note: RTL syntax/semantics is …
|
|
|
|
@1115
|
9 years |
sacerdot |
Some comments.
|
|
|
|
@1106
|
9 years |
mulligan |
changes necessary to get RTLabs->RTL to compile
|
|
|
|
@1089
|
9 years |
mulligan |
more changes from earlier in the week
|
|
|
|
@1071
|
10 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
|
@1068
|
10 years |
mulligan |
rtlabs translation complete subject to axioms
|
|
|
|
@1066
|
10 years |
mulligan |
changes from today
|
|
|
|
@1064
|
10 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
|
@1061
|
10 years |
mulligan |
more work, bug found, ridiculous map3 function with dep. types added
|
|
|
|
@1060
|
10 years |
mulligan |
work from this morning and yesterday
|
|
|
|
@878
|
10 years |
campbell |
Removal of manually inserted record projections.
|
|
|
|
@783
|
10 years |
mulligan |
rtl to ertl pass complete (modulo some straightforward axioms that …
|
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@756
|
10 years |
mulligan |
Made a start on RTL. Renaming in ERTL and below to move closer to …
|
|
|
|
@754
|
10 years |
mulligan |
Syntax of RTL.
|
