|
|
@2917
|
7 years |
tranquil |
made it so that a 0 offset does not generate adding ops when accessing …
|
|
|
@2916
|
7 years |
tranquil |
corrected yet another endianness bug in load and store
|
|
|
@2915
|
7 years |
sacerdot |
Dead code removed.
|
|
|
@2914
|
7 years |
campbell |
Use single definition for stack measurement.
|
|
|
@2912
|
7 years |
sacerdot |
Ouch, another bug in the very same function.
Fixed too, on an example …
|
|
|
@2911
|
7 years |
sacerdot |
Bug fixed in the translation of casts.
|
|
|
@2910
|
7 years |
sacerdot |
Abstract statuses for ASM and OC completed.
A simple test program can …
|
|
|
@2907
|
7 years |
sacerdot |
1. a few bugs fixed
2. as_return implemented for ASM & OC
|
|
|
@2906
|
7 years |
sacerdot |
Bug fixed.
|
|
|
@2905
|
7 years |
sacerdot |
Semantics of ASM in place (up to return values and function call …
|
|
|
@2899
|
7 years |
sacerdot |
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …
|
|
|
@2898
|
7 years |
piccolo |
1) simplification of cond and seq case for StatusSimulationHelper? …
|
|
|
@2897
|
7 years |
campbell |
Minor tidying.
|
|
|
@2896
|
7 years |
campbell |
Complete part of measurable to structured subtraces proof that
shows …
|
|
|
@2895
|
7 years |
campbell |
Match up function id from RTLabs Callstate with shadow stack,
use in …
|
|
|
@2894
|
7 years |
campbell |
Some progress on showing that the change to structured traces …
|
|
|
@2893
|
7 years |
campbell |
Add tlr_unrepeating.
|
|
|
@2892
|
7 years |
campbell |
Add cost hypotheses.
|
|
|
@2891
|
7 years |
piccolo |
added precondition on seq statement and tested correct in the …
|
|
|
@2889
|
7 years |
sacerdot |
It works very nice!
|
|
|
@2888
|
7 years |
tranquil |
backtracked some partial changes
|
|
|
@2887
|
7 years |
tranquil |
Corrected bug where eliminable statements where not eliminated. …
|
|
|
@2886
|
7 years |
piccolo |
partial commit
|
|
|
@2885
|
7 years |
sacerdot |
Hint at how to change everything.
|
|
|
@2883
|
7 years |
piccolo |
partial commit
|
|
|
@2879
|
7 years |
tranquil |
changed coercion from list of joint_seq to blocks to a more efficient one
|
|
|
@2878
|
7 years |
tranquil |
backtracked some changes that were not ready for commit
|
|
|
@2877
|
7 years |
garnier |
Correction of a bug in my former bug correction.
|
|
|
@2876
|
7 years |
tranquil |
corrected another endianess bug in joint_semantics. Switched some …
|
|
|
@2875
|
7 years |
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
|
@2871
|
7 years |
tranquil |
op2 evaluation on beval's rendered oblivious to carry bit when …
|
|
|
@2870
|
7 years |
sacerdot |
Proof fixed.
|
|
|
@2869
|
7 years |
tranquil |
some reorganization of definitions, and a new taaf_append_taaf
|
|
|
@2868
|
7 years |
sacerdot |
Pretty printing of ERTL and ERTLptr code.
|
|
|
@2866
|
7 years |
tranquil |
corrected two bugs of the translation: constant translation used wrong …
|
|
|
@2865
|
7 years |
sacerdot |
…
|
|
|
@2863
|
7 years |
piccolo |
Added new invariant to good_if
Generalized version of cond case for …
|
|
|
@2862
|
7 years |
sacerdot |
Repaired, a reverse was enough.
|
|
|
@2861
|
7 years |
mckinna |
PROVISIONAL commit:
Unintentional list reversal cause final step of …
|
|
|
@2860
|
7 years |
sacerdot |
RTL printing, core dumps ATM
|
|
|
@2859
|
7 years |
sacerdot |
Pretty printing improved (now it always starts the visit from lbl 1).
|
|
|
@2858
|
7 years |
sacerdot |
Trying to pretty print the code graph in visit order.
Slightly bugged …
|
|
|
@2857
|
7 years |
garnier |
CL to CM: some invariants strengthened.
|
|
|
@2855
|
7 years |
piccolo |
little bug fixed in TranslateUtils?.
|
|
|
@2853
|
7 years |
sacerdot |
Pretty printing of line/label numbers.
|
|
|
@2852
|
7 years |
mckinna |
Interim commit to re-establish well-typedness after all the recent …
|
|
|
@2851
|
7 years |
piccolo |
partial commit
|
|
|
@2850
|
7 years |
garnier |
Progress on CL to CM. Some more cases closed modulo some critical …
|
|
|
@2849
|
7 years |
piccolo |
partial commit
|
|
|
@2848
|
7 years |
sacerdot |
The pretty printer for LTL.
|
|
|
@2847
|
7 years |
sacerdot |
…
|
|
|
@2846
|
7 years |
sacerdot |
Pretty printing of joint programs.
|
|
|
@2845
|
7 years |
piccolo |
ERTLptr to LTL correctness proof started
|
|
|
@2844
|
7 years |
piccolo |
Stupid bug fixed
|
|
|
@2843
|
7 years |
piccolo |
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …
|
|
|
@2841
|
7 years |
sacerdot |
The compiler now computes also the stack cost for every intermediate …
|
|
|
@2840
|
7 years |
campbell |
Remove irrelevant stuff from RTLabs_partial_traces
|
|
|
@2839
|
7 years |
campbell |
Basic structure of RTLabs measurable to structured traces results.
|
|
|
@2838
|
7 years |
garnier |
Closing some more cases
|
|
|
@2837
|
7 years |
tranquil |
* filled in evaluation of LTL/LIN's extended instrucitons
|
|
|
@2835
|
7 years |
sacerdot |
Included Uses.ma which is required by the untrusted code.
The …
|
|
|
@2832
|
7 years |
sacerdot |
Added abstraction in front of cases daemon for code extraction.
|
|
|
@2830
|
7 years |
sacerdot |
Added abstractions in front of cases daemon for code extraction.
|
|
|
@2828
|
7 years |
sacerdot |
1. New semantics.ma file that puts together all semantics.
It …
|
|
|
@2825
|
7 years |
garnier |
Progress, Clight to Cminor
|
|
|
@2824
|
7 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
@2823
|
7 years |
tranquil |
* corrected bug in ERTL semantics (both delframe and newframe did the …
|
|
|
@2822
|
7 years |
garnier |
A consitent proof state for Clight to Cminor, with some progress (and …
|
|
|
@2821
|
7 years |
tranquil |
* implemented preclassified system for joint (in joint/joint_fullexec.ma)
|
|
|
@2820
|
7 years |
sacerdot |
Proof obligation closed.
|
|
|
@2819
|
7 years |
sacerdot |
Proof obligation closed.
|
|
|
@2818
|
7 years |
sacerdot |
"Repaired", using non computational daemons.
|
|
|
@2817
|
7 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
@2816
|
7 years |
sacerdot |
Repaired after Paolo's commit.
|
|
|
@2811
|
7 years |
sacerdot |
Pre-classified system for RTLabs.
|
|
|
@2809
|
7 years |
sacerdot |
…
|
|
|
@2808
|
7 years |
tranquil |
added local_stacksize to joint internal functions to accomodate for …
|
|
|
@2807
|
7 years |
mckinna |
Yet another ErrorMessage?
Removed corresponding axiom in …
|
|
|
@2806
|
7 years |
tranquil |
new b_graph_translate obligations
|
|
|
@2802
|
7 years |
sacerdot |
New file Clight_classified_system with the classified system for …
|
|
|
@2801
|
7 years |
piccolo |
Partial commit not yet finished
|
|
|
@2800
|
7 years |
campbell |
Tidy up Measurable.ma a little, get rid of obsolete comments.
|
|
|
@2799
|
7 years |
tranquil |
* added taaf_to_taa, conversion from trace_any_any_free to …
|
|
|
@2796
|
7 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
@2795
|
7 years |
sacerdot |
Added new function Measurable.observe_all_in_measurable to be used to …
|
|
|
@2794
|
7 years |
mckinna |
Minor tweaks/tidying up
|
|
|
@2793
|
7 years |
campbell |
Oops, gave fields wrong order during initialisation.
|
|
|
@2786
|
7 years |
piccolo |
Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
|
|
|
@2785
|
7 years |
piccolo |
Traces.ma repaired
|
|
|
@2784
|
7 years |
sacerdot |
Repaired after Mauro's commit.
|
|
|
@2783
|
7 years |
piccolo |
modified joint_closed_internal_function definition (added condition on …
|
|
|
@2782
|
7 years |
sacerdot |
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
|
|
|
@2781
|
7 years |
sacerdot |
One more computational daemon closed.
|
|
|
@2774
|
7 years |
sacerdot |
1. the compiler now outputs both the stack cost model and the max …
|
|
|
@2772
|
7 years |
sacerdot |
Useless code removed.
|
|
|
@2771
|
7 years |
sacerdot |
Some speed up in Policy.ma.
|
|
|
@2770
|
7 years |
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
|
@2769
|
7 years |
mckinna |
Mistakenly commented out
both as_cost_get_label (needed; OK)
as well …
|
|
|
@2768
|
7 years |
mckinna |
Nightmare: file no longer typechecks,
because defn as_cost_get_labels …
|
|
|
@2767
|
7 years |
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
|