

@1516

10 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1512

10 years 
campbell 
Shorten proof of goal that solves now.



@1510

10 years 
sacerdot 
All files ported to new dependent inversion.



@1480

10 years 
sacerdot 
Proof changed (to use new automation).
BUG FOUND: automation fails if …



@1465

10 years 
sacerdot 
Dead code removed.



@1410

10 years 
campbell 
Remove a few old workarounds.



@1401

10 years 
ricciott 
Changes concerning the new behavior of destruct.



@1395

10 years 
sacerdot 
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …



@1369

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



@1368

10 years 
sacerdot 
A bug in the clear tactic makes the previous (correct) commit wrong. …



@1367

10 years 
sacerdot 
Proof improvement, still somehow a bit slow.



@1355

10 years 
sacerdot 
monadic fold_lefti added



@1353

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



@1351

10 years 
campbell 
Tidy up some loose ends from the invariants branch merge.



@1350

10 years 
sacerdot 
Porting to latest destruct tactic.
Note: the tactics has a few …



@1347

10 years 
campbell 
Remove obsolete definitions.



@1339

10 years 
sacerdot 
Automation is now stronger.



@1316

10 years 
campbell 
Merge in idlookupbranch to trunk.



@1268

10 years 
sacerdot 
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …



@1253

10 years 
mulligan 
uses.ma finished



@1233

10 years 
sacerdot 
1) Ported to Brian's new dependent type for fullexec
2) Universe level …



@1231

10 years 
campbell 
Change SmallstepExec? so that states can depend on global information. …



@1225

10 years 
campbell 
Missing ; in proof



@1224

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



@1215

10 years 
sacerdot 
1) Added shifting directly on pointers
2) More temporary axioms closed.



@1214

10 years 
sacerdot 
res_to_opt function added to common/Errors and used in joint/semantics …



@1213

10 years 
sacerdot 
1) New values (joint/BEValues.ma) and memory model for the backends
…



@1181

10 years 
mulligan 
changed smallstep exec in order to remove matita bug (superposition.ml …



@1139

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



@1129

10 years 
mulligan 
removed conversions between Register and register



@1125

10 years 
sacerdot 
Monadic mfold_left2 added.



@1092

10 years 
campbell 
Some minor definitions for identifiers and lists.



@1082

10 years 
mulligan 
work from today on ertl > ltl pass



@1080

10 years 
mulligan 
more added



@1077

10 years 
mulligan 
ack, dependent types are scary



@1072

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



@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



@1064

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



@1060

10 years 
mulligan 
work from this morning and yesterday



@1059

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



@1058

10 years 
campbell 
Evict CompCert? Maps interface in favour of BitVectorTries?.



@1057

10 years 
mulligan 
changes from today



@1056

10 years 
campbell 
Switch to delayed identifier error scheme.



@1055

10 years 
mulligan 
changes to how identifiers are generated



@1053

10 years 
mulligan 
changes



@1052

10 years 
mulligan 
removed offsets after reading cerco mailing list



@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



@985

10 years 
sacerdot 
1) Major refactoring: proofs moved where they should be.
2) New …



@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 …



@891

10 years 
campbell 
Revise proofs affected by recent matita change.



@889

10 years 
sacerdot 
Minor changes because of the new, weaker (but much faster) delift.



@882

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



@881

10 years 
campbell 
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.



@880

10 years 
campbell 
Add type information into Cminor.
As a result, the Clight to Cminor …



@879

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



@849

10 years 
sacerdot 
…



@816

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



@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.



@790

10 years 
campbell 
A little tidying: get rid of requirement for jmeq in Mem.ma, remove …



@789

10 years 
mulligan 
More work on rtlabs > rtl pass.



@782

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



@781

10 years 
campbell 
Implement labelling pass for Clight.



@779

10 years 
campbell 
Add merging of tries and identifier sets (based on Dominic's earlier …



@777

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



@774

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



@764

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



@761

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



@758

10 years 
campbell 
Implement replacement of global var initialisation data by code in Cminor.



@757

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



@753

10 years 
mulligan 
Work from today.



@751

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



@747

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



@746

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



@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.



@731

10 years 
campbell 
Common definition for animation semantics, and factor out IO definitions.



@728

10 years 
mulligan 
Changes from last two days.



@727

10 years 
campbell 
Enough fixes to let an RTLabs program run.



@726

11 years 
campbell 
Change identifiers to Words in Clight and RTLabs semantics.



@722

11 years 
mulligan 
Committing changes from today. Several files do not typecheck.



@720

11 years 
campbell 
Sort out cost labels.



@718

11 years 
campbell 
Add an AST type (i.e., intermediate language type) for pointers.



@714

11 years 
mulligan 
Work on translation from LTL to LIN.



@710

11 years 
campbell 
Start of way to import RTLabs from prototype compiler.



@702

11 years 
campbell 
Refine smallstep executable semantics abstraction a little.
Some …



@700

11 years 
campbell 
Get Clight semantics going again (except for problems CexecEquiv? that …



@699

11 years 
mulligan 
More or less finished formalisation of LIN.



@698

11 years 
mulligan 
Commit with changes to files to get our files to typecheck.



@697

11 years 
campbell 
Merge Clight branch of vectors and friends.
Start making stuff build.


