|
|
@2989
|
8 years |
campbell |
Make front-end measurability preservation proof cope with moving the …
|
|
|
@2988
|
8 years |
sacerdot |
Some easy tests.
|
|
|
@2987
|
8 years |
sacerdot |
And again.. :(
|
|
|
@2986
|
8 years |
sacerdot |
New extraction.
|
|
|
@2985
|
8 years |
sacerdot |
Order of printing of lines in LIN fixed again, truly this time. But I …
|
|
|
@2984
|
8 years |
tranquil |
better LINToASM initialization of globals (to be tested!)
|
|
|
@2983
|
8 years |
sacerdot |
LIN code was printed in reverse order. But I have not really …
|
|
|
@2982
|
8 years |
sacerdot |
Pretty priting of LIN implemented.
|
|
|
@2981
|
8 years |
sacerdot |
New extraction after code simplification.
|
|
|
@2980
|
8 years |
tranquil |
fixed b_graph_translate
|
|
|
@2979
|
8 years |
sacerdot |
1. LINToASM: new extraction (fix deletion backtracked)
2. …
|
|
|
@2978
|
8 years |
tranquil |
merged accidentally backtracked changes
|
|
|
@2977
|
8 years |
sacerdot |
New extraction after several bug fixes.
|
|
|
@2976
|
8 years |
tranquil |
* a dangling trivial proof obligation is now closed
|
|
|
@2975
|
8 years |
tranquil |
* RTL premain fixed
* fixed bug in back end ops (subtracting to a …
|
|
|
@2974
|
8 years |
sacerdot |
New extraction.
|
|
|
@2973
|
8 years |
tranquil |
semanticUtils adapted to changes in TranslateUtils?
|
|
|
@2972
|
8 years |
campbell |
Remove init from a testcase.
|
|
|
@2971
|
8 years |
campbell |
Single RTLabs return statement.
|
|
|
@2970
|
8 years |
tranquil |
now joint_if_entry can change when a preamble is added, so code points …
|
|
|
@2969
|
8 years |
sacerdot |
Dead axiom removed :-)
|
|
|
@2968
|
8 years |
sacerdot |
The initial status memory was not really initialized. Now it is.
|
|
|
@2967
|
8 years |
sacerdot |
Semantics changed so that a terminating joint program that returns an …
|
|
|
@2966
|
8 years |
sacerdot |
Modified by hand files (to improve a little bit the performance).
|
|
|
@2965
|
8 years |
sacerdot |
Code performance improved a bit by hand.
|
|
|
@2964
|
8 years |
sacerdot |
Debugging code removed.
|
|
|
@2963
|
8 years |
sacerdot |
Bug fixed: the pre-main for the final code is now
COST k1
…
|
|
|
@2962
|
8 years |
sacerdot |
Most performant algorithm restored.
|
|
|
@2961
|
8 years |
sacerdot |
Bug fixed (stupid typo in pre-main code made the compiler diverge on …
|
|
|
@2960
|
8 years |
sacerdot |
New extraction, it diverges in RTL execution now.
|
|
|
@2959
|
8 years |
sacerdot |
Typo
|
|
|
@2958
|
8 years |
sacerdot |
Error message implemented.
|
|
|
@2957
|
8 years |
tranquil |
fixed semantics_blocks
|
|
|
@2956
|
8 years |
tranquil |
fixed LTL/LIN semantics
|
|
|
@2955
|
8 years |
tranquil |
corrected stupid typo
|
|
|
@2954
|
8 years |
tranquil |
resolved circular dependency for ERTLptr's semantics
|
|
|
@2953
|
8 years |
campbell |
Fix silly label handling bug I realised was there during my talk…
|
|
|
@2952
|
8 years |
tranquil |
* corrected all back-end premains to not pass any arguments to the …
|
|
|
@2951
|
8 years |
sacerdot |
New extraction. Novely: a pre-main is used in the back-end. …
|
|
|
@2950
|
8 years |
sacerdot |
linearise repaired (did I do the right thing???)
|
|
|
@2949
|
8 years |
sacerdot |
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
|
|
|
@2948
|
8 years |
campbell |
Finish up measurable to structured proof, exposing the prefix and …
|
|
|
@2947
|
8 years |
campbell |
Init change in measurable to structured file.
|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
@2945
|
8 years |
campbell |
Minor tweak.
|
|
|
@2944
|
8 years |
sacerdot |
Some progress.
|
|
|
@2943
|
8 years |
sacerdot |
Mauro, I have put a daemon in place of the proof obligation that used …
|
|
|
@2942
|
8 years |
sacerdot |
Many changes:
1. Coloured graphs are now specified in terms of …
|
|
|
@2941
|
8 years |
campbell |
Update proof slides.
|
|
|
@2940
|
8 years |
sacerdot |
1. StatusSimulationHelper? changed to allow to use status_rel that …
|
|
|
@2939
|
8 years |
sacerdot |
Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
|
|
|
@2938
|
8 years |
sacerdot |
1. proof of "all eliminable are eliminable" completed
2. the notion of …
|
|
|
@2937
|
8 years |
campbell |
Speed up checking of RTLabs/CostInj.ma.
|
|
|
@2936
|
8 years |
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
|
@2935
|
8 years |
tranquil |
separation of RTL semantics in three different versions, and …
|
|
|
@2934
|
8 years |
sacerdot |
Patch to obtain more easily comparable traces.
|
|
|
@2933
|
8 years |
sacerdot |
New extraction, several bug fixed. RTL_semantics fixed by hand, will …
|
|
|
@2932
|
8 years |
sacerdot |
Same comment as previous commit on this file: the previous commit was …
|
|
|
@2931
|
8 years |
sacerdot |
Partial back-track from Paolo's commit, that was partial.
|
|
|
@2930
|
8 years |
sacerdot |
More progress. Some useless parameters have been removed from the …
|
|
|
@2929
|
8 years |
sacerdot |
Bug fixed: the coercion mechanism made you think that the CALL case …
|
|
|
@2928
|
8 years |
tranquil |
some sketches about correctness proof
|
|
|
@2927
|
8 years |
tranquil |
stupid bug in bool_of_beval
|
|
|
@2926
|
8 years |
tranquil |
corrected bug in executing Sub
|
|
|
@2925
|
8 years |
tranquil |
corrected bug in toggle_bool
|
|
|
@2924
|
8 years |
campbell |
Make calls to a known identifier actually use a direct call.
|
|
|
@2923
|
8 years |
campbell |
Remove some leftovers.
|
|
|
@2922
|
8 years |
sacerdot |
Progress: proof of "eliminable statements can be eliminated" almost …
|
|
|
@2921
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2920
|
8 years |
sacerdot |
dos2unix-ed
|
|
|
@2919
|
8 years |
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
|
@2918
|
8 years |
tranquil |
erased stupid accidental paste at the start of file (happened when …
|
|
|
@2917
|
8 years |
tranquil |
made it so that a 0 offset does not generate adding ops when accessing …
|
|
|
@2916
|
8 years |
tranquil |
corrected yet another endianness bug in load and store
|
|
|
@2915
|
8 years |
sacerdot |
Dead code removed.
|
|
|
@2914
|
8 years |
campbell |
Use single definition for stack measurement.
|
|
|
@2913
|
8 years |
sacerdot |
Bug corrected by hand. It will be corrected automatically by next …
|
|
|
@2912
|
8 years |
sacerdot |
Ouch, another bug in the very same function.
Fixed too, on an example …
|
|
|
@2911
|
8 years |
sacerdot |
Bug fixed in the translation of casts.
|
|
|
@2910
|
8 years |
sacerdot |
Abstract statuses for ASM and OC completed.
A simple test program can …
|
|
|
@2909
|
8 years |
sacerdot |
New extraction.
|
|
|
@2908
|
8 years |
sacerdot |
Bug fixed by hand, they will be fixed automatically by the new extraction.
|
|
|
@2907
|
8 years |
sacerdot |
1. a few bugs fixed
2. as_return implemented for ASM & OC
|
|
|
@2906
|
8 years |
sacerdot |
Bug fixed.
|
|
|
@2905
|
8 years |
sacerdot |
Semantics of ASM in place (up to return values and function call …
|
|
|
@2904
|
8 years |
sacerdot |
1. Algorithm modified by hand to make it run faster.
The trusted …
|
|
|
@2903
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2902
|
8 years |
sacerdot |
Quick hack to allow printing of OC code. It will be automatically …
|
|
|
@2901
|
8 years |
sacerdot |
1. backendPrinter renamed to printer
2. Clight printing branched into …
|
|
|
@2900
|
8 years |
sacerdot |
Flushing to understand where it is slow.
|
|
|
@2899
|
8 years |
sacerdot |
1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system …
|
|
|
@2898
|
8 years |
piccolo |
1) simplification of cond and seq case for StatusSimulationHelper? …
|
|
|
@2897
|
8 years |
campbell |
Minor tidying.
|
|
|
@2896
|
8 years |
campbell |
Complete part of measurable to structured subtraces proof that
shows …
|
|
|
@2895
|
8 years |
campbell |
Match up function id from RTLabs Callstate with shadow stack,
use in …
|
|
|
@2894
|
8 years |
campbell |
Some progress on showing that the change to structured traces …
|
|
|
@2893
|
8 years |
campbell |
Add tlr_unrepeating.
|
|
|
@2892
|
8 years |
campbell |
Add cost hypotheses.
|
|
|
@2891
|
8 years |
piccolo |
added precondition on seq statement and tested correct in the …
|
|
|
@2890
|
8 years |
sacerdot |
Exported again, now the execution is correct up to LIN for a simple …
|
|
|