|
|
@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 …
|
|
|
@2889
|
8 years |
sacerdot |
It works very nice!
|
|
|
@2888
|
8 years |
tranquil |
backtracked some partial changes
|
|
|
@2887
|
8 years |
tranquil |
Corrected bug where eliminable statements where not eliminated. …
|
|
|
@2886
|
8 years |
piccolo |
partial commit
|
|
|
@2885
|
8 years |
sacerdot |
Hint at how to change everything.
|
|
|
@2884
|
8 years |
sacerdot |
Debugging print added.
|
|
|
@2883
|
8 years |
piccolo |
partial commit
|
|
|
@2882
|
8 years |
sacerdot |
…
|
|
|
@2881
|
8 years |
sacerdot |
…
|
|
|
@2880
|
8 years |
sacerdot |
…
|
|
|
@2879
|
8 years |
tranquil |
changed coercion from list of joint_seq to blocks to a more efficient one
|
|
|
@2878
|
8 years |
tranquil |
backtracked some changes that were not ready for commit
|
|
|
@2877
|
8 years |
garnier |
Correction of a bug in my former bug correction.
|
|
|
@2876
|
8 years |
tranquil |
corrected another endianess bug in joint_semantics. Switched some …
|
|
|
@2875
|
8 years |
sacerdot |
Pretty printing of object code integrated too.
A couple of axioms make …
|
|
|
@2874
|
8 years |
sacerdot |
Syntax fixed: ./cerco [-exec] filename annotationoption
|
|
|
@2873
|
8 years |
sacerdot |
Extracted again.
|
|
|
@2872
|
8 years |
tassi |
Fix list of distributed files so that the debian package can be built
|
|
|
@2871
|
8 years |
tranquil |
op2 evaluation on beval's rendered oblivious to carry bit when …
|
|
|
@2870
|
8 years |
sacerdot |
Proof fixed.
|
|
|
@2869
|
8 years |
tranquil |
some reorganization of definitions, and a new taaf_append_taaf
|
|
|
@2868
|
8 years |
sacerdot |
Pretty printing of ERTL and ERTLptr code.
|
|
|