Reorganized the development, modularizing away machine-dependent parts.
Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 69 additions, 66 deletions.depend
- Makefile 40 additions, 19 deletionsMakefile
- arm/Asmgen.v 554 additions, 0 deletionsarm/Asmgen.v
- arm/Asmgenproof.v 1246 additions, 0 deletionsarm/Asmgenproof.v
- arm/Asmgenproof1.v 1507 additions, 0 deletionsarm/Asmgenproof1.v
- arm/Asmgenretaddr.v 201 additions, 0 deletionsarm/Asmgenretaddr.v
- arm/Constprop.v 1254 additions, 0 deletionsarm/Constprop.v
- arm/Constpropproof.v 970 additions, 0 deletionsarm/Constpropproof.v
- arm/Machregs.v 80 additions, 0 deletionsarm/Machregs.v
- arm/Op.v 1007 additions, 0 deletionsarm/Op.v
- arm/Selection.v 1394 additions, 0 deletionsarm/Selection.v
- arm/Selectionproof.v 1475 additions, 0 deletionsarm/Selectionproof.v
- arm/linux/Conventions.v 858 additions, 0 deletionsarm/linux/Conventions.v
- arm/linux/Stacklayout.v 79 additions, 0 deletionsarm/linux/Stacklayout.v
- backend/CMlexer.mli 0 additions, 0 deletionsbackend/CMlexer.mli
- backend/CMlexer.mll 0 additions, 0 deletionsbackend/CMlexer.mll
- backend/CMparser.mly 0 additions, 0 deletionsbackend/CMparser.mly
- backend/CMtypecheck.ml 0 additions, 0 deletionsbackend/CMtypecheck.ml
- backend/CMtypecheck.mli 0 additions, 0 deletionsbackend/CMtypecheck.mli
- backend/CSE.v 2 additions, 5 deletionsbackend/CSE.v
Loading
Please register or sign in to comment