From 4af1682d04244bab9f793e00eb24090153a36a0f Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Jul 2011 12:51:16 +0000 Subject: Added animation of the CompCert C semantics (ccomp -interp) test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c90b9d6..81d339f 100644 --- a/Makefile +++ b/Makefile @@ -71,7 +71,7 @@ BACKEND=\ # C front-end modules (in cfrontend/) -CFRONTEND=Csyntax.v Csem.v Cstrategy.v \ +CFRONTEND=Csyntax.v Csem.v Cstrategy.v Cexec.v \ Initializers.v Initializersproof.v \ SimplExpr.v SimplExprspec.v SimplExprproof.v \ Clight.v Cshmgen.v Cshmgenproof.v \ @@ -114,7 +114,7 @@ ccomp.byte: driver/Configuration.ml runtime: $(MAKE) -C runtime -.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte runtime +.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte cinterp cinterp.byte runtime all: $(MAKE) proof -- cgit v1.2.3