|
|
@991
|
10 years |
mulligan |
loads of axioms related to equality on instructions closed
|
|
|
@990
|
10 years |
sacerdot |
Do no longer use the daemon automatically :-)
|
|
|
@989
|
10 years |
sacerdot |
Type of build_maps strengthened.
|
|
|
@988
|
10 years |
sacerdot |
Proof restored.
|
|
|
@987
|
10 years |
sacerdot |
Real parameterization over the policy.
|
|
|
@986
|
10 years |
mulligan |
changes to paper
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
@984
|
10 years |
mulligan |
updates
|
|
|
@983
|
10 years |
mulligan |
more work added
|
|
|
@982
|
10 years |
boender |
- this should work (see previous commit)
|
|
|
@981
|
10 years |
mulligan |
added more, worked on conclusions and related work. need just to …
|
|
|
@980
|
10 years |
boender |
- displaced some lemmas (jmeq) from AssemblyProof?
|
|
|
@979
|
10 years |
sacerdot |
…
|
|
|
@978
|
10 years |
campbell |
Update remaining Clight examples.
|
|
|
@977
|
10 years |
sacerdot |
#$%@#$@#$
|
|
|
@976
|
10 years |
mulligan |
more changes, rearranged paper to put lemmas/defns in correct order, …
|
|
|
@975
|
10 years |
sacerdot |
…
|
|
|
@974
|
10 years |
mulligan |
more added
|
|
|
@973
|
10 years |
mulligan |
work from yesterday that could not be committed
|
|
|
@972
|
10 years |
sacerdot |
…
|
|
|
@971
|
10 years |
sacerdot |
…
|
|
|
@970
|
10 years |
mulligan |
commit as i need some money for the communists
|
|
|
@969
|
10 years |
mulligan |
more work on paper, nearly finished policy discussion
|
|
|
@968
|
10 years |
mulligan |
work on paper
|
|
|
@967
|
10 years |
campbell |
Update RTLabs pretty printer and examples.
|
|
|
@966
|
10 years |
campbell |
Update Cminor pretty printer and some examples.
|
|
|
@965
|
10 years |
campbell |
Update some Clight examples.
|
|
|
@964
|
10 years |
campbell |
Rest of cast fix.
|
|
|
@963
|
10 years |
campbell |
Extra debugging aid for animation of semantics.
|
|
|
@962
|
10 years |
campbell |
Casts should use source type's signedness, not the target's.
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
@960
|
10 years |
mulligan |
more work on paper
|
|
|
@959
|
10 years |
sacerdot |
…
|
|
|
@958
|
10 years |
sacerdot |
…
|
|
|
@957
|
10 years |
sacerdot |
…
|
|
|
@956
|
10 years |
mulligan |
changes prior to claudio's editing
|
|
|
@955
|
10 years |
mulligan |
more work on conclusions
|
|
|
@954
|
10 years |
mulligan |
more changes to introduction
|
|
|
@953
|
10 years |
mulligan |
more changes, including additions to the bibliography, and tightening …
|
|
|
@952
|
10 years |
mulligan |
work from yesterday
|
|
|
@951
|
10 years |
sacerdot |
long call case completed
|
|
|
@950
|
10 years |
sacerdot |
Horrible sub-proof finished :-)
|
|
|
@949
|
10 years |
mulligan |
resolved conflict, work from today
|
|
|
@948
|
10 years |
sacerdot |
Some progress on the Call case.
|
|
|
@947
|
10 years |
sacerdot |
…
|
|
|
@946
|
10 years |
sacerdot |
Jmp case repaired after addition of MAP hypothesis.
|
|
|
@945
|
10 years |
mulligan |
more small changes to proof of main thrm
|
|
|
@944
|
10 years |
mulligan |
split definition
|
|
|
@943
|
10 years |
sacerdot |
…
|
|
|
@942
|
10 years |
sacerdot |
New invariant for the main theorem.
The new invariant is much more …
|
|
|
@941
|
10 years |
sacerdot |
Jmp case finished up to arithmetical properties.
|
|
|
@940
|
10 years |
mulligan |
more changes to inc case of main theorem
|
|
|
@939
|
10 years |
sacerdot |
Long Jmp case finished.
|
|
|
@938
|
10 years |
sacerdot |
…
|
|
|
@937
|
10 years |
mulligan |
resolved conflict in assembly_proof, more lemmas added
|
|
|
@936
|
10 years |
sacerdot |
Ticks are now handled correctly everywhere and the main proof takes …
|
|
|
@935
|
10 years |
mulligan |
changes to status and assembly proof
|
|
|
@934
|
10 years |
sacerdot |
…
|
|
|
@933
|
10 years |
sacerdot |
New proof strategy.
|
|
|
@932
|
10 years |
sacerdot |
…
|
|
|
@931
|
10 years |
sacerdot |
…
|
|
|
@930
|
10 years |
sacerdot |
Comment, Cost, ADD, ADC cases done.
|
|
|
@929
|
10 years |
mulligan |
added ticks_of function
|
|
|
@928
|
10 years |
sacerdot |
Technical splitting.
|
|
|
@927
|
10 years |
mulligan |
changes
|
|
|
@926
|
10 years |
sacerdot |
Main theorem false because of ticks :-(
|
|
|
@925
|
10 years |
sacerdot |
…
|
|
|
@924
|
10 years |
sacerdot |
…
|
|
|
@923
|
10 years |
sacerdot |
Main theorem made nice... but unprovable at the moment.
|
|
|
@922
|
10 years |
mulligan |
changes to get assemblyproof to compile
|
|
|
@921
|
10 years |
mulligan |
resolved conflict, fixed bugs
|
|
|
@920
|
10 years |
boender |
- corrected mov instruction
|
|
|
@919
|
10 years |
sacerdot |
Back to a readable statement.
|
|
|
@918
|
10 years |
mulligan |
headers added, etc.
|
|
|
@917
|
10 years |
mulligan |
outline of cpp paper committed
|
|
|
@916
|
10 years |
sacerdot |
Fix for jump_expansion_policy.
|
|
|
@915
|
10 years |
mulligan |
finished changes to fetch_assembly_pseudo2
|
|
|
@914
|
10 years |
boender |
- complete.
|
|
|
@913
|
10 years |
boender |
- temporary commit s.t. Assembly compiles
|
|
|
@912
|
10 years |
sacerdot |
Readable main theorem statement.
|
|
|
@911
|
10 years |
sacerdot |
Type of set_code_memory generalized.
|
|
|
@910
|
10 years |
mulligan |
removed bug in execute_1_pseudoinstruction
|
|
|
@909
|
10 years |
sacerdot |
Back to the main theorem.
|
|
|
@908
|
10 years |
sacerdot |
Next big lemma proved!
|
|
|
@907
|
10 years |
boender |
- added quadruples to Util
- start of implementation of new jump …
|
|
|
@906
|
10 years |
sacerdot |
…
|
|
|
@905
|
10 years |
mulligan |
work from today
|
|
|
@904
|
10 years |
sacerdot |
Cleanup.
|
|
|
@903
|
10 years |
sacerdot |
Statement of new main lemma (as axiom).
|
|
|
@902
|
10 years |
sacerdot |
Cleanup.
|
|
|
@901
|
10 years |
sacerdot |
Second main lemma proved.
|
|
|
@900
|
10 years |
sacerdot |
New implementation of flatten was bugged: fixed.
|
|
|
@899
|
10 years |
mulligan |
changed defn. of flatten
|
|
|
@898
|
10 years |
campbell |
Update pretty printers and examples.
|
|
|
@897
|
10 years |
sacerdot |
Proof completed, fetch and assembly are mutual inverses.
|
|
|
@896
|
10 years |
sacerdot |
Proof finished (but ugly) :-)
|
|
|
@895
|
10 years |
sacerdot |
Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
|
|
|
@894
|
10 years |
sacerdot |
Bug more evident.
|
|
|
@893
|
10 years |
sacerdot |
Cleanup.
|
|
|
@892
|
10 years |
sacerdot |
First fundamental lemma almost finished.
|
|
|