|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1457
|
9 years |
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
|
|
|
@1451
|
9 years |
sacerdot |
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …
|
|
|
|
@1430
|
9 years |
sacerdot |
Bug fixed: push/pop must work on the isp (now added).
Note: the sp is …
|
|
|
|
@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 …
|
|
|
|
@1395
|
9 years |
sacerdot |
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
|
|
|
|
@1390
|
9 years |
sacerdot |
All fetch_result implementations have been factorized out, leaving …
|
|
|
|
@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 …
|
