source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3128   9 years campbell Start of D3.4. (Sorry it's taking longer than anticipated; I blame a …
(edit) @3127   9 years piccolo report on general proof
(edit) @3126   9 years sacerdot Splitted into empty report + "stand alone" paper. The paper needs to …
(edit) @3125   9 years sacerdot
(edit) @3124   9 years sacerdot
(edit) @3123   9 years sacerdot
(edit) @3122   9 years sacerdot
(edit) @3121   9 years sacerdot
(edit) @3120   9 years sacerdot
(edit) @3119   9 years sacerdot
(edit) @3118   9 years piccolo 1) finished return case in StatusSimulationHelper? 2) started to write …
(edit) @3117   9 years sacerdot
(edit) @3116   9 years sacerdot
(edit) @3115   9 years campbell Clean up some left-over lemmas and move comment back into place.
(edit) @3114   9 years sacerdot Some progress on pipelines/caches.
(edit) @3113   9 years sacerdot Some work on control flow analysis.
(edit) @3112   9 years tranquil added invariant that costlabels are only assigned to NOPs (not proved …
(edit) @3111   9 years sacerdot Skeleton
(edit) @3110   9 years sacerdot
(edit) @3109   9 years sacerdot New version.
(edit) @3108   9 years sacerdot Towards D5.2.
(edit) @3107   9 years regisgia * External tools to compile the plugin.
(edit) @3106   9 years sacerdot New extraction.
(edit) @3105   9 years sacerdot Pretty printing changed. There is still an inefficiency left: activate …
(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) @3094   9 years sacerdot Makefile with targets: byte opt clean
(edit) @3093   9 years sacerdot Makefile replaces build, targets: byte, opt, clean
(edit) @3092   9 years sacerdot No more references to Lustre stuff.
(edit) @3091   9 years sacerdot
(edit) @3090   9 years tassi dist: take into account symlink
(edit) @3089   9 years sacerdot Symbolic link to the cparser
(edit) @3088   9 years sacerdot We now also generate the package for native code.
(edit) @3087   9 years tassi script to build tarpall
(edit) @3086   9 years sacerdot extracted is now in driver
(edit) @3085   9 years sacerdot extracted directory moved into driver to make debian packages more …
(edit) @3084   9 years amadio
(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) @3080   9 years sacerdot New extraction.
(edit) @3079   9 years tranquil added printing of ERTL, LTL and LIN's ext_seq's.
(edit) @3078   9 years tranquil fixed change of Mov
(edit) @3077   9 years sacerdot New extraction.
(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) @3073   9 years sacerdot New extraction, all tests pass.
(edit) @3072   9 years tranquil corrected a bug (translate_store was wrong)
(edit) @3071   9 years sacerdot
(edit) @3070   9 years sacerdot Ext case of RTL implemented.
(edit) @3069   9 years sacerdot New extraction.
(edit) @3068   9 years sacerdot Debugging code removed.
(edit) @3067   9 years sacerdot New test that fails too.
(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) @3061   9 years sacerdot New extraction.
(edit) @3060   9 years sacerdot Bug fixed in the semantics of JMP. The bug was due to a bug in the …
(edit) @3059   9 years sacerdot New extraction
(edit) @3058   9 years tranquil
(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) @3052   9 years tranquil
(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) @3043   9 years sacerdot New major extraction that should have solved all remaining issues. As …
(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) @3038   9 years sacerdot Bug fixed: the stack_cost* variables must be declared before the …
(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) @3029   9 years sacerdot New extraction after DPH/DPL bug fixing.
Note: See TracRevisionLog for help on using the revision log.