Revised Stacking and Asmgen passes and Mach semantics:

- no more prediction of return addresses (Asmgenretaddr is gone)
- instead, punch a hole for the retaddr in Mach stack frame and
  fill this hole with the return address in the Asmgen proof.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 3 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 4992098..4dfbe48 100644
--- a/Makefile
+++ b/Makefile
@@ -86,10 +86,9 @@ BACKEND=\
   Linear.v Lineartyping.v \
   Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \
   RRE.v RREproof.v RREtyping.v \
-  Mach.v Machtyping.v \
-  Bounds.v Stacklayout.v Stacking.v Stackingproof.v Stackingtyping.v \
-  Machsem.v \
-  Asm.v Asmgen.v Asmgenretaddr.v Asmgenproof1.v Asmgenproof.v
+  Mach.v \
+  Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
+  Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v
 
 # C front-end modules (in cfrontend/)