Merging the Princeton implementation of the memory model. Separate axioms in file lib/Axioms.v.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 8 additions, 7 deletions.depend
- Makefile 1 addition, 1 deletionMakefile
- backend/Machabstr2concr.v 1 addition, 0 deletionsbackend/Machabstr2concr.v
- common/Globalenvs.v 1 addition, 0 deletionscommon/Globalenvs.v
- common/Memory.v 498 additions, 260 deletionscommon/Memory.v
- common/Memtype.v 18 additions, 31 deletionscommon/Memtype.v
- driver/Compiler.v 1 addition, 0 deletionsdriver/Compiler.v
- lib/Coqlib.v 4 additions, 1 deletionlib/Coqlib.v
- lib/Integers.v 2 additions, 1 deletionlib/Integers.v
- lib/Iteration.v 1 addition, 0 deletionslib/Iteration.v
- lib/Parmov.v 4 additions, 3 deletionslib/Parmov.v
- powerpc/PrintAsm.ml 7 additions, 4 deletionspowerpc/PrintAsm.ml
Loading
Please register or sign in to comment