From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/Makefile | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 test/spass/Makefile (limited to 'test/spass/Makefile') diff --git a/test/spass/Makefile b/test/spass/Makefile new file mode 100644 index 00000000..b9647707 --- /dev/null +++ b/test/spass/Makefile @@ -0,0 +1,34 @@ +CC=../../ccomp +CFLAGS=-stdlib ../../runtime -dparse -dclight -dasm -fstruct-passing -fstruct-assign + +SRCS=analyze.c clause.c clock.c closure.c cnf.c component.c \ + condensing.c context.c defs.c dfgparser.c dfgscanner.c doc-proof.c \ + flags.c foldfg.c graph.c hash.c hasharray.c iaparser.c iascanner.c \ + kbo.c list.c memory.c misc.c options.c order.c partition.c \ + proofcheck.c renaming.c resolution.c rpos.c rules-inf.c rules-red.c \ + rules-sort.c rules-split.c rules-ur.c search.c sharing.c sort.c st.c \ + stack.c strings.c subst.c subsumption.c symbol.c table.c tableau.c \ + term.c terminator.c top.c unify.c vector.c + +all: spass + +spass: $(SRCS:.c=.o) + $(CC) $(CFLAGS) -o spass $(SRCS:.c=.o) + +clean: + rm -f spass + rm -f *.o *.s *.parsed.c *.light.c + +test: + ./spass small_problem.dfg | grep 'Proof found' + +TIME=xtime -o /dev/null # Xavier's hack +#TIME=time >/dev/null # Otherwise + +bench: + $(TIME) ./spass problem.dfg + +depend: + gcc -MM $(SRCS) > .depend + +include .depend -- cgit