|
|
|
@1166
|
10 years |
mulligan |
moved joint ltl lin files into their own directory. more changes to …
|
|
|
|
@1165
|
10 years |
mulligan |
more changes
|
|
|
|
@1163
|
10 years |
mulligan |
even more streamlining and fixes to get things type checking
|
|
|
|
@1162
|
10 years |
mulligan |
changes committed to ertl semantics based on our new combined syntax …
|
|
|
|
@1161
|
10 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
|
@1160
|
10 years |
mulligan |
changes to unfunctorised code in ertltoltl.ma
|
|
|
|
@1156
|
10 years |
sacerdot |
ERTL semantics completed up to initialization and memory model.
|
|
|
|
@1155
|
10 years |
mulligan |
removed
|
|
|
|
@1154
|
10 years |
mulligan |
changes to ertl files: in process of removing ertltoltli.ma in favour …
|
|
|
|
@1152
|
10 years |
mulligan |
more added
|
|
|
|
@1151
|
10 years |
sacerdot |
Only new_/del_frame and framesize left.
|
|
|
|
@1150
|
10 years |
sacerdot |
Push/pop implemented.
|
|
|
|
@1148
|
10 years |
sacerdot |
Function call/return finished (up to retrieving parameters from the …
|
|
|
|
@1146
|
10 years |
sacerdot |
More progress: function call/return almost completed.
|
|
|
|
@1144
|
10 years |
mulligan |
added build.ma file. matita bug found
|
|
|
|
@1142
|
10 years |
sacerdot |
More progress.
|
|
|
|
@1140
|
10 years |
sacerdot |
More instructions implemented.
|
|
|
|
@1138
|
10 years |
mulligan |
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
|
|
|
|
@1137
|
10 years |
sacerdot |
More progress.
|
|
|
|
@1136
|
10 years |
mulligan |
fixed ertl pass
|
|
|
|
@1131
|
10 years |
mulligan |
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …
|
|
|
|
@1130
|
10 years |
sacerdot |
File in progress (copied from RTL).
All instructions considered up to …
|
|
|
|
@1128
|
10 years |
mulligan |
fixed ERTLtoLTLI so it type checks again
|
|
|
|
@1127
|
10 years |
mulligan |
interference graphs axiomatised, more added to ertl
|
|
|
|
@1124
|
10 years |
mulligan |
finished off liveness analysis by axiomatising properties
|
|
|
|
@1110
|
10 years |
mulligan |
changes to get ltl to lin pass to work properly
|
|
|
|
@1108
|
10 years |
mulligan |
changes to get ertltoltli to compile
|
|
|
|
@1107
|
10 years |
mulligan |
got rtl-ertl pass working again
|
|
|
|
@1094
|
10 years |
mulligan |
some changes from today to do with liveness analyses
|
|
|
|
@1090
|
10 years |
mulligan |
small change to liveness analysis
|
|
|
|
@1088
|
10 years |
mulligan |
work on liveness analysis: an imperative nightmare
|
|
|
|
@1085
|
10 years |
mulligan |
removed stray files that are no longer needed
|
|
|
|
@1084
|
10 years |
mulligan |
more added on ertl pass: not sure how much should be axiomatised wrt …
|
|
|
|
@1083
|
10 years |
mulligan |
ertl --> ltl statement generation nearly complete. required some …
|
|
|
|
@1082
|
10 years |
mulligan |
work from today on ertl -> ltl pass
|
|
|
|
@1077
|
10 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1071
|
10 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
|
@878
|
10 years |
campbell |
Removal of manually inserted record projections.
|
|
|
|
@783
|
10 years |
mulligan |
rtl to ertl pass complete (modulo some straightforward axioms that …
|
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@777
|
10 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
|
@759
|
10 years |
mulligan |
More work on the RTL to ERTL pass.
|
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@756
|
10 years |
mulligan |
Made a start on RTL. Renaming in ERTL and below to move closer to …
|
|
|
|
@753
|
10 years |
mulligan |
Work from today.
|
|
|
|
@752
|
10 years |
mulligan |
Fixed error in BitVectorTrieSet? file.
|
|
|
|
@746
|
10 years |
mulligan |
Changes to bitvectortrieset: equality on sets. Added new file for …
|
|
|
|
@745
|
10 years |
mulligan |
Changes from yesterday. Slowly implementing the functorized …
|
|
|
|
@735
|
10 years |
mulligan |
Changes from today
|
|
|
|
@733
|
10 years |
mulligan |
Fixed partial commit.
|
