

@1303

8 years 
sacerdot 
1. LTL/semantics.ma added (work in progress)
2. init_locals fixed to …



@1302

8 years 
sacerdot 
ERTL/semantics.ma ported to joint/SemanticUtils (in progress)



@1282

8 years 
sacerdot 
Cosmetic change: names of joint statements/instructions shortened and …



@1281

8 years 
sacerdot 
Porting of all transformation to the joint syntax practically …



@1280

8 years 
sacerdot 
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …



@1275

8 years 
sacerdot 
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …



@1274

8 years 
mulligan 
starting removing axioms from adts and giving them proper implementations



@1271

8 years 
mulligan 
finished, kind of



@1270

8 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1269

8 years 
sacerdot 
Useless include removed.



@1263

8 years 
mulligan 
changes



@1260

8 years 
mulligan 
commit for csc



@1256

8 years 
mulligan 
changes: added a mapi for graphs



@1254

8 years 
sacerdot 
More progress towards porting of RTLtoERTL to joint syntax.



@1253

8 years 
mulligan 
uses.ma finished



@1252

8 years 
sacerdot 
graph_params added to joint/Joint.ma, together with useful common …



@1251

8 years 
mulligan 
changes to get things compiling again after yet another CSC rearrangement!



@1250

8 years 
sacerdot 
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …



@1249

8 years 
mulligan 
changes to get everything to typecheck again



@1248

8 years 
mulligan 
deleted files that do not compile in utilities, changed ertl.ma to use …



@1243

8 years 
mulligan 
small changes



@1242

8 years 
sacerdot 
Some cleanup.



@1241

8 years 
mulligan 
changes for claudio



@1232

8 years 
mulligan 
big changes: got what was implemented in the ertl to ltl pass type …



@1230

8 years 
mulligan 
more changes



@1229

8 years 
mulligan 
changes



@1228

8 years 
mulligan 
some more changes



@1227

8 years 
mulligan 
changes



@1223

8 years 
mulligan 
changes



@1221

8 years 
sacerdot 
Cleanup.



@1220

8 years 
sacerdot 
ERTL ported to the new joint syntax.



@1192

8 years 
mulligan 
some files that were missing / laying dormant on my computer



@1191

8 years 
mulligan 
ertl to ertl pass back where it was before the changes to joint



@1188

8 years 
mulligan 
removed stray lines from uses.ma so that it at least typechecks



@1187

8 years 
mulligan 
fixed build.ma



@1185

8 years 
mulligan 
ported liveness analysis to new code



@1183

8 years 
mulligan 
removed parameterised label types in the three lowest level languages



@1179

8 years 
mulligan 
changes to ertl, ltl and lin to use new notion of joint params. ertl …



@1178

8 years 
mulligan 
fixed ertl.ma to use new version of joint params



@1175

8 years 
mulligan 
changes to ertl pass



@1172

8 years 
mulligan 
ertltoltl.ma half complete



@1171

8 years 
mulligan 
changes made on claudio's request: changed order of nesting in the …



@1170

8 years 
mulligan 
changes to ertl > ltl pass



@1168

8 years 
sacerdot 
Joint statements parameterized over a record.



@1166

8 years 
mulligan 
moved joint ltl lin files into their own directory. more changes to …



@1165

8 years 
mulligan 
more changes



@1163

8 years 
mulligan 
even more streamlining and fixes to get things type checking



@1162

8 years 
mulligan 
changes committed to ertl semantics based on our new combined syntax …



@1161

8 years 
mulligan 
changes from today: merged ertl, ltl and lin into one datatype to …



@1160

8 years 
mulligan 
changes to unfunctorised code in ertltoltl.ma



@1156

8 years 
sacerdot 
ERTL semantics completed up to initialization and memory model.



@1155

8 years 
mulligan 
removed



@1154

8 years 
mulligan 
changes to ertl files: in process of removing ertltoltli.ma in favour …



@1152

8 years 
mulligan 
more added



@1151

8 years 
sacerdot 
Only new_/del_frame and framesize left.



@1150

8 years 
sacerdot 
Push/pop implemented.



@1148

8 years 
sacerdot 
Function call/return finished (up to retrieving parameters from the …



@1146

8 years 
sacerdot 
More progress: function call/return almost completed.



@1144

8 years 
mulligan 
added build.ma file. matita bug found



@1142

8 years 
sacerdot 
More progress.



@1140

8 years 
sacerdot 
More instructions implemented.



@1138

8 years 
mulligan 
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other



@1137

8 years 
sacerdot 
More progress.



@1136

8 years 
mulligan 
fixed ertl pass



@1131

8 years 
mulligan 
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …



@1130

8 years 
sacerdot 
File in progress (copied from RTL).
All instructions considered up to …



@1128

8 years 
mulligan 
fixed ERTLtoLTLI so it type checks again



@1127

8 years 
mulligan 
interference graphs axiomatised, more added to ertl



@1124

8 years 
mulligan 
finished off liveness analysis by axiomatising properties



@1110

8 years 
mulligan 
changes to get ltl to lin pass to work properly



@1108

8 years 
mulligan 
changes to get ertltoltli to compile



@1107

8 years 
mulligan 
got rtlertl pass working again



@1094

9 years 
mulligan 
some changes from today to do with liveness analyses



@1090

9 years 
mulligan 
small change to liveness analysis



@1088

9 years 
mulligan 
work on liveness analysis: an imperative nightmare



@1085

9 years 
mulligan 
removed stray files that are no longer needed



@1084

9 years 
mulligan 
more added on ertl pass: not sure how much should be axiomatised wrt …



@1083

9 years 
mulligan 
ertl > ltl statement generation nearly complete. required some …



@1082

9 years 
mulligan 
work from today on ertl > ltl pass



@1077

9 years 
mulligan 
ack, dependent types are scary



@1071

9 years 
mulligan 
changes the specific form that the added proofs take to use None, not …



@878

9 years 
campbell 
Removal of manually inserted record projections.



@783

9 years 
mulligan 
rtl to ertl pass complete (modulo some straightforward axioms that …



@782

9 years 
mulligan 
More work on rtlertl pass from today, plus resolved conflict.



@777

9 years 
mulligan 
Lots of work on RTL to ERTL pass from today.



@759

9 years 
mulligan 
More work on the RTL to ERTL pass.



@757

9 years 
mulligan 
Lots more fixing to get both front and backends using same conventions …



@756

9 years 
mulligan 
Made a start on RTL. Renaming in ERTL and below to move closer to …



@753

9 years 
mulligan 
Work from today.



@752

9 years 
mulligan 
Fixed error in BitVectorTrieSet? file.



@746

9 years 
mulligan 
Changes to bitvectortrieset: equality on sets. Added new file for …



@745

9 years 
mulligan 
Changes from yesterday. Slowly implementing the functorized …



@735

9 years 
mulligan 
Changes from today



@733

9 years 
mulligan 
Fixed partial commit.
