source: src

Revision Log Mode:


Legend:

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