|
|
|
@3145
|
8 years |
tranquil |
* removed sigma types from traces of intensional events
* completed …
|
|
|
|
@3118
|
8 years |
piccolo |
1) finished return case in StatusSimulationHelper?
2) started to write …
|
|
|
|
@3115
|
8 years |
campbell |
Clean up some left-over lemmas and move comment back into place.
|
|
|
|
@3112
|
8 years |
tranquil |
added invariant that costlabels are only assigned to NOPs (not proved …
|
|
|
|
@3104
|
8 years |
sacerdot |
Performance improvement.
|
|
|
|
@3103
|
8 years |
mckinna |
Simplified "include" dependencies
|
|
|
|
@3102
|
8 years |
mckinna |
Removed redundant refs to current_instruction0,
which itself has been …
|
|
|
|
@3101
|
8 years |
mckinna |
Removed redundant lemma execute_1_technical,
which is covered by …
|
|
|
|
@3100
|
8 years |
mckinna |
Removed redundant defn of current_instruction0,
which only appears in …
|
|
|
|
@3099
|
8 years |
mckinna |
Simplified preliminaries:
inefficient_address_of_word_labels, and …
|
|
|
|
@3098
|
8 years |
sacerdot |
Performance improvement.
|
|
|
|
@3097
|
8 years |
sacerdot |
Performance improvement in policy computation.
|
|
|
|
@3096
|
8 years |
tranquil |
preliminary work on closing correctness.ma
|
|
|
|
@3095
|
8 years |
sacerdot |
Some performance improvement: an heavy computation was done again and …
|
|
|
|
@3083
|
8 years |
sacerdot |
The cost and stack* variables are now initialized with the cost of …
|
|
|
|
@3082
|
8 years |
mckinna |
Tidying up: the long comment about preamble/renamed_symbols in the …
|
|
|
|
@3081
|
8 years |
campbell |
Tidy up recent work a little.
|
|
|
|
@3078
|
8 years |
tranquil |
fixed change of Mov
|
|
|
|
@3076
|
8 years |
mckinna |
simplified include dependencies
|
|
|
|
@3075
|
8 years |
mckinna |
Apologies for late folding in of old changes which were left over from …
|
|
|
|
@3074
|
8 years |
campbell |
Put some kind of high level proof in for front-end.
|
|
|
|
@3072
|
8 years |
tranquil |
corrected a bug (translate_store was wrong)
|
|
|
|
@3066
|
8 years |
tranquil |
* implemented get_arg_16 for ACC_DPTR
* LINToASM is now agnostic as to …
|
|
|
|
@3065
|
8 years |
sacerdot |
Efficiency of semantics of assembled improved: ticks_of was …
|
|
|
|
@3064
|
8 years |
sacerdot |
Efficiency of the semantics of assembly improved by avoiding the …
|
|
|
|
@3063
|
8 years |
campbell |
Remove measure function from FEMeasurable because we're not using it …
|
|
|
|
@3062
|
8 years |
sacerdot |
Bug fixed in the semantics of Mov: the offset was ignored.
Now all …
|
|
|
|
@3060
|
8 years |
sacerdot |
Bug fixed in the semantics of JMP.
The bug was due to a bug in the …
|
|
|
|
@3057
|
8 years |
tranquil |
lookup of function identifiers was not corrected with sigma
|
|
|
|
@3056
|
8 years |
tranquil |
fixed a merge gone wrong
|
|
|
|
@3055
|
8 years |
campbell |
Start getting partial Clight to Cminor proof in shape for …
|
|
|
|
@3054
|
8 years |
campbell |
Put missing typ check in; adjust proof because I did it a little …
|
|
|
|
@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???)
|
|
|
|
