Merge of the newmem and newextcalls branches:
- Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 52 additions, 51 deletions.depend
- Makefile 2 additions, 2 deletionsMakefile
- arm/Asm.v 7 additions, 7 deletionsarm/Asm.v
- arm/Asmgen.v 1 addition, 1 deletionarm/Asmgen.v
- arm/Asmgenproof.v 1 addition, 1 deletionarm/Asmgenproof.v
- arm/Asmgenproof1.v 1 addition, 1 deletionarm/Asmgenproof1.v
- arm/Asmgenretaddr.v 1 addition, 1 deletionarm/Asmgenretaddr.v
- arm/ConstpropOpproof.v 1 addition, 1 deletionarm/ConstpropOpproof.v
- arm/Op.v 13 additions, 13 deletionsarm/Op.v
- arm/SelectOp.v 1 addition, 1 deletionarm/SelectOp.v
- arm/SelectOpproof.v 1 addition, 1 deletionarm/SelectOpproof.v
- backend/Allocproof.v 11 additions, 12 deletionsbackend/Allocproof.v
- backend/CSE.v 2 additions, 2 deletionsbackend/CSE.v
- backend/CSEproof.v 24 additions, 27 deletionsbackend/CSEproof.v
- backend/Cminor.v 37 additions, 28 deletionsbackend/Cminor.v
- backend/CminorSel.v 19 additions, 15 deletionsbackend/CminorSel.v
- backend/Constpropproof.v 27 additions, 30 deletionsbackend/Constpropproof.v
- backend/LTL.v 13 additions, 11 deletionsbackend/LTL.v
- backend/LTLin.v 15 additions, 13 deletionsbackend/LTLin.v
- backend/LTLintyping.v 1 addition, 0 deletionsbackend/LTLintyping.v
Loading
Please register or sign in to comment