source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2967   7 years sacerdot Semantics changed so that a terminating joint program that returns an …
(edit) @2966   7 years sacerdot Modified by hand files (to improve a little bit the performance).
(edit) @2965   7 years sacerdot Code performance improved a bit by hand.
(edit) @2964   7 years sacerdot Debugging code removed.
(edit) @2963   7 years sacerdot Bug fixed: the pre-main for the final code is now COST k1 …
(edit) @2962   7 years sacerdot Most performant algorithm restored.
(edit) @2961   7 years sacerdot Bug fixed (stupid typo in pre-main code made the compiler diverge on …
(edit) @2960   7 years sacerdot New extraction, it diverges in RTL execution now.
(edit) @2959   7 years sacerdot Typo
(edit) @2958   7 years sacerdot Error message implemented.
(edit) @2957   7 years tranquil fixed semantics_blocks
(edit) @2956   7 years tranquil fixed LTL/LIN semantics
(edit) @2955   7 years tranquil corrected stupid typo
(edit) @2954   7 years tranquil resolved circular dependency for ERTLptr's semantics
(edit) @2953   7 years campbell Fix silly label handling bug I realised was there during my talk…
(edit) @2952   7 years tranquil * corrected all back-end premains to not pass any arguments to the …
(edit) @2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
(edit) @2950   7 years sacerdot linearise repaired (did I do the right thing???)
(edit) @2949   7 years sacerdot Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
(edit) @2948   7 years campbell Finish up measurable to structured proof, exposing the prefix and …
(edit) @2947   7 years campbell Init change in measurable to structured file.
(edit) @2946   7 years tranquil main novelties: * there is an in-built stack_usage nat in joint …
(edit) @2945   7 years campbell Minor tweak.
(edit) @2944   7 years sacerdot Some progress.
(edit) @2943   7 years sacerdot Mauro, I have put a daemon in place of the proof obligation that used …
(edit) @2942   7 years sacerdot Many changes: 1. Coloured graphs are now specified in terms of …
(edit) @2941   7 years campbell Update proof slides.
(edit) @2940   7 years sacerdot 1. StatusSimulationHelper? changed to allow to use status_rel that …
(edit) @2939   7 years sacerdot Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
(edit) @2938   7 years sacerdot 1. proof of "all eliminable are eliminable" completed 2. the notion of …
(edit) @2937   7 years campbell Speed up checking of RTLabs/CostInj.ma.
(edit) @2936   7 years campbell Disable initialisation code generation in Cminor, propogate init data …
(edit) @2935   7 years tranquil separation of RTL semantics in three different versions, and …
(edit) @2934   7 years sacerdot Patch to obtain more easily comparable traces.
(edit) @2933   7 years sacerdot New extraction, several bug fixed. RTL_semantics fixed by hand, will …
(edit) @2932   7 years sacerdot Same comment as previous commit on this file: the previous commit was …
(edit) @2931   7 years sacerdot Partial back-track from Paolo's commit, that was partial.
(edit) @2930   7 years sacerdot More progress. Some useless parameters have been removed from the …
(edit) @2929   7 years sacerdot Bug fixed: the coercion mechanism made you think that the CALL case …
(edit) @2928   7 years tranquil some sketches about correctness proof
(edit) @2927   7 years tranquil stupid bug in bool_of_beval
(edit) @2926   7 years tranquil corrected bug in executing Sub
(edit) @2925   7 years tranquil corrected bug in toggle_bool
(edit) @2924   7 years campbell Make calls to a known identifier actually use a direct call.
(edit) @2923   7 years campbell Remove some leftovers.
(edit) @2922   7 years sacerdot Progress: proof of "eliminable statements can be eliminated" almost …
(edit) @2921   7 years sacerdot Extracted again.
(edit) @2920   7 years sacerdot dos2unix-ed
(edit) @2919   7 years fguidi "MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
(edit) @2918   7 years tranquil erased stupid accidental paste at the start of file (happened when …
(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) @2913   7 years sacerdot Bug corrected by hand. It will be corrected automatically by next …
(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) @2909   7 years sacerdot New extraction.
(edit) @2908   7 years sacerdot Bug fixed by hand, they will be fixed automatically by the new extraction.
(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) @2904   7 years sacerdot 1. Algorithm modified by hand to make it run faster. The trusted …
(edit) @2903   7 years sacerdot Extracted again.
(edit) @2902   7 years sacerdot Quick hack to allow printing of OC code. It will be automatically …
(edit) @2901   7 years sacerdot 1. backendPrinter renamed to printer 2. Clight printing branched into …
(edit) @2900   7 years sacerdot Flushing to understand where it is slow.
(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) @2890   7 years sacerdot Exported again, now the execution is correct up to LIN for a simple …
(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) @2884   7 years sacerdot Debugging print added.
(edit) @2883   7 years piccolo partial commit
(edit) @2882   7 years sacerdot …
(edit) @2881   7 years sacerdot …
(edit) @2880   7 years sacerdot …
(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) @2874   7 years sacerdot Syntax fixed: ./cerco [-exec] filename annotationoption
(edit) @2873   7 years sacerdot Extracted again.
(edit) @2872   7 years tassi Fix list of distributed files so that the debian package can be built
(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.
Note: See TracRevisionLog for help on using the revision log.