

@2176

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



@2106

8 years 
campbell 
Fix up a couple of proofs broken by recent changes.



@2019

8 years 
campbell 
Split out special induction principle for Clight from soundness file. …



@1988

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



@1876

8 years 
campbell 
Update Cexec soundness proof.
Change finishes_with predicate to …



@1713

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



@1672

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



@1647

9 years 
tranquil 
* corrected some notation problems
* adapted Cligth with slight …



@1545

9 years 
campbell 
Use pointer record in frontend.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1510

9 years 
sacerdot 
All files ported to new dependent inversion.



@1410

9 years 
campbell 
Remove a few old workarounds.



@1350

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



@1342

9 years 
sacerdot 
The new auto is much more powerful.



@1336

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



@1244

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



@1224

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



@1139

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



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



@882

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



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



@744

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



@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/CexecSound.ma:



@500

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