|
|
@3153
|
8 years |
sacerdot |
More data.
|
|
|
@3152
|
8 years |
amadio |
r
|
|
|
@3151
|
8 years |
sacerdot |
More data flowing in.
|
|
|
@3150
|
8 years |
sacerdot |
Integrated all data I received so far.
|
|
|
@3149
|
8 years |
sacerdot |
More data from Roberto integrated.
|
|
|
@3148
|
8 years |
sacerdot |
Infos by Roberto integrated.
|
|
|
@3147
|
8 years |
sacerdot |
More work on Part 4.
|
|
|
@3146
|
8 years |
sacerdot |
Most of the "scientific" work required for Part4.
I still need to …
|
|
|
@3145
|
8 years |
tranquil |
* removed sigma types from traces of intensional events
* completed …
|
|
|
@3144
|
8 years |
sacerdot |
Initial work on D1.3.
Part 1 and Part 2 have been fixed already.
|
|
|
@3143
|
8 years |
sacerdot |
More papers pulled into the report.
|
|
|
@3142
|
8 years |
campbell |
Sketch out a bit more of 3.4.
|
|
|
@3141
|
8 years |
mckinna |
Rephrase Tullio's contribution... more work needed?
|
|
|
@3140
|
8 years |
campbell |
Diagram illustrating nested function calls in structured traces.
|
|
|
@3139
|
8 years |
mckinna |
English tweaks
|
|
|
@3138
|
8 years |
campbell |
Sketch up-to-labelling bit.
|
|
|
@3137
|
8 years |
mckinna |
Tweaks
|
|
|
@3136
|
8 years |
mckinna |
Updates: form and content, incorporating comments from Brian, and from …
|
|
|
@3135
|
8 years |
campbell |
Discussion with Kevin at HiPEAC workshop.
|
|
|
@3134
|
8 years |
mckinna |
Opps uncommitted edits!
|
|
|
@3133
|
8 years |
mckinna |
Underscores!
|
|
|
@3132
|
8 years |
mckinna |
1st version of workshop s reports. Comments/amendments welcome!
|
|
|
@3131
|
8 years |
campbell |
Add rest of correctness.
|
|
|
@3130
|
8 years |
campbell |
Tweak diagram spacing.
|
|
|
@3129
|
8 years |
campbell |
Right version of the diagram.
|
|
|
@3128
|
8 years |
campbell |
Start of D3.4.
(Sorry it's taking longer than anticipated; I blame a …
|
|
|
@3127
|
8 years |
piccolo |
report on general proof
|
|
|
@3126
|
8 years |
sacerdot |
Splitted into empty report + "stand alone" paper.
The paper needs to …
|
|
|
@3125
|
8 years |
sacerdot |
…
|
|
|
@3124
|
8 years |
sacerdot |
…
|
|
|
@3123
|
8 years |
sacerdot |
…
|
|
|
@3122
|
8 years |
sacerdot |
…
|
|
|
@3121
|
8 years |
sacerdot |
…
|
|
|
@3120
|
8 years |
sacerdot |
…
|
|
|
@3119
|
8 years |
sacerdot |
…
|
|
|
@3118
|
8 years |
piccolo |
1) finished return case in StatusSimulationHelper?
2) started to write …
|
|
|
@3117
|
8 years |
sacerdot |
…
|
|
|
@3116
|
8 years |
sacerdot |
…
|
|
|
@3115
|
8 years |
campbell |
Clean up some left-over lemmas and move comment back into place.
|
|
|
@3114
|
8 years |
sacerdot |
Some progress on pipelines/caches.
|
|
|
@3113
|
8 years |
sacerdot |
Some work on control flow analysis.
|
|
|
@3112
|
8 years |
tranquil |
added invariant that costlabels are only assigned to NOPs (not proved …
|
|
|
@3111
|
8 years |
sacerdot |
Skeleton
|
|
|
@3110
|
8 years |
sacerdot |
…
|
|
|
@3109
|
8 years |
sacerdot |
New version.
|
|
|
@3108
|
8 years |
sacerdot |
Towards D5.2.
|
|
|
@3107
|
8 years |
regisgia |
* External tools to compile the plugin.
|
|
|
@3106
|
8 years |
sacerdot |
New extraction.
|
|
|
@3105
|
8 years |
sacerdot |
Pretty printing changed.
There is still an inefficiency left: activate …
|
|
|
@3104
|
8 years |
sacerdot |
Performance improvement.
|
|
|
@3103
|
8 years |
mckinna |
Simplified "include" dependencies
|
|
|
@3102
|
8 years |
mckinna |
Removed redundant refs to current_instruction0,
which itself has been …
|
|
|
@3101
|
8 years |
mckinna |
Removed redundant lemma execute_1_technical,
which is covered by …
|
|
|
@3100
|
8 years |
mckinna |
Removed redundant defn of current_instruction0,
which only appears in …
|
|
|
@3099
|
8 years |
mckinna |
Simplified preliminaries:
inefficient_address_of_word_labels, and …
|
|
|
@3098
|
8 years |
sacerdot |
Performance improvement.
|
|
|
@3097
|
8 years |
sacerdot |
Performance improvement in policy computation.
|
|
|
@3096
|
8 years |
tranquil |
preliminary work on closing correctness.ma
|
|
|
@3095
|
8 years |
sacerdot |
Some performance improvement: an heavy computation was done again and …
|
|
|
@3094
|
8 years |
sacerdot |
Makefile with targets: byte opt clean
|
|
|
@3093
|
8 years |
sacerdot |
Makefile replaces build, targets: byte, opt, clean
|
|
|
@3092
|
8 years |
sacerdot |
No more references to Lustre stuff.
|
|
|
@3091
|
8 years |
sacerdot |
…
|
|
|
@3090
|
8 years |
tassi |
dist: take into account symlink
|
|
|
@3089
|
8 years |
sacerdot |
Symbolic link to the cparser
|
|
|
@3088
|
8 years |
sacerdot |
We now also generate the package for native code.
|
|
|
@3087
|
8 years |
tassi |
script to build tarpall
|
|
|
@3086
|
8 years |
sacerdot |
extracted is now in driver
|
|
|
@3085
|
8 years |
sacerdot |
extracted directory moved into driver to make debian packages more …
|
|
|
@3084
|
8 years |
amadio |
|
|
|
@3083
|
8 years |
sacerdot |
The cost and stack* variables are now initialized with the cost of …
|
|
|
@3082
|
8 years |
mckinna |
Tidying up: the long comment about preamble/renamed_symbols in the …
|
|
|
@3081
|
8 years |
campbell |
Tidy up recent work a little.
|
|
|
@3080
|
8 years |
sacerdot |
New extraction.
|
|
|
@3079
|
8 years |
tranquil |
added printing of ERTL, LTL and LIN's ext_seq's.
|
|
|
@3078
|
8 years |
tranquil |
fixed change of Mov
|
|
|
@3077
|
8 years |
sacerdot |
New extraction.
|
|
|
@3076
|
8 years |
mckinna |
simplified include dependencies
|
|
|
@3075
|
8 years |
mckinna |
Apologies for late folding in of old changes which were left over from …
|
|
|
@3074
|
8 years |
campbell |
Put some kind of high level proof in for front-end.
|
|
|
@3073
|
8 years |
sacerdot |
New extraction, all tests pass.
|
|
|
@3072
|
8 years |
tranquil |
corrected a bug (translate_store was wrong)
|
|
|
@3071
|
8 years |
sacerdot |
…
|
|
|
@3070
|
8 years |
sacerdot |
Ext case of RTL implemented.
|
|
|
@3069
|
8 years |
sacerdot |
New extraction.
|
|
|
@3068
|
8 years |
sacerdot |
Debugging code removed.
|
|
|
@3067
|
8 years |
sacerdot |
New test that fails too.
|
|
|
@3066
|
8 years |
tranquil |
* implemented get_arg_16 for ACC_DPTR
* LINToASM is now agnostic as to …
|
|
|
@3065
|
8 years |
sacerdot |
Efficiency of semantics of assembled improved: ticks_of was …
|
|
|
@3064
|
8 years |
sacerdot |
Efficiency of the semantics of assembly improved by avoiding the …
|
|
|
@3063
|
8 years |
campbell |
Remove measure function from FEMeasurable because we're not using it …
|
|
|
@3062
|
8 years |
sacerdot |
Bug fixed in the semantics of Mov: the offset was ignored.
Now all …
|
|
|
@3061
|
8 years |
sacerdot |
New extraction.
|
|
|
@3060
|
8 years |
sacerdot |
Bug fixed in the semantics of JMP.
The bug was due to a bug in the …
|
|
|
@3059
|
8 years |
sacerdot |
New extraction
|
|
|
@3058
|
8 years |
tranquil |
…
|
|
|
@3057
|
8 years |
tranquil |
lookup of function identifiers was not corrected with sigma
|
|
|
@3056
|
8 years |
tranquil |
fixed a merge gone wrong
|
|
|
@3055
|
8 years |
campbell |
Start getting partial Clight to Cminor proof in shape for …
|
|
|
@3054
|
8 years |
campbell |
Put missing typ check in; adjust proof because I did it a little …
|
|
|