Context Navigation

11:38 PM Changeset [3160] by sacerdot: Initial part and description of WP2, WP3 and WP4 completed. WP5, final …
7:17 PM Changeset [3159] by campbell: A bit more text in 3.4.
7:17 PM Changeset [3158] by campbell: Some text on measurable subtraces throughout the front-end.
6:13 PM Changeset [3157] by mckinna: Added tables with the workshop programmes indetail
3:24 PM Changeset [3156] by campbell: Rebuild prefix traces in back-end's preferred form.
3:24 PM Changeset [3155] by campbell: Now have proof that the initial states are in simulation for clight to …
2:53 PM Changeset [3154] by piccolo: 1) changed block_of_call in order to prevent pre-main calls 2) …

Apr 16, 2013:

5:31 PM Changeset [3153] by sacerdot: More data.
2:46 PM Changeset [3152] by amadio: r
11:33 AM Changeset [3151] by sacerdot: More data flowing in.
11:30 AM Changeset [3150] by sacerdot: Integrated all data I received so far.
11:09 AM Changeset [3149] by sacerdot: More data from Roberto integrated.
11:00 AM Changeset [3148] by sacerdot: Infos by Roberto integrated.

Apr 15, 2013:

6:57 PM Changeset [3147] by sacerdot: More work on Part 4.
6:29 PM Changeset [3146] by sacerdot: Most of the "scientific" work required for Part4. I still need to …
4:31 PM Changeset [3145] by tranquil: * removed sigma types from traces of intensional events * completed …
3:43 PM Changeset [3144] by sacerdot: Initial work on D1.3. Part 1 and Part 2 have been fixed already.
2:27 PM Changeset [3143] by sacerdot: More papers pulled into the report.
10:51 AM Changeset [3142] by campbell: Sketch out a bit more of 3.4.

Apr 12, 2013:

7:23 PM Changeset [3141] by mckinna: Rephrase Tullio's contribution... more work needed?
7:22 PM Changeset [3140] by campbell: Diagram illustrating nested function calls in structured traces.
7:11 PM Changeset [3139] by mckinna: English tweaks
7:03 PM Changeset [3138] by campbell: Sketch up-to-labelling bit.
6:53 PM Changeset [3137] by mckinna: Tweaks
6:47 PM Changeset [3136] by mckinna: Updates: form and content, incorporating comments from Brian, and from …
6:34 PM Changeset [3135] by campbell: Discussion with Kevin at HiPEAC workshop.
6:27 PM Changeset [3134] by mckinna: Opps uncommitted edits!
6:18 PM Changeset [3133] by mckinna: Underscores!
6:17 PM Changeset [3132] by mckinna: 1st version of workshop s reports. Comments/amendments welcome!
6:10 PM Changeset [3131] by campbell: Add rest of correctness.
6:10 PM Changeset [3130] by campbell: Tweak diagram spacing.
6:10 PM Changeset [3129] by campbell: Right version of the diagram.
5:00 PM Changeset [3128] by campbell: Start of D3.4. (Sorry it's taking longer than anticipated; I blame a …
4:03 PM Changeset [3127] by piccolo: report on general proof
1:00 AM Changeset [3126] by sacerdot: Splitted into empty report + "stand alone" paper. The paper needs to …

Apr 11, 2013:

7:10 PM Changeset [3125] by sacerdot: …
6:34 PM Changeset [3124] by sacerdot: …
6:22 PM Changeset [3123] by sacerdot: …
3:55 PM Changeset [3122] by sacerdot: …
3:08 PM Changeset [3121] by sacerdot: …
2:04 PM Changeset [3120] by sacerdot: …

Apr 10, 2013:

7:15 PM Changeset [3119] by sacerdot: …
6:45 PM Changeset [3118] by piccolo: 1) finished return case in StatusSimulationHelper? 2) started to write …
6:25 PM Changeset [3117] by sacerdot: …
5:07 PM Changeset [3116] by sacerdot: …
1:28 PM Changeset [3115] by campbell: Clean up some left-over lemmas and move comment back into place.
9:48 AM Changeset [3114] by sacerdot: Some progress on pipelines/caches.
9:39 AM cost-plug-in-0.2.tgz attached to WikiStart by regisgia: Frama-C (Nitrogen) Cost plugin

Apr 9, 2013:

7:00 PM Changeset [3113] by sacerdot: Some work on control flow analysis.
6:05 PM Changeset [3112] by tranquil: added invariant that costlabels are only assigned to NOPs (not proved …
6:05 PM Changeset [3111] by sacerdot: Skeleton
6:02 PM Changeset [3110] by sacerdot: …
5:28 PM Changeset [3109] by sacerdot: New version.

Apr 8, 2013:

11:50 PM Changeset [3108] by sacerdot: Towards D5.2.
1:17 PM Changeset [3107] by regisgia: * External tools to compile the plugin.

Apr 6, 2013:

7:35 PM Changeset [3106] by sacerdot: New extraction.
6:38 PM Changeset [3105] by sacerdot: Pretty printing changed. There is still an inefficiency left: activate …
6:37 PM Changeset [3104] by sacerdot: Performance improvement.
4:19 PM Changeset [3103] by mckinna: Simplified "include" dependencies
4:11 PM Changeset [3102] by mckinna: Removed redundant refs to current_instruction0, which itself has been …
4:08 PM Changeset [3101] by mckinna: Removed redundant lemma execute_1_technical, which is covered by …
4:05 PM Changeset [3100] by mckinna: Removed redundant defn of current_instruction0, which only appears in …
4:02 PM Changeset [3099] by mckinna: Simplified preliminaries: inefficient_address_of_word_labels, and …
11:44 AM Changeset [3098] by sacerdot: Performance improvement.

Apr 5, 2013:

9:53 PM Changeset [3097] by sacerdot: Performance improvement in policy computation.
6:04 PM Changeset [3096] by tranquil: preliminary work on closing correctness.ma

Apr 4, 2013:

9:53 PM Changeset [3095] by sacerdot: Some performance improvement: an heavy computation was done again and …
12:04 PM Changeset [3094] by sacerdot: Makefile with targets: byte opt clean
11:52 AM Changeset [3093] by sacerdot: Makefile replaces build, targets: byte, opt, clean
11:36 AM Changeset [3092] by sacerdot: No more references to Lustre stuff.
11:31 AM Changeset [3091] by sacerdot: …
11:26 AM Changeset [3090] by tassi: dist: take into account symlink
11:18 AM Changeset [3089] by sacerdot: Symbolic link to the cparser
11:16 AM Changeset [3088] by sacerdot: We now also generate the package for native code.
11:06 AM Changeset [3087] by tassi: script to build tarpall
10:53 AM Changeset [3086] by sacerdot: extracted is now in driver
10:46 AM Changeset [3085] by sacerdot: extracted directory moved into driver to make debian packages more …
10:19 AM Changeset [3084] by amadio
9:58 AM Changeset [3083] by sacerdot: The cost and stack* variables are now initialized with the cost of …
9:31 AM Changeset [3082] by mckinna: Tidying up: the long comment about preamble/renamed_symbols in the …

Apr 3, 2013:

5:54 PM Changeset [3081] by campbell: Tidy up recent work a little.
5:27 PM Changeset [3080] by sacerdot: New extraction.
5:03 PM Changeset [3079] by tranquil: added printing of ERTL, LTL and LIN's ext_seq's.
3:01 PM Changeset [3078] by tranquil: fixed change of Mov
11:49 AM Changeset [3077] by sacerdot: New extraction.
10:13 AM Changeset [3076] by mckinna: simplified include dependencies

Apr 2, 2013:

7:59 PM Changeset [3075] by mckinna: Apologies for late folding in of old changes which were left over from …
7:25 PM Changeset [3074] by campbell: Put some kind of high level proof in for front-end.
6:44 PM Changeset [3073] by sacerdot: New extraction, all tests pass.
6:39 PM Changeset [3072] by tranquil: corrected a bug (translate_store was wrong)
4:49 PM Changeset [3071] by sacerdot: …
4:49 PM Changeset [3070] by sacerdot: Ext case of RTL implemented.
2:09 PM Changeset [3069] by sacerdot: New extraction.
1:51 PM Changeset [3068] by sacerdot: Debugging code removed.
1:49 PM Changeset [3067] by sacerdot: New test that fails too.
1:48 PM Changeset [3066] by tranquil: * implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
1:37 PM Changeset [3065] by sacerdot: Efficiency of semantics of assembled improved: ticks_of was …
1:02 PM Changeset [3064] by sacerdot: Efficiency of the semantics of assembly improved by avoiding the …
12:16 PM Changeset [3063] by campbell: Remove measure function from FEMeasurable because we're not using it …
11:59 AM Changeset [3062] by sacerdot: Bug fixed in the semantics of Mov: the offset was ignored. Now all …
11:32 AM Changeset [3061] by sacerdot: New extraction.
11:11 AM Changeset [3060] by sacerdot: Bug fixed in the semantics of JMP. The bug was due to a bug in the …
1:25 AM Changeset [3059] by sacerdot: New extraction

Apr 1, 2013:

9:14 PM Changeset [3058] by tranquil: …
9:14 PM Changeset [3057] by tranquil: lookup of function identifiers was not corrected with sigma
7:17 PM Changeset [3056] by tranquil: fixed a merge gone wrong
7:04 PM Changeset [3055] by campbell: Start getting partial Clight to Cminor proof in shape for …
7:04 PM Changeset [3054] by campbell: Put missing typ check in; adjust proof because I did it a little …
7:04 PM Changeset [3053] by campbell: Cast simplification preserves measurable subtraces.
6:31 PM Changeset [3052] by tranquil: …
6:28 PM Changeset [3051] by tranquil: fixed order of global initialization in LINToASM. For the moment …
5:18 PM Changeset [3050] by piccolo: 1) Added general commutation theorem for monads. 2) Added some …
12:06 AM Changeset [3049] by campbell: Globalenvs and initial states for cast simplification.
12:06 AM Changeset [3048] by campbell: Improve dependency for cast simplification.

Mar 31, 2013:

10:01 PM Changeset [3047] by campbell: Switch removal and labelling combined.

Note: See TracTimeline for information about the timeline view.

Download in other formats:

RSS Feed