|
|
@3051
|
8 years |
tranquil |
fixed order of global initialization in LINToASM. For the moment …
|
|
|
@3050
|
8 years |
piccolo |
1) Added general commutation theorem for monads.
2) Added some …
|
|
|
@3049
|
8 years |
campbell |
Globalenvs and initial states for cast simplification.
|
|
|
@3048
|
8 years |
campbell |
Improve dependency for cast simplification.
|
|
|
@3047
|
8 years |
campbell |
Switch removal and labelling combined.
|
|
|
@3046
|
8 years |
campbell |
Main part of combined switch removal and labelling proof.
|
|
|
@3045
|
8 years |
tranquil |
fixed what made test3 fail. However it involves a different notion of …
|
|
|
@3044
|
8 years |
campbell |
Start showing combination of switch removal and labelling is OK.
Fix …
|
|
|
@3043
|
8 years |
sacerdot |
New major extraction that should have solved all remaining issues.
As …
|
|
|
@3042
|
8 years |
sacerdot |
Repaired.
|
|
|
@3041
|
8 years |
sacerdot |
Repaired
|
|
|
@3040
|
8 years |
tranquil |
fixed LINToASM
|
|
|
@3039
|
8 years |
tranquil |
* merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
|
|
|
@3038
|
8 years |
sacerdot |
Bug fixed: the stack_cost* variables must be declared before the …
|
|
|
@3037
|
8 years |
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
|
@3036
|
8 years |
garnier |
Fixing some problems, progress, etc
|
|
|
@3035
|
8 years |
mckinna |
Tweak: tidied up ?/\ldots
Conceptual: better monadic threading of …
|
|
|
@3034
|
8 years |
sacerdot |
Bug fixed: COST instructions are now assembled as NOP to prevent the …
|
|
|
@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 …
|
|
|