

@2786

9 years 
piccolo 
Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas



@2785

9 years 
piccolo 
Traces.ma repaired



@2783

9 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2696

9 years 
sacerdot 
I can't get this right... :(



@2695

9 years 
sacerdot 
Renamed again.



@2693

9 years 
sacerdot 
1. Stuff moved to correct places.
2. ERTLptr pass added



@2691

9 years 
sacerdot 
ERTLtoERTLptr* moved to the proper place



@2689

9 years 
tranquil 
* fixed passes up to linearisation



@2681

9 years 
tranquil 
* improvements to the graph translation function
* fixed passes up to LTL



@2674

9 years 
tranquil 
* another change in block definition
* RTLabs > RTL and ERTL > …



@2666

9 years 
piccolo 
bug fixed in blocks.ma



@2645

9 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2604

9 years 
piccolo 
ERTLtoERTLptr in place.



@2601

9 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2590

9 years 
piccolo 
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …



@2566

9 years 
piccolo 
ERTL to ERTLptr pass implemented up to a few things to be
left to the …



@2564

9 years 
piccolo 
ERTL fully repaired, useless part of return value of pop_ra
removed.



@2563

9 years 
piccolo 
Repairing ERTL: show stopper found.



@2490

9 years 
tranquil 
switched back to Byte immediate (instead of beval ones)
propagated …



@2443

9 years 
tranquil 
changed joint's stack pointer and internal stack



@2286

9 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2233

9 years 
tranquil 
* completed update of ERTL semantics
* some minor changes in joint …



@2217

9 years 
tranquil 
* collapsed step_params, unserialized_params, funct_params and …



@2214

9 years 
tranquil 
* changed order of parameters of joint_internal_function and genv in …



@2208

9 years 
tranquil 
* moving some code around
* changed immediates to hold beval in …



@2182

9 years 
tranquil 
updated linearisation pass



@2175

9 years 
tranquil 
corrected small bug



@2174

9 years 
tranquil 
* factored out script for (axiomatised) fixpoint computation
* ERTL → …



@2162

9 years 
tranquil 
* yet another correction to joint
* added functions adding prologues …



@2103

9 years 
campbell 
Make transform_*program take a more general transformation to make …



@2041

9 years 
sacerdot 
Repaired: unified syntax for monads.



@1995

9 years 
campbell 
Overall compiler definition; bits and pieces to
make everything happy(ish).



@1730

10 years 
sacerdot 
Minor changes while studying the proof.



@1729

10 years 
sacerdot 
Comment left from SVN merge removed.



@1601

10 years 
sacerdot 
Files ported to new version of the standard library.



@1515

10 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1463

10 years 
mulligan 
added erasure for lin



@1451

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



@1429

10 years 
sacerdot 
Useless and removed.



@1425

10 years 
mulligan 
changes to the fixpoint calculation in ertl



@1424

10 years 
sacerdot 
1. fold function over BitVectorTries? moved from ERTLToLTL to …



@1423

10 years 
sacerdot 
 spill no longer used
 BUG IN Interference: generating the destruct …



@1415

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



@1411

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



@1408

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



@1390

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



@1389

10 years 
sacerdot 
One more axiom closed.



@1388

10 years 
sacerdot 
fetch_result implemented for ERTL. This required a different …



@1386

10 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

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



@1384

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



@1381

10 years 
sacerdot 
Old commented out code removed.



@1377

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



@1372

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



@1371

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



@1359

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



@1352

10 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1329

10 years 
sacerdot 
1. Definition of addresses moved to BEMem
2. Basic functions on …



@1327

10 years 
sacerdot 
More progress in the implementation of the ERTL specific statements. …



@1324

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



@1318

10 years 
sacerdot 
Frame management implemented.



@1313

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



@1312

10 years 
sacerdot 
Type of frame operations (pop_frame/save_frame) generalized to take in …



@1303

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



@1302

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



@1282

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



@1281

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



@1280

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



@1275

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



@1274

10 years 
mulligan 
starting removing axioms from adts and giving them proper implementations



@1271

10 years 
mulligan 
finished, kind of



@1270

10 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1269

10 years 
sacerdot 
Useless include removed.



@1263

10 years 
mulligan 
changes



@1260

10 years 
mulligan 
commit for csc



@1256

10 years 
mulligan 
changes: added a mapi for graphs



@1254

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



@1253

10 years 
mulligan 
uses.ma finished



@1252

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



@1251

10 years 
mulligan 
changes to get things compiling again after yet another CSC rearrangement!



@1250

10 years 
sacerdot 
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …



@1249

10 years 
mulligan 
changes to get everything to typecheck again



@1248

10 years 
mulligan 
deleted files that do not compile in utilities, changed ertl.ma to use …



@1243

10 years 
mulligan 
small changes



@1242

10 years 
sacerdot 
Some cleanup.



@1241

10 years 
mulligan 
changes for claudio



@1232

10 years 
mulligan 
big changes: got what was implemented in the ertl to ltl pass type …



@1230

10 years 
mulligan 
more changes



@1229

10 years 
mulligan 
changes



@1228

10 years 
mulligan 
some more changes



@1227

10 years 
mulligan 
changes



@1223

10 years 
mulligan 
changes



@1221

10 years 
sacerdot 
Cleanup.



@1220

10 years 
sacerdot 
ERTL ported to the new joint syntax.



@1192

10 years 
mulligan 
some files that were missing / laying dormant on my computer



@1191

10 years 
mulligan 
ertl to ertl pass back where it was before the changes to joint



@1188

10 years 
mulligan 
removed stray lines from uses.ma so that it at least typechecks



@1187

10 years 
mulligan 
fixed build.ma



@1185

10 years 
mulligan 
ported liveness analysis to new code



@1183

10 years 
mulligan 
removed parameterised label types in the three lowest level languages


