

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



@1302

9 years 
sacerdot 
ERTL/semantics.ma ported to joint/SemanticUtils (in progress)



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



@1294

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



@1289

9 years 
sacerdot 
semantics ported to latest Joint version



@1284

9 years 
sacerdot 
Bugs fixed: fresh_label changes the label universe, but this was not …



@1283

9 years 
sacerdot 
Bad programming practice removed: change_label is no longer required …



@1282

9 years 
sacerdot 
Cosmetic change: names of joint statements/instructions shortened and …



@1281

9 years 
sacerdot 
Porting of all transformation to the joint syntax practically …



@1280

9 years 
sacerdot 
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …



@1275

9 years 
sacerdot 
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …



@1271

9 years 
mulligan 
finished, kind of



@1270

9 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1260

9 years 
mulligan 
commit for csc



@1255

9 years 
sacerdot 
Major mistake fixed: op1 and op2 were assuming the source and dest …



@1254

9 years 
sacerdot 
More progress towards porting of RTLtoERTL to joint syntax.



@1252

9 years 
sacerdot 
graph_params added to joint/Joint.ma, together with useful common …



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



@1245

9 years 
sacerdot 
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …



@1236

9 years 
sacerdot 
LTLToLin.ma completed (up to a couple of daemons used to provide dead …



@1233

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



@1228

9 years 
mulligan 
some more changes



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



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



@1171

9 years 
mulligan 
changes made on claudio's request: changed order of nesting in the …



@1169

9 years 
sacerdot 
JointRTLtoLIN moved to Joint



@1167

9 years 
mulligan 
…



@1166

9 years 
mulligan 
moved joint ltl lin files into their own directory. more changes to …
