|
|
|
@1387
|
9 years |
sacerdot |
Further simplification *params1 no longer used.
|
|
|
|
@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 …
|
|
|
|
@1383
|
9 years |
sacerdot |
Potential bug fixed and bug found: the way pointers and labels are put …
|
|
|
|
@1382
|
9 years |
sacerdot |
- succ_pc generalized to return a res (necessary for LIN semantics)
- …
|
|
|
|
@1377
|
9 years |
sacerdot |
pop_frame now incorporates the fetch_result (that made sense only for …
|
|
|
|
@1376
|
9 years |
sacerdot |
Stack deallocation for RTL implemented in pop_frame.
|
|
|
|
@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 …
|
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1329
|
9 years |
sacerdot |
1. Definition of addresses moved to BEMem
2. Basic functions on …
|
|
|
|
@1324
|
9 years |
sacerdot |
The semantics of extended statements must also consider the label …
|
|
|
|
@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 …
|
|
|
|
@1298
|
9 years |
sacerdot |
- fetch_statement now takes in input the globalenv
- fetch_statement …
|
|
|
|
@1294
|
9 years |
sacerdot |
RTL semantics: porting to joint semantics started.
|
|
|
|
@1289
|
9 years |
sacerdot |
semantics ported to latest Joint version
|
|
|
|
@1281
|
9 years |
sacerdot |
Porting of all transformation to the joint syntax practically …
|
|
|
|
@1250
|
9 years |
sacerdot |
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …
|
|
|
|
@1247
|
9 years |
sacerdot |
Code (almost) ported to latest joint/Joint.ma datatype.
I still need …
|
|
|
|
@1246
|
9 years |
sacerdot |
Yet another change to Joint.ma to accomodate all passes.
The concrete …
|
|
|
|
@1233
|
9 years |
sacerdot |
1) Ported to Brian's new dependent type for fullexec
2) Universe level …
|
|
|
|
@1220
|
9 years |
sacerdot |
ERTL ported to the new joint syntax.
|
|
|
|
@1217
|
9 years |
sacerdot |
Only one axiom left.
|
|
|
|
@1215
|
9 years |
sacerdot |
1) Added shifting directly on pointers
2) More temporary axioms closed.
|
|
|
|
@1214
|
9 years |
sacerdot |
res_to_opt function added to common/Errors and used in joint/semantics …
|
|
|
|
@1213
|
9 years |
sacerdot |
1) New values (joint/BEValues.ma) and memory model for the back-ends
…
|
|
|
|
@1186
|
9 years |
sacerdot |
Spurious code removed.
joint_fullexec implemented up to …
|
|
|
|
@1182
|
9 years |
mulligan |
changes to semantics: removing parameterised "next" element in joint …
|
|
|
|
@1177
|
9 years |
sacerdot |
Almost finished. Some functions still to be implemented, but I suspect …
|
|
|
|
@1176
|
9 years |
sacerdot |
…
|
|
|
|
@1174
|
9 years |
sacerdot |
Semantics of most instructions completed.
|
|
|
|
@1173
|
9 years |
sacerdot |
Unified semantics for ERTL/LTL/LIN (in progress).
I hope to include …
|
