source: src

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3115   9 years campbell Clean up some left-over lemmas and move comment back into place.
(edit) @3112   9 years tranquil added invariant that costlabels are only assigned to NOPs (not proved …
(edit) @3104   9 years sacerdot Performance improvement.
(edit) @3103   9 years mckinna Simplified "include" dependencies
(edit) @3102   9 years mckinna Removed redundant refs to current_instruction0, which itself has been …
(edit) @3101   9 years mckinna Removed redundant lemma execute_1_technical, which is covered by …
(edit) @3100   9 years mckinna Removed redundant defn of current_instruction0, which only appears in …
(edit) @3099   9 years mckinna Simplified preliminaries: inefficient_address_of_word_labels, and …
(edit) @3098   9 years sacerdot Performance improvement.
(edit) @3097   9 years sacerdot Performance improvement in policy computation.
(edit) @3096   9 years tranquil preliminary work on closing correctness.ma
(edit) @3095   9 years sacerdot Some performance improvement: an heavy computation was done again and …
(edit) @3083   9 years sacerdot The cost and stack* variables are now initialized with the cost of …
(edit) @3082   9 years mckinna Tidying up: the long comment about preamble/renamed_symbols in the …
(edit) @3081   9 years campbell Tidy up recent work a little.
(edit) @3078   9 years tranquil fixed change of Mov
(edit) @3076   9 years mckinna simplified include dependencies
(edit) @3075   9 years mckinna Apologies for late folding in of old changes which were left over from …
(edit) @3074   9 years campbell Put some kind of high level proof in for front-end.
(edit) @3072   9 years tranquil corrected a bug (translate_store was wrong)
(edit) @3066   9 years tranquil * implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
(edit) @3065   9 years sacerdot Efficiency of semantics of assembled improved: ticks_of was …
(edit) @3064   9 years sacerdot Efficiency of the semantics of assembly improved by avoiding the …
(edit) @3063   9 years campbell Remove measure function from FEMeasurable because we're not using it …
(edit) @3062   9 years sacerdot Bug fixed in the semantics of Mov: the offset was ignored. Now all …
(edit) @3060   9 years sacerdot Bug fixed in the semantics of JMP. The bug was due to a bug in the …
(edit) @3057   9 years tranquil lookup of function identifiers was not corrected with sigma
(edit) @3056   9 years tranquil fixed a merge gone wrong
(edit) @3055   9 years campbell Start getting partial Clight to Cminor proof in shape for …
(edit) @3054   9 years campbell Put missing typ check in; adjust proof because I did it a little …
(edit) @3053   9 years campbell Cast simplification preserves measurable subtraces.
(edit) @3051   9 years tranquil fixed order of global initialization in LINToASM. For the moment …
(edit) @3050   9 years piccolo 1) Added general commutation theorem for monads. 2) Added some …
(edit) @3049   9 years campbell Globalenvs and initial states for cast simplification.
(edit) @3048   9 years campbell Improve dependency for cast simplification.
(edit) @3047   9 years campbell Switch removal and labelling combined.
(edit) @3046   9 years campbell Main part of combined switch removal and labelling proof.
(edit) @3045   9 years tranquil fixed what made test3 fail. However it involves a different notion of …
(edit) @3044   9 years campbell Start showing combination of switch removal and labelling is OK. Fix …
(edit) @3042   9 years sacerdot Repaired.
(edit) @3041   9 years sacerdot Repaired
(edit) @3040   9 years tranquil fixed LINToASM
(edit) @3039   9 years tranquil * merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
(edit) @3037   9 years tranquil * ADDRESS joint instruction now has also an offset * corrected call to …
(edit) @3036   9 years garnier Fixing some problems, progress, etc
(edit) @3035   9 years mckinna Tweak: tidied up ?/\ldots Conceptual: better monadic threading of …
(edit) @3034   9 years sacerdot Bug fixed: COST instructions are now assembled as NOP to prevent the …
(edit) @3033   9 years sacerdot Bug fixed: sign_extension was extending according to the _second_ bit, …
(edit) @3032   9 years campbell Remind myself why ms_rel_normal is reasonable.
(edit) @3031   9 years campbell Tidy up RTLabs preclassified_system definitions.
(edit) @3030   9 years campbell Break up front-end for correctness proof. Use let rec to prevent …
(edit) @3028   9 years sacerdot Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
(edit) @3024   9 years sacerdot Bug fixed: set_flags was ignoring the cy and ov flags.
(edit) @3023   9 years sacerdot Typo fixed. It made all GOTOs jump to random positions in the ASM code.
(edit) @3022   9 years campbell Make a couple of tests monadic for easier inversion.
(edit) @3021   9 years campbell Replace clight_clock_after with a more sensible definition that uses …
(edit) @3018   9 years sacerdot 1) some files repaired 2) all stuff related to the aborted pass …
(edit) @3017   9 years sacerdot Repaired.
(edit) @3016   9 years tranquil fixed after previous commit
(edit) @3014   9 years tranquil ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
(edit) @3010   9 years tranquil same bug as was in liveness is now fixed
(edit) @3008   9 years tranquil corrected bug where the address of pointer calls was not defined as used
(edit) @3007   9 years campbell Sketch out how Cminor to RTLabs correctness would fit into the …
(edit) @3004   9 years tranquil fixed a bug where when doing an asymetrical op, cast initialization …
(edit) @3003   9 years sacerdot Correctness.ma "repaired"
(edit) @2999   9 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
(edit) @2996   9 years sacerdot Printing of graphs now starts from the entry point.
(edit) @2994   9 years sacerdot The LIN printer.
(edit) @2993   9 years sacerdot 1. performance improved: the type inference was inferring …
(edit) @2992   9 years campbell Add "only one return" invariant to RTLabs functions.
(edit) @2991   9 years piccolo Fixed cond and seq case in StatusSimulationHelper? Added cost case in …
(edit) @2990   9 years campbell Replace dodgy hypothesis by nice ones, clean up a little.
(edit) @2989   9 years campbell Make front-end measurability preservation proof cope with moving the …
(edit) @2985   9 years sacerdot Order of printing of lines in LIN fixed again, truly this time. But I …
(edit) @2984   9 years tranquil better LINToASM initialization of globals (to be tested!)
(edit) @2983   9 years sacerdot LIN code was printed in reverse order. But I have not really …
(edit) @2982   9 years sacerdot Pretty priting of LIN implemented.
(edit) @2980   9 years tranquil fixed b_graph_translate
(edit) @2978   9 years tranquil merged accidentally backtracked changes
(edit) @2976   9 years tranquil * a dangling trivial proof obligation is now closed
(edit) @2975   9 years tranquil * RTL premain fixed * fixed bug in back end ops (subtracting to a …
(edit) @2973   9 years tranquil semanticUtils adapted to changes in TranslateUtils?
(edit) @2972   9 years campbell Remove init from a testcase.
(edit) @2971   9 years campbell Single RTLabs return statement.
(edit) @2970   9 years tranquil now joint_if_entry can change when a preamble is added, so code points …
(edit) @2969   9 years sacerdot Dead axiom removed :-)
(edit) @2968   9 years sacerdot The initial status memory was not really initialized. Now it is.
(edit) @2967   9 years sacerdot Semantics changed so that a terminating joint program that returns an …
(edit) @2963   9 years sacerdot Bug fixed: the pre-main for the final code is now COST k1 …
(edit) @2959   9 years sacerdot Typo
(edit) @2958   9 years sacerdot Error message implemented.
(edit) @2957   9 years tranquil fixed semantics_blocks
(edit) @2956   9 years tranquil fixed LTL/LIN semantics
(edit) @2955   9 years tranquil corrected stupid typo
(edit) @2954   9 years tranquil resolved circular dependency for ERTLptr's semantics
(edit) @2953   9 years campbell Fix silly label handling bug I realised was there during my talk…
(edit) @2952   9 years tranquil * corrected all back-end premains to not pass any arguments to the …
(edit) @2950   9 years sacerdot linearise repaired (did I do the right thing???)
(edit) @2949   9 years sacerdot Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
(edit) @2948   9 years campbell Finish up measurable to structured proof, exposing the prefix and …
Note: See TracRevisionLog for help on using the revision log.