|
|
|
@3053
|
8 years |
campbell |
Cast simplification preserves measurable subtraces.
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@3028
|
8 years |
sacerdot |
Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
|
|
|
|
@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 …
|
|
|
|
@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
|
|
|
|
@3014
|
8 years |
tranquil |
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
|
|
|
|
@3010
|
8 years |
tranquil |
same bug as was in liveness is now fixed
|
|
|
|
@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 …
|
|
|
|
@3004
|
8 years |
tranquil |
fixed a bug where when doing an asymetrical op, cast initialization …
|
|
|
|
@3003
|
8 years |
sacerdot |
Correctness.ma "repaired"
|
|
|
|
@2999
|
8 years |
sacerdot |
code_memory added to labelled_object_code to avoid recomputing it …
|
|
|
|
@2996
|
8 years |
sacerdot |
Printing of graphs now starts from the entry point.
|
|
|
|
@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 …
|
|
|
|
@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.
|
|
|
|
@2980
|
8 years |
tranquil |
fixed b_graph_translate
|
|
|
|
@2978
|
8 years |
tranquil |
merged accidentally backtracked changes
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@2963
|
8 years |
sacerdot |
Bug fixed: the pre-main for the final code is now
COST k1
…
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@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 …
|
|
|
|
@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.
|
|
|
|
@2912
|
8 years |
sacerdot |
Ouch, another bug in the very same function.
Fixed too, on an example …
|
|
|
|
