

@1574

10 years 
campbell 
A little more progress on traces on RTLabs.



@1565

10 years 
campbell 
Note that RTLabs ought to classify branches as "jumps" (in the …



@1563

10 years 
campbell 
A little progress on constructing RTLabs structured traces.



@1559

10 years 
campbell 
Add a notion of flat traces with evidence for RTLabs.



@1552

10 years 
campbell 
Update RTLabs structured trace definition.



@1537

10 years 
campbell 
A preliminary definition of the abstract status record for RTLabs.



@1535

10 years 
campbell 
Make RTLabs semantics use knowledge that the next instruction always …



@1529

10 years 
campbell 
Update RTLabs to RTL with unary operation types.



@1521

10 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1515

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



@1408

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



@1369

10 years 
campbell 
Put type information into frontend unary ops.
Slight change to …



@1358

10 years 
mulligan 
got rtlabs to rtl compiling, foldi_strong needs examining



@1356

10 years 
mulligan 
deleted redundant directory. added outlines for both reports, and …



@1354

10 years 
sacerdot 
One axiom closed.



@1352

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



@1343

10 years 
mulligan 
fixed some bugs in the translation



@1331

10 years 
mulligan 
some changes, but i now have two contradictory proof obligations.



@1325

10 years 
mulligan 
finished implementing the translate constant function



@1316

10 years 
campbell 
Merge in idlookupbranch to trunk.



@1315

10 years 
mulligan 
another move for the same reason. got rtlabs > rtl compiling again by …



@1314

10 years 
mulligan 
name changes so that bash tab completion actually works with some …



@1308

10 years 
mulligan 
changes to translate_cst



@1307

10 years 
mulligan 
adding translate_cst



@1306

10 years 
mulligan 
small changes to rtlabs. what axioms remain look hard to close. need …



@1296

10 years 
mulligan 
changes



@1293

10 years 
mulligan 
finished rtl abs to rtl transformation subject to closing some axioms …



@1292

10 years 
mulligan 
more added to rtlabs translation



@1290

10 years 
sacerdot 
One more function ported to new Joint.



@1288

10 years 
mulligan 
more added to rtlabs to rtl pass



@1287

10 years 
mulligan 
about 3/4 of the way through rtlabs to rtl now



@1286

10 years 
mulligan 
more changes to the rtl abs to rtl pass



@1285

10 years 
mulligan 
more implementation on maps, final push to get rtl abs to rtl working



@1283

10 years 
sacerdot 
Bad programming practice removed: change_label is no longer required …



@1282

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



@1281

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



@1280

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



@1239

10 years 
sacerdot 
RTLAbstoRTL ported to new datatypes.
Note: RTL syntax/semantics is …



@1238

10 years 
campbell 
Update Cminor and RTLabs to fit SmallstepExec? changes.



@1226

10 years 
campbell 
Adjust pretty printers for change in program records, try a test of each.



@1224

10 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1157

10 years 
campbell 
Update pretty printers and examples.



@1149

10 years 
mulligan 
changes to get everything type checking again after changing names of …



@1147

10 years 
campbell 
Remove some obsolete commented out code, update a couple of comments.



@1139

10 years 
campbell 
Shift init_data out of generic program record so that it only appears …



@1138

10 years 
mulligan 
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other



@1123

10 years 
sacerdot 
Added comment about missing alignment of data in memory.



@1116

10 years 
sacerdot 
Some comments.



@1077

10 years 
mulligan 
ack, dependent types are scary



@1073

10 years 
mulligan 
more changes from today



@1072

10 years 
campbell 
Use not equals form of showing entry/exit labels.



@1071

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



@1070

10 years 
campbell 
Show that entry and exit labels are in the RTLabs graph.



@1068

10 years 
mulligan 
rtlabs translation complete subject to axioms



@1067

10 years 
mulligan 
more smaller changes



@1066

10 years 
mulligan 
changes from today



@1064

10 years 
mulligan 
changes from today, nearly complete rtlabs translation pass



@1063

10 years 
mulligan 
changes from today



@1062

10 years 
mulligan 
separated jmeq and coercions from foldstuff.ma in order to fix the …



@1061

10 years 
mulligan 
more work, bug found, ridiculous map3 function with dep. types added



@1060

10 years 
mulligan 
work from this morning and yesterday



@1059

10 years 
mulligan 
work from today, bit of a mess at the moment



@1057

10 years 
mulligan 
changes from today



@1056

10 years 
campbell 
Switch to delayed identifier error scheme.



@1053

10 years 
mulligan 
changes



@1052

10 years 
mulligan 
removed offsets after reading cerco mailing list



@1051

10 years 
mulligan 
removed superfluous addressing mode code from RTLabs/syntax.ma



@1050

10 years 
mulligan 
adding dependent types to map datastructure to remove all option …



@1049

10 years 
mulligan 
more stuff added



@1047

10 years 
mulligan 
more work from today



@1046

10 years 
mulligan 
syntax of rtlabs was wrong: cast not const. more added to rtlabs > …



@1045

10 years 
mulligan 
resolved conflict in rtlabs



@967

10 years 
campbell 
Update RTLabs pretty printer and examples.



@961

10 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@898

10 years 
campbell 
Update pretty printers and examples.



@888

10 years 
campbell 
Use simplified conditionals in RTLabs, following the prototype.



@887

10 years 
campbell 
Start bringing RTLabs into line with the prototype compiler:
 a …



@882

10 years 
campbell 
Fix up fragile proofs for current version of matita.



@879

10 years 
campbell 
Refine "AST" types to include size/signedness information.



@878

10 years 
campbell 
Removal of manually inserted record projections.



@816

10 years 
campbell 
Clight to Cminor compilation, modulo switch statements, temporary …



@799

10 years 
mulligan 
more changes.



@797

10 years 
campbell 
Add error messages wherever the error monad is used.
Sticks to …



@795

10 years 
mulligan 
Changes from this morning.



@793

10 years 
mulligan 
Work from today on rtlabs > rtl pass.



@789

10 years 
mulligan 
More work on rtlabs > rtl pass.



@775

10 years 
campbell 
A few useful definitions for when RTLabs programs fail.



@774

10 years 
campbell 
Separate out the different forms of addition and subtraction in the …



@766

10 years 
campbell 
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …



@765

10 years 
campbell 
Remove superfluous register in RTLabs return statements.
Also fix up …



@764

10 years 
campbell 
Start Cminor to RTLabs phase.
Includes some syntax for matching …



@762

10 years 
campbell 
Make naming of RTLabs files more uniform



@761

10 years 
campbell 
Enforce the use of declared identifiers/registers in Cminor/RTLabs.



@751

10 years 
campbell 
Initial version of the Cminor syntax and semantics.



@750

10 years 
campbell 
Track some of the changes to the prototype in RTLabs.
Just one …



@747

10 years 
campbell 
Merge the two AST files together (although some definitions still need …



@744

10 years 
campbell 
Evict Coqstyle integers from common/Integers.ma.
Make more bitvector …



@738

10 years 
campbell 
Use lower case names for identifiers for consistency with CompCert? …



@737

10 years 
campbell 
Use more abstract identifiers in Clight / RTLabs.



@736

10 years 
campbell 
Extra type safety for identifiers.


