source: src

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3466   6 years asperti Removed function that is only in the standard library. Maaaany more to …
(edit) @3415   6 years boender - changes for proceedings of TACAS 2014
(edit) @3395   6 years fguidi scan for redundant includes with new version of matitadep
(edit) @3393   6 years boender - TACAS stuff
(edit) @3392   6 years boender - renamed paper yet again
(edit) @3388   6 years piccolo partial commit
(edit) @3372   7 years piccolo Added new implementation of labelling approach based on LTS and …
(edit) @3371   7 years piccolo Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …
(edit) @3370   7 years sacerdot Submitted.
(edit) @3365   7 years boender - changed spelling error
(edit) @3364   7 years boender - added bit to the introduction about contribution
(edit) @3363   7 years boender - renamed directory
(edit) @3362   7 years boender - added some bits as per Claudio's mail - rewrote some small things - …
(edit) @3361   7 years sacerdot 15 pages version
(edit) @3354   7 years boender - one more
(edit) @3353   7 years boender - addressed minor corrections by referees
(edit) @3352   7 years boender - nicified formulas
(edit) @3342   7 years boender - completed reworking of proofs
(edit) @3341   7 years boender - more notation stuff (still needs work!)
(edit) @3338   7 years boender - updated statement of main correctness statement (still needs work)
(edit) @3304   7 years boender - added 2012 reviews - updated affiliation
(edit) @3265   7 years tranquil added validate_pointer filter in Interference added that intereference …
(edit) @3263   7 years tranquil moved callee saved saving and restoring to ERTL -> LTL pass (untrusted …
(edit) @3262   7 years piccolo reverted status_simulation_utils
(edit) @3261   7 years piccolo reverted joint_semantics rtl_semantics and ltl_semantics
(edit) @3259   7 years piccolo changed ERTL semantics: 1) added manipulation of stack pointer …
(edit) @3257   7 years tranquil fixed uses in ERTL
(edit) @3256   7 years tranquil fixed compilation
(edit) @3255   7 years tranquil * dropped newframe and delframe (to be integrated in calls and returns …
(edit) @3254   7 years sacerdot Code I always forgot to commit. To be ported to ERTLtoLTLProof.ma.
(edit) @3253   7 years piccolo some proof obbligation closed of ERTL to LTL proof
(edit) @3252   7 years piccolo proof obbligation added on ERTL to LTL proof
(edit) @3237   7 years campbell Some incomplete work on Clight -> Cminor call steps.
(edit) @3217   7 years piccolo Correctness of ERTL to LTL in place
(edit) @3178   7 years campbell Some progress on Callstate steps in Clight to Cminor. Note that some …
(edit) @3176   7 years mckinna simplified dependencies
(edit) @3171   7 years mckinna removed redundant dependencies
(edit) @3170   7 years mckinna removed redundant dependencies
(edit) @3165   7 years campbell A little bit of progress on Callstate case.
(edit) @3156   7 years campbell Rebuild prefix traces in back-end's preferred form.
(edit) @3155   7 years campbell Now have proof that the initial states are in simulation for clight to …
(edit) @3154   7 years piccolo 1) changed block_of_call in order to prevent pre-main calls 2) …
(edit) @3145   7 years tranquil * removed sigma types from traces of intensional events * completed …
(edit) @3118   7 years piccolo 1) finished return case in StatusSimulationHelper? 2) started to write …
(edit) @3115   7 years campbell Clean up some left-over lemmas and move comment back into place.
(edit) @3112   7 years tranquil added invariant that costlabels are only assigned to NOPs (not proved …
(edit) @3104   7 years sacerdot Performance improvement.
(edit) @3103   7 years mckinna Simplified "include" dependencies
(edit) @3102   7 years mckinna Removed redundant refs to current_instruction0, which itself has been …
(edit) @3101   7 years mckinna Removed redundant lemma execute_1_technical, which is covered by …
(edit) @3100   7 years mckinna Removed redundant defn of current_instruction0, which only appears in …
(edit) @3099   7 years mckinna Simplified preliminaries: inefficient_address_of_word_labels, and …
(edit) @3098   7 years sacerdot Performance improvement.
(edit) @3097   7 years sacerdot Performance improvement in policy computation.
(edit) @3096   7 years tranquil preliminary work on closing correctness.ma
(edit) @3095   7 years sacerdot Some performance improvement: an heavy computation was done again and …
(edit) @3083   7 years sacerdot The cost and stack* variables are now initialized with the cost of …
(edit) @3082   7 years mckinna Tidying up: the long comment about preamble/renamed_symbols in the …
(edit) @3081   7 years campbell Tidy up recent work a little.
(edit) @3078   7 years tranquil fixed change of Mov
(edit) @3076   7 years mckinna simplified include dependencies
(edit) @3075   7 years mckinna Apologies for late folding in of old changes which were left over from …
(edit) @3074   7 years campbell Put some kind of high level proof in for front-end.
(edit) @3072   7 years tranquil corrected a bug (translate_store was wrong)
(edit) @3066   7 years tranquil * implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
(edit) @3065   7 years sacerdot Efficiency of semantics of assembled improved: ticks_of was …
(edit) @3064   7 years sacerdot Efficiency of the semantics of assembly improved by avoiding the …
(edit) @3063   7 years campbell Remove measure function from FEMeasurable because we're not using it …
(edit) @3062   7 years sacerdot Bug fixed in the semantics of Mov: the offset was ignored. Now all …
(edit) @3060   7 years sacerdot Bug fixed in the semantics of JMP. The bug was due to a bug in the …
(edit) @3057   7 years tranquil lookup of function identifiers was not corrected with sigma
(edit) @3056   7 years tranquil fixed a merge gone wrong
(edit) @3055   7 years campbell Start getting partial Clight to Cminor proof in shape for …
(edit) @3054   7 years campbell Put missing typ check in; adjust proof because I did it a little …
(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 …
Note: See TracRevisionLog for help on using the revision log.