|
|
|
@2896
|
8 years |
campbell |
Complete part of measurable to structured subtraces proof that
shows …
|
|
|
|
@2895
|
8 years |
campbell |
Match up function id from RTLabs Callstate with shadow stack,
use in …
|
|
|
|
@2722
|
8 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2624
|
8 years |
campbell |
Properly evict unused and axiomatised Floats.
|
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2471
|
8 years |
campbell |
Tame global environments a little.
|
|
|
|
@2468
|
8 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
|
@2439
|
8 years |
campbell |
Get a proper reverse mapping of function blocks to identifiers by …
|
|
|
|
@2415
|
8 years |
campbell |
Add the ability to map blocks to symbols in preparation for stack space.
|
|
|
|
@2319
|
9 years |
campbell |
Generate per-program cost labels rather than per-function ones, and …
|
|
|
|
@2226
|
9 years |
campbell |
Whole program proof.
|
|
|
|
@2185
|
9 years |
campbell |
Use bitvectors for offsets.
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2117
|
9 years |
campbell |
Workaround for bug in Matita.
|
|
|
|
@2107
|
9 years |
campbell |
Memory initialisation and program transformations.
|
|
|
|
@2105
|
9 years |
campbell |
Show some results about globalenvs and program transformations.
|
|
|
|
@2010
|
9 years |
campbell |
Make globalenvs use proper maps.
|
|
|
|
@1999
|
9 years |
campbell |
Make back-end use the main global envs.
|
|
|
|
@1994
|
9 years |
campbell |
Remove redundant allocation definition in Globalenvs.
|
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
|
@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 …
|
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1599
|
9 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1583
|
9 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
|
@1545
|
9 years |
campbell |
Use pointer record in front-end.
|
|
|
|
@1395
|
9 years |
sacerdot |
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
|
|
|
|
@1231
|
10 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
|
@1224
|
10 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1139
|
10 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@758
|
10 years |
campbell |
Implement replacement of global var initialisation data by code in Cminor.
|
|
|
|
@747
|
10 years |
campbell |
Merge the two AST files together (although some definitions still need …
|
|
|
|
@744
|
10 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@700
|
10 years |
campbell |
Get Clight semantics going again (except for problems CexecEquiv? that …
|
|
|
|
@695
|
10 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
copied from src/Clight/Globalenvs.ma:
|
|
|
|
@694
|
10 years |
campbell |
Start moving Clight into common directory.
|
