

@3263

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



@3096

8 years 
tranquil 
preliminary work on closing correctness.ma



@3037

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



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



@2858

8 years 
sacerdot 
Trying to pretty print the code graph in visit order.
Slightly bugged …



@2848

8 years 
sacerdot 
The pretty printer for LTL.



@2845

8 years 
piccolo 
ERTLptr to LTL correctness proof started



@2796

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



@2783

8 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2601

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



@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

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



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



@2205

9 years 
campbell 
Get correctness.ma type checking again.



@2182

9 years 
tranquil 
updated linearisation pass



@2174

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



@2103

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



@1515

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



@1451

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



@1383

9 years 
sacerdot 
Potential bug fixed and bug found: the way pointers and labels are put …



@1381

9 years 
sacerdot 
Old commented out code removed.



@1380

9 years 
sacerdot 
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …



@1379

9 years 
sacerdot 
Invariant on LIN code removed. In Paris it was decided that a simpler …



@1378

9 years 
sacerdot 
New file LIN/joint_LTL_LIN.ma to factorize out the syntactic …



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



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



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



@1271

9 years 
mulligan 
finished, kind of



@1270

9 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1269

9 years 
sacerdot 
Useless include removed.



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



@1246

9 years 
sacerdot 
Yet another change to Joint.ma to accomodate all passes.
The concrete …



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



@1224

9 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1222

9 years 
sacerdot 
LTL fully ported to the joint syntax.



@1183

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



@1180

9 years 
mulligan 
lin to ltl pass complete



@1179

9 years 
mulligan 
changes to ertl, ltl and lin to use new notion of joint params. ertl …



@1171

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



@1168

9 years 
sacerdot 
Joint statements parameterized over a record.



@1166

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



@1164

9 years 
mulligan 
ltl to lin working again, more changes to joint syntax



@1163

9 years 
mulligan 
even more streamlining and fixes to get things type checking



@1161

9 years 
mulligan 
changes from today: merged ertl, ltl and lin into one datatype to …



@1149

9 years 
mulligan 
changes to get everything type checking again after changing names of …



@1132

9 years 
mulligan 
reunified ltl and lin instruction type, removing lifting in ltl and …



@1111

9 years 
mulligan 
minor change: marked some possibly dodgy (and very complex) code



@1110

9 years 
mulligan 
changes to get ltl to lin pass to work properly



@1089

9 years 
mulligan 
more changes from earlier in the week



@1082

10 years 
mulligan 
work from today on ertl > ltl pass



@759

10 years 
mulligan 
More work on the RTL to ERTL pass.



@757

10 years 
mulligan 
Lots more fixing to get both front and backends using same conventions …



@753

10 years 
mulligan 
Work from today.



@733

10 years 
mulligan 
Fixed partial commit.



@728

10 years 
mulligan 
Changes from last two days.



@723

10 years 
mulligan 
Added dependent type internalising the invariant that LIN function …



@722

10 years 
mulligan 
Committing changes from today. Several files do not typecheck.



@716

10 years 
mulligan 
Finished translating LTL statements to LIN statements. Need to …



@715

10 years 
mulligan 
Restored rev from Util as it appears that list reversal is not a part …



@714

10 years 
mulligan 
Work on translation from LTL to LIN.



@713

10 years 
mulligan 
Commit of initial LTL files.
