|
|
|
@3042
|
8 years |
sacerdot |
Repaired.
|
|
|
|
@3041
|
8 years |
sacerdot |
Repaired
|
|
|
|
@3037
|
8 years |
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
|
|
@3014
|
8 years |
tranquil |
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
|
|
|
|
@2996
|
8 years |
sacerdot |
Printing of graphs now starts from the entry point.
|
|
|
|
@2991
|
8 years |
piccolo |
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …
|
|
|
|
@2985
|
8 years |
sacerdot |
Order of printing of lines in LIN fixed again, truly this time. But I …
|
|
|
|
@2983
|
8 years |
sacerdot |
LIN code was printed in reverse order. But I have not really …
|
|
|
|
@2982
|
8 years |
sacerdot |
Pretty priting of LIN implemented.
|
|
|
|
@2980
|
8 years |
tranquil |
fixed b_graph_translate
|
|
|
|
@2973
|
8 years |
tranquil |
semanticUtils adapted to changes in TranslateUtils?
|
|
|
|
@2970
|
8 years |
tranquil |
now joint_if_entry can change when a preamble is added, so code points …
|
|
|
|
@2968
|
8 years |
sacerdot |
The initial status memory was not really initialized. Now it is.
|
|
|
|
@2967
|
8 years |
sacerdot |
Semantics changed so that a terminating joint program that returns an …
|
|
|
|
@2957
|
8 years |
tranquil |
fixed semantics_blocks
|
|
|
|
@2954
|
8 years |
tranquil |
resolved circular dependency for ERTLptr's semantics
|
|
|
|
@2952
|
8 years |
tranquil |
* corrected all back-end premains to not pass any arguments to the …
|
|
|
|
@2950
|
8 years |
sacerdot |
linearise repaired (did I do the right thing???)
|
|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
|
@2940
|
8 years |
sacerdot |
1. StatusSimulationHelper? changed to allow to use status_rel that …
|
|
|
|
@2939
|
8 years |
sacerdot |
Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
|
|
|
|
@2932
|
8 years |
sacerdot |
Same comment as previous commit on this file: the previous commit was …
|
|
|
|
@2929
|
8 years |
sacerdot |
Bug fixed: the coercion mechanism made you think that the CALL case …
|
|
|
|
@2920
|
8 years |
sacerdot |
dos2unix-ed
|
|
|
|
@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 …
|
|
|
|
@2886
|
8 years |
piccolo |
partial commit
|
|
|
|
@2885
|
8 years |
sacerdot |
Hint at how to change everything.
|
|
|
|
@2883
|
8 years |
piccolo |
partial commit
|
|
|
|
@2879
|
8 years |
tranquil |
changed coercion from list of joint_seq to blocks to a more efficient one
|
|
|
|
@2878
|
8 years |
tranquil |
backtracked some changes that were not ready for commit
|
|
|
|
@2876
|
8 years |
tranquil |
corrected another endianess bug in joint_semantics. Switched some …
|
|
|
|
@2869
|
8 years |
tranquil |
some reorganization of definitions, and a new taaf_append_taaf
|
|
|
|
@2865
|
8 years |
sacerdot |
…
|
|
|
|
@2863
|
8 years |
piccolo |
Added new invariant to good_if
Generalized version of cond case for …
|
|
|
|
@2859
|
8 years |
sacerdot |
Pretty printing improved (now it always starts the visit from lbl 1).
|
|
|
|
@2858
|
8 years |
sacerdot |
Trying to pretty print the code graph in visit order.
Slightly bugged …
|
|
|
|
@2855
|
8 years |
piccolo |
little bug fixed in TranslateUtils?.
|
|
|
|
@2853
|
8 years |
sacerdot |
Pretty printing of line/label numbers.
|
|
|
|
@2851
|
8 years |
piccolo |
partial commit
|
|
|
|
@2847
|
8 years |
sacerdot |
…
|
|
|
|
@2846
|
8 years |
sacerdot |
Pretty printing of joint programs.
|
|
|
|
@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 …
|
|
|
|
@2821
|
8 years |
tranquil |
* implemented preclassified system for joint (in joint/joint_fullexec.ma)
|
|
|
|
@2817
|
8 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
|
@2816
|
8 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
|
@2808
|
8 years |
tranquil |
added local_stacksize to joint internal functions to accomodate for …
|
|
|
|
@2806
|
8 years |
tranquil |
new b_graph_translate obligations
|
|
|
|
@2796
|
8 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
|
@2785
|
8 years |
piccolo |
Traces.ma repaired
|
|
|
|
@2784
|
8 years |
sacerdot |
Repaired after Mauro's commit.
|
|
|
|
@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 …
|
|
|
|
@2760
|
8 years |
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
|
|
@2757
|
8 years |
tranquil |
many things are still broken, but there is a partial backtrack on …
|
|
|
|
@2755
|
8 years |
tranquil |
* changed primitives of abstract status (with stuf that is probably …
|
|
|
|
@2723
|
8 years |
campbell |
Library name typo fixed.
|
|
|
|
@2716
|
8 years |
sacerdot |
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
|
|
|
|
@2712
|
8 years |
tranquil |
changed some fields of joint_internal_function's invariant
fixed linearise
|
|
|
|
@2708
|
8 years |
tranquil |
fixed linearise and LINToASM
LINToASM has now correct transformation …
|
|
|
|
@2702
|
8 years |
sacerdot |
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …
|
|
|
|
@2688
|
8 years |
tranquil |
* in Arithmeticcs.ma: commented include that breaks script in latest …
|
|
|
|
@2687
|
8 years |
tranquil |
* polished some interfaces
|
|
|
|
@2683
|
8 years |
tranquil |
proof of properties of b_graph_program_transform (with an open axiom)
|
|
|
|
@2681
|
8 years |
tranquil |
* improvements to the graph translation function
* fixed passes up to LTL
|
|
|
|
@2675
|
8 years |
tranquil |
* a generic graph program transformation
|
|
|
|
@2674
|
8 years |
tranquil |
* another change in block definition
* RTLabs -> RTL and ERTL -> …
|
|
|
|
@2666
|
8 years |
piccolo |
bug fixed in blocks.ma
|
|
|
|
@2661
|
8 years |
sacerdot |
stacksize "repaired" by "considering" tailcalls
Some daemons added …
|
|
|
|
@2655
|
8 years |
tranquil |
new step in code semantic lemma
|
|
|
|
@2647
|
8 years |
sacerdot |
Stupid typo fixed.
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2642
|
8 years |
piccolo |
fixed joint/Traces after having posed block 0 to be Code
|
|
|
|
@2641
|
8 years |
piccolo |
defined dummy block code equals to 0
|
|
|
|
@2639
|
8 years |
sacerdot |
We are not going to prove erasure. Thus this becomes dead code.
|
|
|
|
@2638
|
8 years |
piccolo |
Back-end fixes for last Garnier's commit that removes the regions from …
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2599
|
8 years |
tranquil |
* map_opt and map on positive maps are now clean (erase empty …
|
|
|
|
@2595
|
8 years |
tranquil |
* dropped locals and exit from definition of joint_if_function
* new …
|
|
|
|
@2592
|
8 years |
piccolo |
main lemma of ERTLptr in place
|
|
|
|
@2590
|
8 years |
piccolo |
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …
|
|
|
|
@2570
|
8 years |
piccolo |
ERTLtoERTLptr in place
|
|
|
|
@2564
|
8 years |
piccolo |
ERTL fully repaired, useless part of return value of pop_ra
removed.
|
|
|
|
@2562
|
8 years |
piccolo |
linearise modified
|
|
|
|
@2561
|
8 years |
tranquil |
* moved CALL as different case than joint_seq: lots of broken code now …
|
|
|
|
@2559
|
8 years |
piccolo |
lineariseProof finished
|
|
|
|
@2557
|
8 years |
tranquil |
minor modification of commented (for now) proof of correctness of …
|
|
|
|
@2556
|
8 years |
tranquil |
in joint semantics and traces: added a last popped calling address to …
|
|
|
|
@2555
|
8 years |
piccolo |
lemma eval_call_ok finished
|
|
|
|
@2553
|
8 years |
tranquil |
as_classify changed to a partial function
added a status for tailcalls
|
|
|
|
@2551
|
8 years |
piccolo |
completed isFinal and fetchStatementSigmaCommute. Fixed exit …
|
|
|
|
@2548
|
8 years |
tranquil |
in BackEndOps?, cleaner def of be_op2
new statement of …
|
|
|
|
@2547
|
8 years |
tranquil |
going on in proof of linearise
simplified by use of monadic functional …
|
|
|
|
@2543
|
8 years |
piccolo |
finished stmt_at_sigma_commute
|
|
|
|
@2538
|
8 years |
tranquil |
fixed Traces.ma after changes in joint/semantics.ma
|
|
|
|
@2537
|
8 years |
tranquil |
rolled back changes on calls in joint. Now the save_frame parameter …
|
|
|
|
@2536
|
8 years |
piccolo |
finished eval_seq_no_pc_sigma_commute lemma
|
|
|
|
@2532
|
8 years |
tranquil |
added FCOND in LIN, and rewritten linearise so that it never adds a …
|
|
|
|
