diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-08 23:00:40 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-08 23:00:40 +0100 |
| commit | 0a7eca06548e7261e28ba49679cc2ba4e6851e59 (patch) | |
| tree | 0f050c71616d047074b8b482339edb3270194e27 | |
| parent | 82604915aab691007abfa937fd5e90d646332034 (diff) | |
| download | vericert-kvx-0a7eca06548e7261e28ba49679cc2ba4e6851e59.tar.gz vericert-kvx-0a7eca06548e7261e28ba49679cc2ba4e6851e59.zip | |
Fix running of tests using a Makefile
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | test/Makefile | 34 |
2 files changed, 36 insertions, 1 deletions
@@ -54,7 +54,7 @@ doc: Makefile.coq extraction: src/extraction/STAMP test: - ./test/test_all.sh ./test + $(MAKE) -C test compile: src/extraction/STAMP @echo "OCaml bin/vericert" @@ -73,6 +73,7 @@ Makefile.coq: clean:: Makefile.coq $(MAKE) -f Makefile.coq clean + $(MAKE) -C test clean rm -f Makefile.coq clean:: diff --git a/test/Makefile b/test/Makefile new file mode 100644 index 0000000..f161386 --- /dev/null +++ b/test/Makefile @@ -0,0 +1,34 @@ +CC ?= gcc +VERICERT ?= vericert +VERICERT_OPTS ?= -fschedule +IVERILOG ?= iverilog +IVERILOG_OPTS ?= + +TESTS := $(patsubst %.c,%.check,$(wildcard *.c)) + +all: $(TESTS) + +%.gcc.out: %.gcc + @./$< ; echo "$$?" >$@ + +%.o: %.c + @$(CC) $(CFLAGS) -c $< -o $@ + +%.gcc: %.o + @$(CC) $(CFLAGS) $< -o $@ + +%.v: %.c + @$(VERICERT) $(VERICERT_OPTS) $< -o $@ + +%.iver: %.v + @$(IVERILOG) $(IVERILOG_OPTS) -o $@ -- $< + +%.veri.out: %.iver + @./$< | tail -n1 | sed -r -e 's/[^0-9]*([0-9]+)/\1/' >$@ + +%.check: %.gcc.out %.veri.out + @diff $^ >$@ + @printf "\033[0;36mOK\033[0m\t$(patsubst %.check,%,$@)\n" + +clean: + rm -f *.check *.gcc *.gcc.out *.o *.v *.iver *.veri.out |