Updated raytracer test. Added SPASS test.

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

1 files changed, 34 insertions, 0 deletions

diff --git a/test/spass/Makefile b/test/spass/Makefile
new file mode 100644
index 0000000..b964770
--- /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