|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1986
|
9 years |
campbell |
Get rid of unused abstraction of Globalenvs.
|
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end 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 front-end.
|
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1244
|
10 years |
campbell |
Sort out Clight semantics equivalence proof for new SmallstepExec?.
|
|
|
|
@1231
|
10 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
|
@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 …
|
|
|
|
@1058
|
10 years |
campbell |
Evict CompCert? Maps interface in favour of BitVectorTries?.
|
|
|
|
@964
|
10 years |
campbell |
Rest of cast fix.
|
|
|
|
@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.
|
|
|
|
@880
|
10 years |
campbell |
Add type information into Cminor.
As a result, the Clight to Cminor …
|
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@744
|
10 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@731
|
10 years |
campbell |
Common definition for animation semantics, and factor out IO definitions.
|
|
|
|
@725
|
10 years |
campbell |
Do some light manual disambiguation to make Clight examples go through …
|
|
|
|
@718
|
10 years |
campbell |
Add an AST type (i.e., intermediate language type) for pointers.
|
|
|
|
@708
|
10 years |
campbell |
Use a more normalize-friendly definition of clight_exec to make the …
|
|
|
|
@702
|
10 years |
campbell |
Refine small-step executable semantics abstraction a little.
Some …
|
|
|
|
@700
|
10 years |
campbell |
Get Clight semantics going again (except for problems CexecEquiv? that …
|
|
|
|
@694
|
10 years |
campbell |
Start moving Clight into common directory.
|
|
copied from Deliverables/D3.1/C-semantics/Cexec.ma:
|
|
|
|
@693
|
10 years |
campbell |
Separate out whole program executions from the clight semantics and …
|
