

@1369

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



@1352

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 …



@1344

10 years 
sacerdot 
Ported to new destruct.



@1342

10 years 
sacerdot 
The new auto is much more powerful.



@1336

10 years 
sacerdot 
Ported to new Matita destruct/inversion.
One lemma fails at qed. …



@1332

10 years 
campbell 
Summation example updated (needs computational K).



@1316

10 years 
campbell 
Merge in idlookupbranch to trunk.



@1276

10 years 
campbell 
Support for replacing operations with runtime support functions in …



@1244

10 years 
campbell 
Sort out Clight semantics equivalence proof for new SmallstepExec?.



@1238

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



@1231

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



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



@1216

10 years 
campbell 
Update Clight semantics equivalence proof to match changes in …



@1207

10 years 
campbell 
Second part of fixing temporaries in Clight to Cminor stage.



@1206

10 years 
campbell 
First stage of fixing temporary generation in Clight/toCminor.ma.



@1198

10 years 
campbell 
Clight cast removal (NB: quite different from the prototype).



@1194

10 years 
campbell 
Remove old, commented out code.



@1157

10 years 
campbell 
Update pretty printers and examples.



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



@1078

10 years 
campbell 
Implement stack allocation for parameters whose address is taken.



@1058

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



@1056

10 years 
campbell 
Switch to delayed identifier error scheme.



@978

10 years 
campbell 
Update remaining Clight examples.



@965

10 years 
campbell 
Update some Clight examples.



@964

10 years 
campbell 
Rest of cast fix.



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



@886

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



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



@824

10 years 
campbell 
Some work on showing that casts around integer operations can be removed.



@816

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



@798

10 years 
campbell 
Fix usual matita tactic mistake.



@797

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



@786

10 years 
campbell 
A version of the clight matita term printer for the current prototype.



@781

11 years 
campbell 
Implement labelling pass for Clight.



@776

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



@770

11 years 
campbell 
Clight and Cminor examples for switch statement.



@758

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



@748

11 years 
campbell 
Change example statement for easier testing.



@747

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



@744

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



@738

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



@737

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



@732

11 years 
campbell 
Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma



@731

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



@726

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



@725

11 years 
campbell 
Do some light manual disambiguation to make Clight examples go through …



@720

11 years 
campbell 
Sort out cost labels.



@718

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



@717

11 years 
campbell 
Clean up Clight examples; better temporary definition of multiply.



@708

11 years 
campbell 
Use a more normalizefriendly definition of clight_exec to make the …



@707

11 years 
campbell 
Remove old branch, which was merged after the move to src.



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



@697

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



@695

11 years 
campbell 
Rearrange Clight files a bit  will try to make them work again soon…



@694

11 years 
campbell 
Start moving Clight into common directory.


copied from Deliverables/D3.1/Csemantics:



@693

11 years 
campbell 
Separate out whole program executions from the clight semantics and …
