

@2176

8 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@1999

8 years 
campbell 
Make backend use the main global envs.



@1451

8 years 
sacerdot 
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …



@1415

8 years 
sacerdot 
1. hwreg_store/retrieve no longer returns a res (but it is still …



@1412

8 years 
sacerdot 
Tailcalls (via ids or pointers) to internal functions implemented. …



@1411

8 years 
sacerdot 
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …



@1408

8 years 
sacerdot 
1. Added joint/BEGlobalenvs that is a modification of …



@1396

8 years 
sacerdot 
Proof obligation closed.



@1390

8 years 
sacerdot 
All fetch_result implementations have been factorized out, leaving …



@1386

8 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

8 years 
sacerdot 
1. fetch_result and pop_frame now takes the genv in input
2. …



@1384

8 years 
sacerdot 
* fetch_ra taken out of pop_frame again since it is used uniformly and …



@1381

8 years 
sacerdot 
Old commented out code removed.



@1377

8 years 
sacerdot 
pop_frame now incorporates the fetch_result (that made sense only for …



@1376

8 years 
sacerdot 
Stack deallocation for RTL implemented in pop_frame.



@1372

8 years 
sacerdot 
save_frame now takes the stacksize to allow RTL to allocate the stack frame



@1371

8 years 
sacerdot 
save_frame changed to accept also the formal/actual argument pairs, …



@1359

8 years 
sacerdot 
1. more work on the RTL semantics
2. changes to joint/semantics to …



@1326

8 years 
sacerdot 
Code improved (now it uses the high level functions from …



@1324

8 years 
sacerdot 
The semantics of extended statements must also consider the label …



@1322

8 years 
sacerdot 
address => stack_address



@1320

8 years 
sacerdot 
Frame operations implemented.



@1313

8 years 
sacerdot 
(E)RTL semantics ported to new data type for save/pop frame (but not …



@1303

8 years 
sacerdot 
1. LTL/semantics.ma added (work in progress)
2. init_locals fixed to …



@1301

8 years 
sacerdot 
Axioms regrouped according to their use.



@1300

8 years 
sacerdot 
More (graph) axioms implemented. Look at the comments marked with XXX …



@1299

8 years 
sacerdot 
Functions from RTL/semantics.ma generalized to work on every graph …



@1298

8 years 
sacerdot 
 fetch_statement now takes in input the globalenv
 fetch_statement …



@1295

8 years 
sacerdot 
More progress.



@1294

8 years 
sacerdot 
RTL semantics: porting to joint semantics started.



@1233

8 years 
sacerdot 
1) Ported to Brian's new dependent type for fullexec
2) Universe level …



@1141

8 years 
sacerdot 
Comment (about a bug) added.



@1126

9 years 
sacerdot 
Semantics completed up to initial state creation.



@1122

9 years 
sacerdot 
Internal function call implemented too.



@1121

9 years 
sacerdot 
External function calls implemented (but look at the new comment on …



@1120

9 years 
sacerdot 
All operations implemented.



@1118

9 years 
sacerdot 
All derivatives of St_const implemented (up to axioms to match the two …



@1117

9 years 
sacerdot 
More operations implemented.



@1114

9 years 
sacerdot 
some more operations implemented



@1113

9 years 
sacerdot 
Semantics (interpreter) of RTL.
The file does not compile yet. I am …
