source: src

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3053   7 years campbell Cast simplification preserves measurable subtraces.
(edit) @3051   7 years tranquil fixed order of global initialization in LINToASM. For the moment …
(edit) @3050   7 years piccolo 1) Added general commutation theorem for monads. 2) Added some …
(edit) @3049   7 years campbell Globalenvs and initial states for cast simplification.
(edit) @3048   7 years campbell Improve dependency for cast simplification.
(edit) @3047   7 years campbell Switch removal and labelling combined.
(edit) @3046   7 years campbell Main part of combined switch removal and labelling proof.
(edit) @3045   7 years tranquil fixed what made test3 fail. However it involves a different notion of …
(edit) @3044   7 years campbell Start showing combination of switch removal and labelling is OK. Fix …
(edit) @3042   7 years sacerdot Repaired.
(edit) @3041   7 years sacerdot Repaired
(edit) @3040   7 years tranquil fixed LINToASM
(edit) @3039   7 years tranquil * merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
(edit) @3037   7 years tranquil * ADDRESS joint instruction now has also an offset * corrected call to …
(edit) @3036   7 years garnier Fixing some problems, progress, etc
(edit) @3035   7 years mckinna Tweak: tidied up ?/\ldots Conceptual: better monadic threading of …
(edit) @3034   7 years sacerdot Bug fixed: COST instructions are now assembled as NOP to prevent the …
(edit) @3033   7 years sacerdot Bug fixed: sign_extension was extending according to the _second_ bit, …
(edit) @3032   7 years campbell Remind myself why ms_rel_normal is reasonable.
(edit) @3031   7 years campbell Tidy up RTLabs preclassified_system definitions.
(edit) @3030   7 years campbell Break up front-end for correctness proof. Use let rec to prevent …
(edit) @3028   7 years sacerdot Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
(edit) @3024   7 years sacerdot Bug fixed: set_flags was ignoring the cy and ov flags.
(edit) @3023   7 years sacerdot Typo fixed. It made all GOTOs jump to random positions in the ASM code.
(edit) @3022   7 years campbell Make a couple of tests monadic for easier inversion.
(edit) @3021   7 years campbell Replace clight_clock_after with a more sensible definition that uses …
(edit) @3018   7 years sacerdot 1) some files repaired 2) all stuff related to the aborted pass …
(edit) @3017   7 years sacerdot Repaired.
(edit) @3016   7 years tranquil fixed after previous commit
(edit) @3014   7 years tranquil ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
(edit) @3010   7 years tranquil same bug as was in liveness is now fixed
(edit) @3008   7 years tranquil corrected bug where the address of pointer calls was not defined as used
(edit) @3007   7 years campbell Sketch out how Cminor to RTLabs correctness would fit into the …
(edit) @3004   7 years tranquil fixed a bug where when doing an asymetrical op, cast initialization …
(edit) @3003   7 years sacerdot Correctness.ma "repaired"
(edit) @2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
(edit) @2996   7 years sacerdot Printing of graphs now starts from the entry point.
(edit) @2994   7 years sacerdot The LIN printer.
(edit) @2993   7 years sacerdot 1. performance improved: the type inference was inferring …
(edit) @2992   7 years campbell Add "only one return" invariant to RTLabs functions.
(edit) @2991   7 years piccolo Fixed cond and seq case in StatusSimulationHelper? Added cost case in …
(edit) @2990   7 years campbell Replace dodgy hypothesis by nice ones, clean up a little.
(edit) @2989   7 years campbell Make front-end measurability preservation proof cope with moving the …
(edit) @2985   7 years sacerdot Order of printing of lines in LIN fixed again, truly this time. But I …
(edit) @2984   7 years tranquil better LINToASM initialization of globals (to be tested!)
(edit) @2983   7 years sacerdot LIN code was printed in reverse order. But I have not really …
(edit) @2982   7 years sacerdot Pretty priting of LIN implemented.
(edit) @2980   7 years tranquil fixed b_graph_translate
(edit) @2978   7 years tranquil merged accidentally backtracked changes
(edit) @2976   7 years tranquil * a dangling trivial proof obligation is now closed
(edit) @2975   7 years tranquil * RTL premain fixed * fixed bug in back end ops (subtracting to a …
(edit) @2973   7 years tranquil semanticUtils adapted to changes in TranslateUtils?
(edit) @2972   7 years campbell Remove init from a testcase.
(edit) @2971   7 years campbell Single RTLabs return statement.
(edit) @2970   7 years tranquil now joint_if_entry can change when a preamble is added, so code points …
(edit) @2969   7 years sacerdot Dead axiom removed :-)
(edit) @2968   7 years sacerdot The initial status memory was not really initialized. Now it is.
(edit) @2967   7 years sacerdot Semantics changed so that a terminating joint program that returns an …
(edit) @2963   7 years sacerdot Bug fixed: the pre-main for the final code is now COST k1 …
(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) @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) @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) @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) @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) @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) @2912   7 years sacerdot Ouch, another bug in the very same function. Fixed too, on an example …
Note: See TracRevisionLog for help on using the revision log.