

@3265

8 years 
tranquil 
added validate_pointer filter
in Interference added that intereference …



@3263

8 years 
tranquil 
moved callee saved saving and restoring to ERTL > LTL pass (untrusted …



@3262

8 years 
piccolo 
reverted status_simulation_utils



@3261

8 years 
piccolo 
reverted joint_semantics rtl_semantics and ltl_semantics



@3259

8 years 
piccolo 
changed ERTL semantics:
1) added manipulation of stack pointer …



@3257

8 years 
tranquil 
fixed uses in ERTL



@3255

8 years 
tranquil 
* dropped newframe and delframe (to be integrated in calls and returns …



@3253

8 years 
piccolo 
some proof obbligation closed of ERTL to LTL proof



@3252

8 years 
piccolo 
proof obbligation added on ERTL to LTL proof



@3217

8 years 
piccolo 
Correctness of ERTL to LTL in place



@3145

8 years 
tranquil 
* removed sigma types from traces of intensional events
* completed …



@3096

8 years 
tranquil 
preliminary work on closing correctness.ma



@3072

8 years 
tranquil 
corrected a bug (translate_store was wrong)



@3037

8 years 
tranquil 
* ADDRESS joint instruction now has also an offset
* corrected call to …



@3018

8 years 
sacerdot 
1) some files repaired
2) all stuff related to the aborted pass …



@3014

8 years 
tranquil 
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …



@2991

8 years 
piccolo 
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …



@2952

8 years 
tranquil 
* corrected all backend premains to not pass any arguments to the …



@2946

8 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2943

8 years 
sacerdot 
Mauro, I have put a daemon in place of the proof obligation that used …



@2942

8 years 
sacerdot 
Many changes:
1. Coloured graphs are now specified in terms of …



@2940

8 years 
sacerdot 
1. StatusSimulationHelper? changed to allow to use status_rel that …



@2898

8 years 
piccolo 
1) simplification of cond and seq case for StatusSimulationHelper? …



@2891

8 years 
piccolo 
added precondition on seq statement and tested correct in the …



@2883

8 years 
piccolo 
partial commit



@2868

8 years 
sacerdot 
Pretty printing of ERTL and ERTLptr code.



@2845

8 years 
piccolo 
ERTLptr to LTL correctness proof started



@2843

8 years 
piccolo 
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …



@2823

8 years 
tranquil 
* corrected bug in ERTL semantics (both delframe and newframe did the …



@2820

8 years 
sacerdot 
Proof obligation closed.



@2818

8 years 
sacerdot 
"Repaired", using non computational daemons.



@2807

8 years 
mckinna 
Yet another ErrorMessage?
Removed corresponding axiom in …



@2806

8 years 
tranquil 
new b_graph_translate obligations



@2801

8 years 
piccolo 
Partial commit not yet finished



@2796

8 years 
tranquil 
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …



@2786

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



@2785

8 years 
piccolo 
Traces.ma repaired



@2783

8 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2696

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



@2695

8 years 
sacerdot 
Renamed again.



@2693

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



@2691

8 years 
sacerdot 
ERTLtoERTLptr* moved to the proper place



@2689

8 years 
tranquil 
* fixed passes up to linearisation



@2681

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



@2674

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



@2666

8 years 
piccolo 
bug fixed in blocks.ma



@2645

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



@2604

8 years 
piccolo 
ERTLtoERTLptr in place.



@2601

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



@2590

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



@2566

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



@2564

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



@2563

8 years 
piccolo 
Repairing ERTL: show stopper found.



@2490

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



@2443

8 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

9 years 
sacerdot 
Minor changes while studying the proof.



@1729

9 years 
sacerdot 
Comment left from SVN merge removed.



@1601

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



@1515

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



@1463

9 years 
mulligan 
added erasure for lin



@1451

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



@1429

9 years 
sacerdot 
Useless and removed.



@1425

9 years 
mulligan 
changes to the fixpoint calculation in ertl



@1424

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



@1423

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



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



@1390

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



@1389

9 years 
sacerdot 
One more axiom closed.



@1388

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



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



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



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



@1327

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



@1324

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



@1318

9 years 
sacerdot 
Frame management implemented.



@1313

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



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


