

@2677

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



@2588

7 years 
garnier 
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …



@2468

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



@2428

7 years 
campbell 
Tighten requirements on switch statements in Clight to only give …



@2391

8 years 
campbell 
Revert "Put the postloop cost label into the Clight while statement …



@2353

8 years 
campbell 
Put the postloop cost label into the Clight while statement to get …



@2176

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



@2120

8 years 
campbell 
Fix victim of alloc unfolding.



@1930

8 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1713

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



@1672

8 years 
campbell 
Matita now generates a couple of inversion lemmas that were manually …



@1603

8 years 
sacerdot 
More proofs ported to new lib.



@1566

8 years 
campbell 
Pacify changes to destruct tactic.



@1545

8 years 
campbell 
Use pointer record in frontend.



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



@1510

8 years 
sacerdot 
All files ported to new dependent inversion.



@1244

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



@1058

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



@961

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



@891

9 years 
campbell 
Revise proofs affected by recent matita change.



@879

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



@797

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



@726

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



@708

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



@700

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



@694

9 years 
campbell 
Start moving Clight into common directory.


copied from Deliverables/D3.1/Csemantics/CexecComplete.ma:



@500

9 years 
campbell 
Use dependent pointer type to ensure that the representation is always …
