

@3081

7 years 
campbell 
Tidy up recent work a little.



@3063

7 years 
campbell 
Remove measure function from FEMeasurable because we're not using it …



@3007

7 years 
campbell 
Sketch out how Cminor to RTLabs correctness would fit into the …



@2992

7 years 
campbell 
Add "only one return" invariant to RTLabs functions.



@2971

7 years 
campbell 
Single RTLabs return statement.



@2936

7 years 
campbell 
Disable initialisation code generation in Cminor, propogate init data …



@2924

7 years 
campbell 
Make calls to a known identifier actually use a direct call.



@2809

7 years 
sacerdot 
…



@2793

7 years 
campbell 
Oops, gave fields wrong order during initialisation.



@2737

7 years 
garnier 
Commit of current proof state for Clight to Cminor translation.



@2722

7 years 
campbell 
It's easier to keep the real function identifier in frontend …



@2677

7 years 
campbell 
Retain the pointer for the function called in frontend call states
so …



@2645

7 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2624

7 years 
campbell 
Properly evict unused and axiomatised Floats.



@2608

7 years 
garnier 
Regions are no more stored in blocks. block_region now tests the id, …



@2601

7 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2598

7 years 
garnier 
Tentative, partial draft for the definition of ClightCminor …



@2597

7 years 
campbell 
Some work in progress on measurable subtrace preservation.



@2511

7 years 
campbell 
Conjecture main Cminor/RTLabs simulation results.
Add a few notes …



@2496

7 years 
garnier 
Some tentative work on the simulation proof for expressions, in order …



@2489

7 years 
campbell 
Conjecture some Clight/Cminor? simulation results.



@2468

7 years 
garnier 
Floats are gone from the frontend. Some trace amount might remain in …



@2395

7 years 
campbell 
Proper handling of comparison of pointers offtheend of an object.
We …



@2390

7 years 
campbell 
Tidy up a corner case when generating RTLabs so that we generate
less …



@2384

7 years 
campbell 
Move Matita pretty printers into place.



@2335

7 years 
campbell 
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …



@2319

7 years 
campbell 
Generate perprogram cost labels rather than perfunction ones, and …



@2292

7 years 
campbell 
More RTLabs invariants.



@2289

7 years 
campbell 
Update alias



@2287

7 years 
campbell 
RTLabs typing for loads and stores.



@2254

7 years 
campbell 
Fix up invariants in Cminor semantics.



@2253

7 years 
campbell 
Cminor to RTLabs is now a total function.



@2252

7 years 
campbell 
Use the return statement invariant. Restructure the invariants for …



@2251

7 years 
campbell 
Add new invariant to Cminor that return typs should be respected.



@2249

7 years 
campbell 
Tweak Cminor invariant to be slightly more readable/extendable.



@2232

7 years 
campbell 
Remove unused block structure in Cminor.



@2178

7 years 
campbell 
Shift some notation into utilities.



@2176

7 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2103

7 years 
campbell 
Make transform_*program take a more general transformation to make …



@2033

7 years 
sacerdot 
Daemon reverted.



@2032

7 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@1993

7 years 
campbell 
Make frontend memory model only depend on the general definitions by …



@1988

7 years 
campbell 
Abstraction of the memory contents in the memory models is no longer …



@1986

7 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1884

8 years 
campbell 
Syntax changes to fit Paolo's commit.



@1878

8 years 
campbell 
Enforce typing of constants in frontend, plus binops for RTLabs.



@1874

8 years 
campbell 
First cut at using backend memory model throughout.
Note the …



@1872

8 years 
campbell 
Make binary operations in Cminor/RTLabs properly typed.
A few extra …



@1713

8 years 
campbell 
Add a distinguished final state to the frontend languages to match up …



@1680

8 years 
campbell 
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …



@1655

8 years 
campbell 
Update Cminor and RTLabs semantics to use new monad definitions.



@1633

8 years 
campbell 
Update Cminor pretty printer and examples.



@1631

8 years 
campbell 
Use fact that type environments in Cminor have distinct variables to …



@1626

8 years 
campbell 
Add extra type safety in front end. NB: critical freshness parts …



@1611

8 years 
sacerdot 
All of Cminor now compiles with the latest lib of Matita.



@1610

8 years 
sacerdot 
Ported to new lib.



@1608

8 years 
sacerdot 
Porting to new library still in progress.



@1605

8 years 
sacerdot 
Porting to last standard library of Matita.



@1603

8 years 
sacerdot 
More proofs ported to new lib.



@1599

8 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1521

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



@1516

8 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1464

8 years 
campbell 
Use unification hints to simplify the graph monotonicity proofs.



@1410

8 years 
campbell 
Remove a few old workarounds.



@1401

8 years 
ricciott 
Changes concerning the new behavior of destruct.



@1369

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



@1352

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



@1351

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



@1316

8 years 
campbell 
Merge in idlookupbranch to trunk.



@1238

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



@1226

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



@1224

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



@1157

8 years 
campbell 
Update pretty printers and examples.



@1147

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



@1139

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



@1072

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



@1070

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



@1056

8 years 
campbell 
Switch to delayed identifier error scheme.



@966

8 years 
campbell 
Update Cminor pretty printer and some examples.



@961

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



@898

8 years 
campbell 
Update pretty printers and examples.



@888

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



@887

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



@886

8 years 
campbell 
Put types into parameter and variable lists in Cminor.
Temporarily …



@881

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



@880

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



@879

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



@878

8 years 
campbell 
Removal of manually inserted record projections.



@816

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



@797

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



@790

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



@780

8 years 
campbell 
Properly update set of registers that are used for pointers in Cminor …



@776

8 years 
campbell 
Fix up some minor null pointer issues in Clight.
Add corresponding …



@772

8 years 
campbell 
Implement proper support for RTLabs addressing modes.



@771

8 years 
campbell 
Implement switch statements in Cminor > RTLabs phase



@770

8 years 
campbell 
Clight and Cminor examples for switch statement.



@768

8 years 
campbell 
Make Cminor tests test translation to RTLabs.



@767

8 years 
campbell 
Use variable shadowing as a poor man's state monad in cminor to rtlabs …



@766

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


