|
|
|
@2041
|
9 years |
sacerdot |
Repaired: unified syntax for monads.
|
|
|
|
@1451
|
9 years |
sacerdot |
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …
|
|
|
|
@1415
|
9 years |
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
|
|
@1411
|
9 years |
sacerdot |
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
|
|
|
|
@1408
|
9 years |
sacerdot |
1. Added joint/BEGlobalenvs that is a modification of …
|
|
|
|
@1390
|
9 years |
sacerdot |
All fetch_result implementations have been factorized out, leaving …
|
|
|
|
@1389
|
9 years |
sacerdot |
One more axiom closed.
|
|
|
|
@1388
|
9 years |
sacerdot |
fetch_result implemented for ERTL. This required a different …
|
|
|
|
@1386
|
9 years |
sacerdot |
Structure of semantic parameters simplified.
|
|
|
|
@1385
|
9 years |
sacerdot |
1. fetch_result and pop_frame now takes the genv in input
2. …
|
|
|
|
@1384
|
9 years |
sacerdot |
* fetch_ra taken out of pop_frame again since it is used uniformly and …
|
|
|
|
@1381
|
9 years |
sacerdot |
Old commented out code removed.
|
|
|
|
@1377
|
9 years |
sacerdot |
pop_frame now incorporates the fetch_result (that made sense only for …
|
|
|
|
@1372
|
9 years |
sacerdot |
save_frame now takes the stacksize to allow RTL to allocate the stack frame
|
|
|
|
@1371
|
9 years |
sacerdot |
save_frame changed to accept also the formal/actual argument pairs, …
|
|
|
|
@1359
|
9 years |
sacerdot |
1. more work on the RTL semantics
2. changes to joint/semantics to …
|
|
|
|
@1329
|
9 years |
sacerdot |
1. Definition of addresses moved to BEMem
2. Basic functions on …
|
|
|
|
@1327
|
9 years |
sacerdot |
More progress in the implementation of the ERTL specific statements. …
|
|
|
|
@1324
|
9 years |
sacerdot |
The semantics of extended statements must also consider the label …
|
|
|
|
@1318
|
9 years |
sacerdot |
Frame management implemented.
|
|
|
|
@1313
|
9 years |
sacerdot |
(E)RTL semantics ported to new data type for save/pop frame (but not …
|
|
|
|
@1312
|
9 years |
sacerdot |
Type of frame operations (pop_frame/save_frame) generalized to take in …
|
|
|
|
@1303
|
9 years |
sacerdot |
1. LTL/semantics.ma added (work in progress)
2. init_locals fixed to …
|
|
|
|
@1302
|
9 years |
sacerdot |
ERTL/semantics.ma ported to joint/SemanticUtils (in progress)
|
|
|
|
@1221
|
9 years |
sacerdot |
Cleanup.
|
|
|
|
@1163
|
9 years |
mulligan |
even more streamlining and fixes to get things type checking
|
|
|
|
@1162
|
10 years |
mulligan |
changes committed to ertl semantics based on our new combined syntax …
|
|
|
|
@1161
|
10 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
|
@1156
|
10 years |
sacerdot |
ERTL semantics completed up to initialization and memory model.
|
|
|
|
@1151
|
10 years |
sacerdot |
Only new_/del_frame and framesize left.
|
|
|
|
@1150
|
10 years |
sacerdot |
Push/pop implemented.
|
|
|
|
@1148
|
10 years |
sacerdot |
Function call/return finished (up to retrieving parameters from the …
|
|
|
|
@1146
|
10 years |
sacerdot |
More progress: function call/return almost completed.
|
|
|
|
@1142
|
10 years |
sacerdot |
More progress.
|
|
|
|
@1140
|
10 years |
sacerdot |
More instructions implemented.
|
|
|
|
@1137
|
10 years |
sacerdot |
More progress.
|
|
|
|
@1130
|
10 years |
sacerdot |
File in progress (copied from RTL).
All instructions considered up to …
|
