source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2938   8 years sacerdot 1. proof of "all eliminable are eliminable" completed 2. the notion of …
(edit) @2937   8 years campbell Speed up checking of RTLabs/CostInj.ma.
(edit) @2936   8 years campbell Disable initialisation code generation in Cminor, propogate init data …
(edit) @2935   8 years tranquil separation of RTL semantics in three different versions, and …
(edit) @2934   8 years sacerdot Patch to obtain more easily comparable traces.
(edit) @2933   8 years sacerdot New extraction, several bug fixed. RTL_semantics fixed by hand, will …
(edit) @2932   8 years sacerdot Same comment as previous commit on this file: the previous commit was …
(edit) @2931   8 years sacerdot Partial back-track from Paolo's commit, that was partial.
(edit) @2930   8 years sacerdot More progress. Some useless parameters have been removed from the …
(edit) @2929   8 years sacerdot Bug fixed: the coercion mechanism made you think that the CALL case …
(edit) @2928   8 years tranquil some sketches about correctness proof
(edit) @2927   8 years tranquil stupid bug in bool_of_beval
(edit) @2926   8 years tranquil corrected bug in executing Sub
(edit) @2925   8 years tranquil corrected bug in toggle_bool
(edit) @2924   8 years campbell Make calls to a known identifier actually use a direct call.
(edit) @2923   8 years campbell Remove some leftovers.
(edit) @2922   8 years sacerdot Progress: proof of "eliminable statements can be eliminated" almost …
(edit) @2921   8 years sacerdot Extracted again.
(edit) @2920   8 years sacerdot dos2unix-ed
(edit) @2919   8 years fguidi "MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
(edit) @2918   8 years tranquil erased stupid accidental paste at the start of file (happened when …
(edit) @2917   8 years tranquil made it so that a 0 offset does not generate adding ops when accessing …
(edit) @2916   8 years tranquil corrected yet another endianness bug in load and store
(edit) @2915   8 years sacerdot Dead code removed.
(edit) @2914   8 years campbell Use single definition for stack measurement.
(edit) @2913   8 years sacerdot Bug corrected by hand. It will be corrected automatically by next …
(edit) @2912   8 years sacerdot Ouch, another bug in the very same function. Fixed too, on an example …
(edit) @2911   8 years sacerdot Bug fixed in the translation of casts.
(edit) @2910   8 years sacerdot Abstract statuses for ASM and OC completed. A simple test program can …
(edit) @2909   8 years sacerdot New extraction.
(edit) @2908   8 years sacerdot Bug fixed by hand, they will be fixed automatically by the new extraction.
(edit) @2907   8 years sacerdot 1. a few bugs fixed 2. as_return implemented for ASM & OC
(edit) @2906   8 years sacerdot Bug fixed.
(edit) @2905   8 years sacerdot Semantics of ASM in place (up to return values and function call …
(edit) @2904   8 years sacerdot 1. Algorithm modified by hand to make it run faster. The trusted …
(edit) @2903   8 years sacerdot Extracted again.
(edit) @2902   8 years sacerdot Quick hack to allow printing of OC code. It will be automatically …
(edit) @2901   8 years sacerdot 1. backendPrinter renamed to printer 2. Clight printing branched into …
(edit) @2900   8 years sacerdot Flushing to understand where it is slow.
(edit) @2899   8 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
(edit) @2898   8 years piccolo 1) simplification of cond and seq case for StatusSimulationHelper? …
(edit) @2897   8 years campbell Minor tidying.
(edit) @2896   8 years campbell Complete part of measurable to structured subtraces proof that shows …
(edit) @2895   8 years campbell Match up function id from RTLabs Callstate with shadow stack, use in …
(edit) @2894   8 years campbell Some progress on showing that the change to structured traces …
(edit) @2893   8 years campbell Add tlr_unrepeating.
(edit) @2892   8 years campbell Add cost hypotheses.
(edit) @2891   8 years piccolo added precondition on seq statement and tested correct in the …
(edit) @2890   8 years sacerdot Exported again, now the execution is correct up to LIN for a simple …
(edit) @2889   8 years sacerdot It works very nice!
(edit) @2888   8 years tranquil backtracked some partial changes
(edit) @2887   8 years tranquil Corrected bug where eliminable statements where not eliminated. …
(edit) @2886   8 years piccolo partial commit
(edit) @2885   8 years sacerdot Hint at how to change everything.
(edit) @2884   8 years sacerdot Debugging print added.
(edit) @2883   8 years piccolo partial commit
(edit) @2882   8 years sacerdot …
(edit) @2881   8 years sacerdot …
(edit) @2880   8 years sacerdot …
(edit) @2879   8 years tranquil changed coercion from list of joint_seq to blocks to a more efficient one
(edit) @2878   8 years tranquil backtracked some changes that were not ready for commit
(edit) @2877   8 years garnier Correction of a bug in my former bug correction.
(edit) @2876   8 years tranquil corrected another endianess bug in joint_semantics. Switched some …
(edit) @2875   8 years sacerdot Pretty printing of object code integrated too. A couple of axioms make …
(edit) @2874   8 years sacerdot Syntax fixed: ./cerco [-exec] filename annotationoption
(edit) @2873   8 years sacerdot Extracted again.
(edit) @2872   8 years tassi Fix list of distributed files so that the debian package can be built
(edit) @2871   8 years tranquil op2 evaluation on beval's rendered oblivious to carry bit when …
(edit) @2870   8 years sacerdot Proof fixed.
(edit) @2869   8 years tranquil some reorganization of definitions, and a new taaf_append_taaf
(edit) @2868   8 years sacerdot Pretty printing of ERTL and ERTLptr code.
(edit) @2867   8 years sacerdot New extraction after indianess bug fixes by Paolo.
(edit) @2866   8 years tranquil corrected two bugs of the translation: constant translation used wrong …
(edit) @2865   8 years sacerdot …
(edit) @2864   8 years sacerdot I must have drunk yesterday: all RTL passes are printed correctly; the …
(edit) @2863   8 years piccolo Added new invariant to good_if Generalized version of cond case for …
(edit) @2862   8 years sacerdot Repaired, a reverse was enough.
(edit) @2861   8 years mckinna PROVISIONAL commit: Unintentional list reversal cause final step of …
(edit) @2860   8 years sacerdot RTL printing, core dumps ATM
(edit) @2859   8 years sacerdot Pretty printing improved (now it always starts the visit from lbl 1).
(edit) @2858   8 years sacerdot Trying to pretty print the code graph in visit order. Slightly bugged …
(edit) @2857   8 years garnier CL to CM: some invariants strengthened.
(edit) @2856   8 years sacerdot Pretty printing of LTL almost finished.
(edit) @2855   8 years piccolo little bug fixed in TranslateUtils?.
(edit) @2854   8 years sacerdot Pretty printing of the LTL program.
(edit) @2853   8 years sacerdot Pretty printing of line/label numbers.
(edit) @2852   8 years mckinna Interim commit to re-establish well-typedness after all the recent …
(edit) @2851   8 years piccolo partial commit
(edit) @2850   8 years garnier Progress on CL to CM. Some more cases closed modulo some critical …
(edit) @2849   8 years piccolo partial commit
(edit) @2848   8 years sacerdot The pretty printer for LTL.
(edit) @2847   8 years sacerdot …
(edit) @2846   8 years sacerdot Pretty printing of joint programs.
(edit) @2845   8 years piccolo ERTLptr to LTL correctness proof started
(edit) @2844   8 years piccolo Stupid bug fixed
(edit) @2843   8 years piccolo 1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
(edit) @2842   8 years sacerdot The compiler can now show all back-end traces too (assembly and object …
(edit) @2841   8 years sacerdot The compiler now computes also the stack cost for every intermediate …
(edit) @2840   8 years campbell Remove irrelevant stuff from RTLabs_partial_traces
(edit) @2839   8 years campbell Basic structure of RTLabs measurable to structured traces results.
Note: See TracRevisionLog for help on using the revision log.