|
|
|
@2722
|
7 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
|
@2677
|
7 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2608
|
7 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2588
|
7 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
|
@2569
|
7 years |
campbell |
Fix Clight semantics for ptr + char. (Compiler works anyway.)
|
|
|
|
@2560
|
7 years |
garnier |
Fix in trace gen for CL
|
|
|
|
@2468
|
7 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
|
@2433
|
7 years |
campbell |
Tidy up Clight pointer comparison.
|
|
|
|
@2429
|
7 years |
garnier |
Restrict semantics of pointer comparison to what CompCert? does - i.e. …
|
|
|
|
@2428
|
7 years |
campbell |
Tighten requirements on switch statements in Clight to only give …
|
|
|
|
@2395
|
7 years |
campbell |
Proper handling of comparison of pointers off-the-end of an object.
We …
|
|
|
|
@2391
|
7 years |
campbell |
Revert "Put the post-loop cost label into the Clight while statement …
|
|
|
|
@2353
|
7 years |
campbell |
Put the post-loop cost label into the Clight while statement to get …
|
|
|
|
@2263
|
7 years |
garnier |
Finished proving semantics preservation under memory injections for …
|
|
|
|
@2177
|
8 years |
campbell |
Tidy up multiplication.
|
|
|
|
@2176
|
8 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2032
|
8 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
|
@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.
|
|
|
|
@1914
|
8 years |
campbell |
Fix bug in Clight semantics that misses goto-labels inside a cost …
|
|
|
|
@1874
|
8 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1872
|
8 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1713
|
8 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
|
@1672
|
8 years |
campbell |
Matita now generates a couple of inversion lemmas that were manually …
|
|
|
|
@1545
|
8 years |
campbell |
Use pointer record in front-end.
|
|
|
|
@1231
|
8 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
|
@1147
|
8 years |
campbell |
Remove some obsolete commented out code, update a couple of comments.
|
|
|
|
@1139
|
8 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 …
|
|
|
|
@816
|
9 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@776
|
9 years |
campbell |
Fix up some minor null pointer issues in Clight.
Add corresponding …
|
|
|
|
@744
|
9 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@725
|
9 years |
campbell |
Do some light manual disambiguation to make Clight examples go through …
|
|
|
|
@717
|
9 years |
campbell |
Clean up Clight examples; better temporary definition of multiply.
|
|
|
|
@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/C-semantics/Csem.ma:
|
|
|
|
@648
|
9 years |
campbell |
Oops, wrong bitvector negation.
|
