source:

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3153   7 years sacerdot More data.
(edit) @3152   7 years amadio r
(edit) @3151   7 years sacerdot More data flowing in.
(edit) @3150   7 years sacerdot Integrated all data I received so far.
(edit) @3149   7 years sacerdot More data from Roberto integrated.
(edit) @3148   7 years sacerdot Infos by Roberto integrated.
(edit) @3147   7 years sacerdot More work on Part 4.
(edit) @3146   7 years sacerdot Most of the "scientific" work required for Part4. I still need to …
(edit) @3145   7 years tranquil * removed sigma types from traces of intensional events * completed …
(edit) @3144   7 years sacerdot Initial work on D1.3. Part 1 and Part 2 have been fixed already.
(edit) @3143   7 years sacerdot More papers pulled into the report.
(edit) @3142   7 years campbell Sketch out a bit more of 3.4.
(edit) @3141   7 years mckinna Rephrase Tullio's contribution... more work needed?
(edit) @3140   7 years campbell Diagram illustrating nested function calls in structured traces.
(edit) @3139   7 years mckinna English tweaks
(edit) @3138   7 years campbell Sketch up-to-labelling bit.
(edit) @3137   7 years mckinna Tweaks
(edit) @3136   7 years mckinna Updates: form and content, incorporating comments from Brian, and from …
(edit) @3135   7 years campbell Discussion with Kevin at HiPEAC workshop.
(edit) @3134   7 years mckinna Opps uncommitted edits!
(edit) @3133   7 years mckinna Underscores!
(edit) @3132   7 years mckinna 1st version of workshop s reports. Comments/amendments welcome!
(edit) @3131   7 years campbell Add rest of correctness.
(edit) @3130   7 years campbell Tweak diagram spacing.
(edit) @3129   7 years campbell Right version of the diagram.
(edit) @3128   7 years campbell Start of D3.4. (Sorry it's taking longer than anticipated; I blame a …
(edit) @3127   7 years piccolo report on general proof
(edit) @3126   7 years sacerdot Splitted into empty report + "stand alone" paper. The paper needs to …
(edit) @3125   7 years sacerdot …
(edit) @3124   7 years sacerdot …
(edit) @3123   7 years sacerdot …
(edit) @3122   7 years sacerdot …
(edit) @3121   7 years sacerdot …
(edit) @3120   7 years sacerdot …
(edit) @3119   7 years sacerdot …
(edit) @3118   7 years piccolo 1) finished return case in StatusSimulationHelper? 2) started to write …
(edit) @3117   7 years sacerdot …
(edit) @3116   7 years sacerdot …
(edit) @3115   7 years campbell Clean up some left-over lemmas and move comment back into place.
(edit) @3114   7 years sacerdot Some progress on pipelines/caches.
(edit) @3113   7 years sacerdot Some work on control flow analysis.
(edit) @3112   7 years tranquil added invariant that costlabels are only assigned to NOPs (not proved …
(edit) @3111   7 years sacerdot Skeleton
(edit) @3110   7 years sacerdot …
(edit) @3109   7 years sacerdot New version.
(edit) @3108   7 years sacerdot Towards D5.2.
(edit) @3107   7 years regisgia * External tools to compile the plugin.
(edit) @3106   7 years sacerdot New extraction.
(edit) @3105   7 years sacerdot Pretty printing changed. There is still an inefficiency left: activate …
(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) @3094   7 years sacerdot Makefile with targets: byte opt clean
(edit) @3093   7 years sacerdot Makefile replaces build, targets: byte, opt, clean
(edit) @3092   7 years sacerdot No more references to Lustre stuff.
(edit) @3091   7 years sacerdot …
(edit) @3090   7 years tassi dist: take into account symlink
(edit) @3089   7 years sacerdot Symbolic link to the cparser
(edit) @3088   7 years sacerdot We now also generate the package for native code.
(edit) @3087   7 years tassi script to build tarpall
(edit) @3086   7 years sacerdot extracted is now in driver
(edit) @3085   7 years sacerdot extracted directory moved into driver to make debian packages more …
(edit) @3084   7 years amadio
(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) @3080   7 years sacerdot New extraction.
(edit) @3079   7 years tranquil added printing of ERTL, LTL and LIN's ext_seq's.
(edit) @3078   7 years tranquil fixed change of Mov
(edit) @3077   7 years sacerdot New extraction.
(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) @3073   7 years sacerdot New extraction, all tests pass.
(edit) @3072   7 years tranquil corrected a bug (translate_store was wrong)
(edit) @3071   7 years sacerdot …
(edit) @3070   7 years sacerdot Ext case of RTL implemented.
(edit) @3069   7 years sacerdot New extraction.
(edit) @3068   7 years sacerdot Debugging code removed.
(edit) @3067   7 years sacerdot New test that fails too.
(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) @3061   7 years sacerdot New extraction.
(edit) @3060   7 years sacerdot Bug fixed in the semantics of JMP. The bug was due to a bug in the …
(edit) @3059   7 years sacerdot New extraction
(edit) @3058   7 years tranquil …
(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 …
Note: See TracRevisionLog for help on using the revision log.