From d7573df9806e8c69e99d571b1a2024b0657114c1 Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Mon, 8 Feb 2016 10:47:51 +0100 Subject: [PATCH] [tests] prepare GMP tests --- src/plugins/e-acsl/Makefile.in | 2 +- src/plugins/e-acsl/tests/gmp/README.md | 1 + src/plugins/e-acsl/tests/gmp/test_config | 4 ++++ 3 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 src/plugins/e-acsl/tests/gmp/README.md create mode 100644 src/plugins/e-acsl/tests/gmp/test_config diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 91e71e2e0b2..b149e813820 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -116,7 +116,7 @@ ifeq (@MAY_RUN_TESTS@,yes) $(PLUGIN_DIR)/tests/print.cmxs: OFLAGS=-I $(FRAMAC_LIBDIR) $(PLUGIN_DIR)/tests/print.cmo: BFLAGS=-I $(FRAMAC_LIBDIR) -PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime bts +PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime bts gmp E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config \ $(PLUGIN_DIR)/tests/print.cmxs \ $(PLUGIN_DIR)/tests/print.cmo diff --git a/src/plugins/e-acsl/tests/gmp/README.md b/src/plugins/e-acsl/tests/gmp/README.md new file mode 100644 index 00000000000..6ba931bda42 --- /dev/null +++ b/src/plugins/e-acsl/tests/gmp/README.md @@ -0,0 +1 @@ +Like e-acsl-runtime, but also test the -e-acsl-gmp-only mode. diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config new file mode 100644 index 00000000000..8ae28537c63 --- /dev/null +++ b/src/plugins/e-acsl/tests/gmp/test_config @@ -0,0 +1,4 @@ +LOG: gen_@PTEST_NAME@.c +OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results +EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ gmp "" "--frama-c=@frama-c@" +OPT: -check -e-acsl -e-acsl-gmp-only -then-last -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -- GitLab