source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3033   8 years sacerdot Bug fixed: sign_extension was extending according to the _second_ bit, …
(edit) @3032   8 years campbell Remind myself why ms_rel_normal is reasonable.
(edit) @3031   8 years campbell Tidy up RTLabs preclassified_system definitions.
(edit) @3030   8 years campbell Break up front-end for correctness proof. Use let rec to prevent …
(edit) @3029   8 years sacerdot New extraction after DPH/DPL bug fixing.
(edit) @3028   8 years sacerdot Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
(edit) @3027   8 years sacerdot Another output used by the plug-in.
(edit) @3026   8 years sacerdot With -a we now produce also the .cerco file required by the plug-in.
(edit) @3025   8 years sacerdot 1. two syntax errors in instrumented files fixed 2. the compiler now …
(edit) @3024   8 years sacerdot Bug fixed: set_flags was ignoring the cy and ov flags.
(edit) @3023   8 years sacerdot Typo fixed. It made all GOTOs jump to random positions in the ASM code.
(edit) @3022   8 years campbell Make a couple of tests monadic for easier inversion.
(edit) @3021   8 years campbell Replace clight_clock_after with a more sensible definition that uses …
(edit) @3020   8 years sacerdot - Options not used removed from the help/interface. - More compliance …
(edit) @3019   8 years sacerdot New extraction after ERTLptr abortion.
(edit) @3018   8 years sacerdot 1) some files repaired 2) all stuff related to the aborted pass …
(edit) @3017   8 years sacerdot Repaired.
(edit) @3016   8 years tranquil fixed after previous commit
(edit) @3015   8 years sacerdot Comment removed
(edit) @3014   8 years tranquil ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
(edit) @3013   8 years sacerdot Temporary parsing files removed.
(edit) @3012   8 years sacerdot Debugging code removed after bug fixing.
(edit) @3011   8 years sacerdot New extraction.
(edit) @3010   8 years tranquil same bug as was in liveness is now fixed
(edit) @3009   8 years sacerdot New extraction.
(edit) @3008   8 years tranquil corrected bug where the address of pointer calls was not defined as used
(edit) @3007   8 years campbell Sketch out how Cminor to RTLabs correctness would fit into the …
(edit) @3006   8 years sacerdot New extraction, bugs fixed.
(edit) @3005   8 years sacerdot Beginning of making it fully compatible with untrusted one.
(edit) @3004   8 years tranquil fixed a bug where when doing an asymetrical op, cast initialization …
(edit) @3003   8 years sacerdot Correctness.ma "repaired"
(edit) @3002   8 years tranquil fixed previous commit
(edit) @3001   8 years sacerdot New extraction.
(edit) @3000   8 years tranquil added RTLabs printer
(edit) @2999   8 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
(edit) @2998   8 years sacerdot Test on conditional execution. Fails atm.
(edit) @2997   8 years sacerdot New extraction.
(edit) @2996   8 years sacerdot Printing of graphs now starts from the entry point.
(edit) @2995   8 years sacerdot The lIN_printer extracted.
(edit) @2994   8 years sacerdot The LIN printer.
(edit) @2993   8 years sacerdot 1. performance improved: the type inference was inferring …
(edit) @2992   8 years campbell Add "only one return" invariant to RTLabs functions.
(edit) @2991   8 years piccolo Fixed cond and seq case in StatusSimulationHelper? Added cost case in …
(edit) @2990   8 years campbell Replace dodgy hypothesis by nice ones, clean up a little.
(edit) @2989   8 years campbell Make front-end measurability preservation proof cope with moving the …
(edit) @2988   8 years sacerdot Some easy tests.
(edit) @2987   8 years sacerdot And again.. :(
(edit) @2986   8 years sacerdot New extraction.
(edit) @2985   8 years sacerdot Order of printing of lines in LIN fixed again, truly this time. But I …
(edit) @2984   8 years tranquil better LINToASM initialization of globals (to be tested!)
(edit) @2983   8 years sacerdot LIN code was printed in reverse order. But I have not really …
(edit) @2982   8 years sacerdot Pretty priting of LIN implemented.
(edit) @2981   8 years sacerdot New extraction after code simplification.
(edit) @2980   8 years tranquil fixed b_graph_translate
(edit) @2979   8 years sacerdot 1. LINToASM: new extraction (fix deletion backtracked) 2. …
(edit) @2978   8 years tranquil merged accidentally backtracked changes
(edit) @2977   8 years sacerdot New extraction after several bug fixes.
(edit) @2976   8 years tranquil * a dangling trivial proof obligation is now closed
(edit) @2975   8 years tranquil * RTL premain fixed * fixed bug in back end ops (subtracting to a …
(edit) @2974   8 years sacerdot New extraction.
(edit) @2973   8 years tranquil semanticUtils adapted to changes in TranslateUtils?
(edit) @2972   8 years campbell Remove init from a testcase.
(edit) @2971   8 years campbell Single RTLabs return statement.
(edit) @2970   8 years tranquil now joint_if_entry can change when a preamble is added, so code points …
(edit) @2969   8 years sacerdot Dead axiom removed :-)
(edit) @2968   8 years sacerdot The initial status memory was not really initialized. Now it is.
(edit) @2967   8 years sacerdot Semantics changed so that a terminating joint program that returns an …
(edit) @2966   8 years sacerdot Modified by hand files (to improve a little bit the performance).
(edit) @2965   8 years sacerdot Code performance improved a bit by hand.
(edit) @2964   8 years sacerdot Debugging code removed.
(edit) @2963   8 years sacerdot Bug fixed: the pre-main for the final code is now COST k1 …
(edit) @2962   8 years sacerdot Most performant algorithm restored.
(edit) @2961   8 years sacerdot Bug fixed (stupid typo in pre-main code made the compiler diverge on …
(edit) @2960   8 years sacerdot New extraction, it diverges in RTL execution now.
(edit) @2959   8 years sacerdot Typo
(edit) @2958   8 years sacerdot Error message implemented.
(edit) @2957   8 years tranquil fixed semantics_blocks
(edit) @2956   8 years tranquil fixed LTL/LIN semantics
(edit) @2955   8 years tranquil corrected stupid typo
(edit) @2954   8 years tranquil resolved circular dependency for ERTLptr's semantics
(edit) @2953   8 years campbell Fix silly label handling bug I realised was there during my talk…
(edit) @2952   8 years tranquil * corrected all back-end premains to not pass any arguments to the …
(edit) @2951   8 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
(edit) @2950   8 years sacerdot linearise repaired (did I do the right thing???)
(edit) @2949   8 years sacerdot Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
(edit) @2948   8 years campbell Finish up measurable to structured proof, exposing the prefix and …
(edit) @2947   8 years campbell Init change in measurable to structured file.
(edit) @2946   8 years tranquil main novelties: * there is an in-built stack_usage nat in joint …
(edit) @2945   8 years campbell Minor tweak.
(edit) @2944   8 years sacerdot Some progress.
(edit) @2943   8 years sacerdot Mauro, I have put a daemon in place of the proof obligation that used …
(edit) @2942   8 years sacerdot Many changes: 1. Coloured graphs are now specified in terms of …
(edit) @2941   8 years campbell Update proof slides.
(edit) @2940   8 years sacerdot 1. StatusSimulationHelper? changed to allow to use status_rel that …
(edit) @2939   8 years sacerdot Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
(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.
Note: See TracRevisionLog for help on using the revision log.