source: src/common/Globalenvs.ma

Revision Log Mode:


Legend:

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