|
|
@2952
|
8 years |
tranquil |
* corrected all back-end premains to not pass any arguments to the …
|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built 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
|
9 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
|
10 years |
sacerdot |
Potential bug fixed and bug found: the way pointers and labels are put …
|
|
|
@1381
|
10 years |
sacerdot |
Old commented out code removed.
|
|
|
@1380
|
10 years |
sacerdot |
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
|
|
|
@1379
|
10 years |
sacerdot |
Invariant on LIN code removed. In Paris it was decided that a simpler …
|
|
|
@1378
|
10 years |
sacerdot |
New file LIN/joint_LTL_LIN.ma to factorize out the syntactic …
|
|
|
@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 …
|
|
|
@1324
|
10 years |
sacerdot |
The semantics of extended statements must also consider the label …
|
|
|
@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 …
|
|
|
@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) …
|
|
|
@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.
|
|
|
@1252
|
10 years |
sacerdot |
graph_params added to joint/Joint.ma, together with useful common …
|
|
|
@1250
|
10 years |
sacerdot |
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …
|
|
|
@1246
|
10 years |
sacerdot |
Yet another change to Joint.ma to accomodate all passes.
The concrete …
|
|
|
@1236
|
10 years |
sacerdot |
LTLToLin.ma completed (up to a couple of daemons used to provide dead …
|
|
|
@1233
|
10 years |
sacerdot |
1) Ported to Brian's new dependent type for fullexec
2) Universe level …
|
|
|
@1224
|
10 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
@1222
|
10 years |
sacerdot |
LTL fully ported to the joint syntax.
|
|
|
@1183
|
10 years |
mulligan |
removed parameterised label types in the three lowest level languages
|
|
|
@1180
|
10 years |
mulligan |
lin to ltl pass complete
|
|
|
@1179
|
10 years |
mulligan |
changes to ertl, ltl and lin to use new notion of joint params. ertl …
|
|
|
@1171
|
10 years |
mulligan |
changes made on claudio's request: changed order of nesting in the …
|
|
|
@1168
|
10 years |
sacerdot |
Joint statements parameterized over a record.
|
|
|
@1166
|
10 years |
mulligan |
moved joint ltl lin files into their own directory. more changes to …
|
|
|
@1164
|
10 years |
mulligan |
ltl to lin working again, more changes to joint syntax
|
|
|
@1163
|
10 years |
mulligan |
even more streamlining and fixes to get things type checking
|
|
|
@1161
|
10 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
@1149
|
10 years |
mulligan |
changes to get everything type checking again after changing names of …
|
|
|
@1132
|
10 years |
mulligan |
reunified ltl and lin instruction type, removing lifting in ltl and …
|
|
|
@1111
|
10 years |
mulligan |
minor change: marked some possibly dodgy (and very complex) code
|
|
|
@1110
|
10 years |
mulligan |
changes to get ltl to lin pass to work properly
|
|
|
@1089
|
10 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.
|