|
|
@3466
|
7 years |
asperti |
Removed function that is only in the standard library.
Maaaany more to …
|
|
|
@3415
|
7 years |
boender |
- changes for proceedings of TACAS 2014
|
|
|
@3395
|
7 years |
fguidi |
scan for redundant includes with new version of matitadep
|
|
|
@3393
|
7 years |
boender |
- TACAS stuff
|
|
|
@3392
|
7 years |
boender |
- renamed paper yet again
|
|
|
@3388
|
8 years |
piccolo |
partial commit
|
|
|
@3372
|
8 years |
piccolo |
Added new implementation of labelling approach based on LTS and …
|
|
|
@3371
|
8 years |
piccolo |
Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …
|
|
|
@3370
|
8 years |
sacerdot |
Submitted.
|
|
|
@3365
|
8 years |
boender |
- changed spelling error
|
|
|
@3364
|
8 years |
boender |
- added bit to the introduction about contribution
|
|
|
@3363
|
8 years |
boender |
- renamed directory
|
|
|
@3362
|
8 years |
boender |
- added some bits as per Claudio's mail
- rewrote some small things
- …
|
|
|
@3361
|
8 years |
sacerdot |
15 pages version
|
|
|
@3354
|
8 years |
boender |
- one more
|
|
|
@3353
|
8 years |
boender |
- addressed minor corrections by referees
|
|
|
@3352
|
8 years |
boender |
- nicified formulas
|
|
|
@3342
|
8 years |
boender |
- completed reworking of proofs
|
|
|
@3341
|
8 years |
boender |
- more notation stuff (still needs work!)
|
|
|
@3338
|
8 years |
boender |
- updated statement of main correctness statement (still needs work)
|
|
|
@3304
|
8 years |
boender |
- added 2012 reviews
- updated affiliation
|
|
|
@3265
|
8 years |
tranquil |
added validate_pointer filter
in Interference added that intereference …
|
|
|
@3263
|
8 years |
tranquil |
moved callee saved saving and restoring to ERTL -> LTL pass (untrusted …
|
|
|
@3262
|
8 years |
piccolo |
reverted status_simulation_utils
|
|
|
@3261
|
8 years |
piccolo |
reverted joint_semantics rtl_semantics and ltl_semantics
|
|
|
@3259
|
8 years |
piccolo |
changed ERTL semantics:
1) added manipulation of stack pointer …
|
|
|
@3257
|
8 years |
tranquil |
fixed uses in ERTL
|
|
|
@3256
|
8 years |
tranquil |
fixed compilation
|
|
|
@3255
|
8 years |
tranquil |
* dropped newframe and delframe (to be integrated in calls and returns …
|
|
|
@3254
|
8 years |
sacerdot |
Code I always forgot to commit.
To be ported to ERTLtoLTLProof.ma.
|
|
|
@3253
|
8 years |
piccolo |
some proof obbligation closed of ERTL to LTL proof
|
|
|
@3252
|
8 years |
piccolo |
proof obbligation added on ERTL to LTL proof
|
|
|
@3237
|
8 years |
campbell |
Some incomplete work on Clight -> Cminor call steps.
|
|
|
@3217
|
8 years |
piccolo |
Correctness of ERTL to LTL in place
|
|
|
@3178
|
8 years |
campbell |
Some progress on Callstate steps in Clight to Cminor.
Note that some …
|
|
|
@3176
|
8 years |
mckinna |
simplified dependencies
|
|
|
@3171
|
8 years |
mckinna |
removed redundant dependencies
|
|
|
@3170
|
8 years |
mckinna |
removed redundant dependencies
|
|
|
@3165
|
8 years |
campbell |
A little bit of progress on Callstate case.
|
|
|
@3156
|
8 years |
campbell |
Rebuild prefix traces in back-end's preferred form.
|
|
|
@3155
|
8 years |
campbell |
Now have proof that the initial states are in simulation for clight to …
|
|
|
@3154
|
8 years |
piccolo |
1) changed block_of_call in order to prevent pre-main calls
2) …
|
|
|
@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 …
|
|
|