|
|
|
@3145
|
8 years |
tranquil |
* removed sigma types from traces of intensional events
* completed …
|
|
|
|
@3037
|
8 years |
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
|
@2865
|
8 years |
sacerdot |
…
|
|
|
|
@2863
|
8 years |
piccolo |
Added new invariant to good_if
Generalized version of cond case for …
|
|
|
|
@2843
|
8 years |
piccolo |
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …
|
|
|
|
@2824
|
8 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
|
@2823
|
8 years |
tranquil |
* corrected bug in ERTL semantics (both delframe and newframe did the …
|
|
|
|
@2808
|
8 years |
tranquil |
added local_stacksize to joint internal functions to accomodate for …
|
|
|
|
@2783
|
8 years |
piccolo |
modified joint_closed_internal_function definition (added condition on …
|
|
|
|
@2774
|
8 years |
sacerdot |
1. the compiler now outputs both the stack cost model and the max …
|
|
|
|
@2712
|
8 years |
tranquil |
changed some fields of joint_internal_function's invariant
fixed linearise
|
|
|
|
@2688
|
8 years |
tranquil |
* in Arithmeticcs.ma: commented include that breaks script in latest …
|
|
|
|
@2681
|
8 years |
tranquil |
* improvements to the graph translation function
* fixed passes up to LTL
|
|
|
|
@2655
|
8 years |
tranquil |
new step in code semantic lemma
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2595
|
8 years |
tranquil |
* dropped locals and exit from definition of joint_if_function
* new …
|
|
|
|
@2562
|
8 years |
piccolo |
linearise modified
|
|
|
|
@2561
|
8 years |
tranquil |
* moved CALL as different case than joint_seq: lots of broken code now …
|
|
|
|
@2547
|
8 years |
tranquil |
going on in proof of linearise
simplified by use of monadic functional …
|
|
|
|
@2537
|
8 years |
tranquil |
rolled back changes on calls in joint. Now the save_frame parameter …
|
|
|
|
@2532
|
8 years |
tranquil |
added FCOND in LIN, and rewritten linearise so that it never adds a …
|
|
|
|
@2490
|
8 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
|
@2462
|
8 years |
tranquil |
separated in back end values program counters from code pointers …
|
|
|
|
@2457
|
8 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
|
@2437
|
8 years |
tranquil |
generalised calls to calls with pointers
|
|
|
|
@2422
|
8 years |
tranquil |
adapted joint to cl_call f
|
|
|
|
@2286
|
8 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1471
|
9 years |
mulligan |
finished erasure and generalised so as to work on arbitrary joint programs
|
|
|
|
@1380
|
9 years |
sacerdot |
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
|
|
|
|
@1282
|
9 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
|
@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 …
|
|
|
|
@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.
|
|
|
|
@1182
|
9 years |
mulligan |
changes to semantics: removing parameterised "next" element in joint …
|
|
|
|
@1176
|
9 years |
sacerdot |
…
|
|
|
|
@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 |
…
|
|
copied from src/joint/JointLTLLIN.ma:
|
|
|
|
@1166
|
9 years |
mulligan |
moved joint ltl lin files into their own directory. more changes to …
|
