

@1730

8 years 
sacerdot 
Minor changes while studying the proof.



@1729

8 years 
sacerdot 
Comment left from SVN merge removed.



@1601

9 years 
sacerdot 
Files ported to new version of the standard library.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1463

9 years 
mulligan 
added erasure for lin



@1451

9 years 
sacerdot 
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …



@1429

9 years 
sacerdot 
Useless and removed.



@1425

9 years 
mulligan 
changes to the fixpoint calculation in ertl



@1424

9 years 
sacerdot 
1. fold function over BitVectorTries? moved from ERTLToLTL to …



@1423

9 years 
sacerdot 
 spill no longer used
 BUG IN Interference: generating the destruct …



@1415

9 years 
sacerdot 
1. hwreg_store/retrieve no longer returns a res (but it is still …



@1411

9 years 
sacerdot 
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …



@1408

9 years 
sacerdot 
1. Added joint/BEGlobalenvs that is a modification of …



@1390

9 years 
sacerdot 
All fetch_result implementations have been factorized out, leaving …



@1389

9 years 
sacerdot 
One more axiom closed.



@1388

9 years 
sacerdot 
fetch_result implemented for ERTL. This required a different …



@1386

9 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

9 years 
sacerdot 
1. fetch_result and pop_frame now takes the genv in input
2. …



@1384

9 years 
sacerdot 
* fetch_ra taken out of pop_frame again since it is used uniformly and …



@1381

9 years 
sacerdot 
Old commented out code removed.



@1377

9 years 
sacerdot 
pop_frame now incorporates the fetch_result (that made sense only for …



@1372

9 years 
sacerdot 
save_frame now takes the stacksize to allow RTL to allocate the stack frame



@1371

9 years 
sacerdot 
save_frame changed to accept also the formal/actual argument pairs, …



@1359

9 years 
sacerdot 
1. more work on the RTL semantics
2. changes to joint/semantics to …



@1352

9 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1329

9 years 
sacerdot 
1. Definition of addresses moved to BEMem
2. Basic functions on …



@1327

9 years 
sacerdot 
More progress in the implementation of the ERTL specific statements. …



@1324

9 years 
sacerdot 
The semantics of extended statements must also consider the label …



@1318

9 years 
sacerdot 
Frame management implemented.



@1313

9 years 
sacerdot 
(E)RTL semantics ported to new data type for save/pop frame (but not …



@1312

9 years 
sacerdot 
Type of frame operations (pop_frame/save_frame) generalized to take in …



@1303

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



@1302

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



@1282

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



@1281

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



@1280

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



@1275

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



@1274

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



@1271

9 years 
mulligan 
finished, kind of



@1270

9 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1269

9 years 
sacerdot 
Useless include removed.



@1263

9 years 
mulligan 
changes



@1260

9 years 
mulligan 
commit for csc



@1256

9 years 
mulligan 
changes: added a mapi for graphs



@1254

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



@1253

9 years 
mulligan 
uses.ma finished



@1252

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



@1251

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



@1250

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



@1249

9 years 
mulligan 
changes to get everything to typecheck again



@1248

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



@1243

9 years 
mulligan 
small changes



@1242

9 years 
sacerdot 
Some cleanup.



@1241

9 years 
mulligan 
changes for claudio



@1232

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



@1230

9 years 
mulligan 
more changes



@1229

9 years 
mulligan 
changes



@1228

9 years 
mulligan 
some more changes



@1227

9 years 
mulligan 
changes



@1223

9 years 
mulligan 
changes



@1221

9 years 
sacerdot 
Cleanup.



@1220

9 years 
sacerdot 
ERTL ported to the new joint syntax.



@1192

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



@1191

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



@1188

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



@1187

9 years 
mulligan 
fixed build.ma



@1185

9 years 
mulligan 
ported liveness analysis to new code



@1183

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



@1179

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



@1178

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



@1175

9 years 
mulligan 
changes to ertl pass



@1172

9 years 
mulligan 
ertltoltl.ma half complete



@1171

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



@1170

9 years 
mulligan 
changes to ertl > ltl pass



@1168

9 years 
sacerdot 
Joint statements parameterized over a record.



@1166

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



@1165

9 years 
mulligan 
more changes



@1163

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



@1162

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



@1161

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



@1160

9 years 
mulligan 
changes to unfunctorised code in ertltoltl.ma



@1156

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



@1155

9 years 
mulligan 
removed



@1154

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



@1152

9 years 
mulligan 
more added



@1151

9 years 
sacerdot 
Only new_/del_frame and framesize left.



@1150

9 years 
sacerdot 
Push/pop implemented.



@1148

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



@1146

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



@1144

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



@1142

9 years 
sacerdot 
More progress.



@1140

9 years 
sacerdot 
More instructions implemented.



@1138

9 years 
mulligan 
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other



@1137

9 years 
sacerdot 
More progress.



@1136

9 years 
mulligan 
fixed ertl pass



@1131

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



@1130

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



@1128

9 years 
mulligan 
fixed ERTLtoLTLI so it type checks again



@1127

9 years 
mulligan 
interference graphs axiomatised, more added to ertl



@1124

9 years 
mulligan 
finished off liveness analysis by axiomatising properties


