

@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 …



@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 …



@1326

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



@1324

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



@1322

9 years 
sacerdot 
address => stack_address



@1320

9 years 
sacerdot 
Frame operations implemented.



@1313

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



@1303

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



@1301

9 years 
sacerdot 
Axioms regrouped according to their use.



@1300

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



@1299

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



@1298

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



@1295

9 years 
sacerdot 
More progress.



@1294

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



@1233

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



@1141

9 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 …
