

@2203

8 years 
campbell 
A general result about simulations of executions.



@2176

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



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



@1986

8 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1874

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



@1713

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



@1647

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



@1603

9 years 
sacerdot 
More proofs ported to new lib.



@1599

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



@1545

9 years 
campbell 
Use pointer record in frontend.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1244

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



@1231

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



@1147

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



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



@964

9 years 
campbell 
Rest of cast fix.



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



@880

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



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



@731

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



@725

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



@718

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



@708

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



@702

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



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



@693

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