|
|
@3033
|
8 years |
sacerdot |
Bug fixed: sign_extension was extending according to the _second_ bit, …
|
|
|
@3032
|
8 years |
campbell |
Remind myself why ms_rel_normal is reasonable.
|
|
|
@3031
|
8 years |
campbell |
Tidy up RTLabs preclassified_system definitions.
|
|
|
@3030
|
8 years |
campbell |
Break up front-end for correctness proof.
Use let rec to prevent …
|
|
|
@3029
|
8 years |
sacerdot |
New extraction after DPH/DPL bug fixing.
|
|
|
@3028
|
8 years |
sacerdot |
Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
|
|
|
@3027
|
8 years |
sacerdot |
Another output used by the plug-in.
|
|
|
@3026
|
8 years |
sacerdot |
With -a we now produce also the .cerco file required by the plug-in.
|
|
|
@3025
|
8 years |
sacerdot |
1. two syntax errors in instrumented files fixed
2. the compiler now …
|
|
|
@3024
|
8 years |
sacerdot |
Bug fixed: set_flags was ignoring the cy and ov flags.
|
|
|
@3023
|
8 years |
sacerdot |
Typo fixed. It made all GOTOs jump to random positions in the ASM code.
|
|
|
@3022
|
8 years |
campbell |
Make a couple of tests monadic for easier inversion.
|
|
|
@3021
|
8 years |
campbell |
Replace clight_clock_after with a more sensible definition that uses …
|
|
|
@3020
|
8 years |
sacerdot |
- Options not used removed from the help/interface.
- More compliance …
|
|
|
@3019
|
8 years |
sacerdot |
New extraction after ERTLptr abortion.
|
|
|
@3018
|
8 years |
sacerdot |
1) some files repaired
2) all stuff related to the aborted pass …
|
|
|
@3017
|
8 years |
sacerdot |
Repaired.
|
|
|
@3016
|
8 years |
tranquil |
fixed after previous commit
|
|
|
@3015
|
8 years |
sacerdot |
Comment removed
|
|
|
@3014
|
8 years |
tranquil |
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
|
|
|
@3013
|
8 years |
sacerdot |
Temporary parsing files removed.
|
|
|
@3012
|
8 years |
sacerdot |
Debugging code removed after bug fixing.
|
|
|
@3011
|
8 years |
sacerdot |
New extraction.
|
|
|
@3010
|
8 years |
tranquil |
same bug as was in liveness is now fixed
|
|
|
@3009
|
8 years |
sacerdot |
New extraction.
|
|
|
@3008
|
8 years |
tranquil |
corrected bug where the address of pointer calls was not defined as used
|
|
|
@3007
|
8 years |
campbell |
Sketch out how Cminor to RTLabs correctness would fit into the …
|
|
|
@3006
|
8 years |
sacerdot |
New extraction, bugs fixed.
|
|
|
@3005
|
8 years |
sacerdot |
Beginning of making it fully compatible with untrusted one.
|
|
|
@3004
|
8 years |
tranquil |
fixed a bug where when doing an asymetrical op, cast initialization …
|
|
|
@3003
|
8 years |
sacerdot |
Correctness.ma "repaired"
|
|
|
@3002
|
8 years |
tranquil |
fixed previous commit
|
|
|
@3001
|
8 years |
sacerdot |
New extraction.
|
|
|
@3000
|
8 years |
tranquil |
added RTLabs printer
|
|
|
@2999
|
8 years |
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
|
@2998
|
8 years |
sacerdot |
Test on conditional execution. Fails atm.
|
|
|
@2997
|
8 years |
sacerdot |
New extraction.
|
|
|
@2996
|
8 years |
sacerdot |
Printing of graphs now starts from the entry point.
|
|
|
@2995
|
8 years |
sacerdot |
The lIN_printer extracted.
|
|
|
@2994
|
8 years |
sacerdot |
The LIN printer.
|
|
|
@2993
|
8 years |
sacerdot |
1. performance improved: the type inference was inferring
…
|
|
|
@2992
|
8 years |
campbell |
Add "only one return" invariant to RTLabs functions.
|
|
|
@2991
|
8 years |
piccolo |
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …
|
|
|
@2990
|
8 years |
campbell |
Replace dodgy hypothesis by nice ones, clean up a little.
|
|
|
@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.
|
|
|