diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 12:34:43 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 12:34:43 +0000 |
commit | 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 (patch) | |
tree | 4e1422ea2a810520d0d9b0fbb78c0014ba9f8443 /test/spass/Makefile | |
parent | 93d89c2b5e8497365be152fb53cb6cd4c5764d34 (diff) | |
download | compcert-6c196ec8a41d6ed506c133c8b33dba9684f9a7a6.tar.gz compcert-6c196ec8a41d6ed506c133c8b33dba9684f9a7a6.zip |
Updated raytracer test. Added SPASS test.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'test/spass/Makefile')
-rw-r--r-- | test/spass/Makefile | 34 |
1 files changed, 34 insertions, 0 deletions
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 |