From dba986fa06137e07dcff1bdd0a4839eed424bcb9 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 6 Oct 2021 17:26:03 +0200
Subject: [PATCH] [Tests] using @FRAMA_SHARE@ macro
---
tests/compliance/check-json.i | 3 ++-
tests/jcdb/jcdb.c | 2 +-
tests/libc/coverage.c | 6 +++---
tests/libc/runtime.c | 8 ++++----
tests/libc/string_c_generic.c | 2 +-
tests/libc/string_c_strchr.c | 2 +-
tests/libc/string_c_strstr.c | 2 +-
tests/misc/bts0541.c | 4 ++--
tests/spec/clash_double_file_bts1598.c | 4 ++--
tests/syntax/multiple_decls_contracts.c | 12 ++++++------
tests/syntax/offset.c | 4 ++--
11 files changed, 25 insertions(+), 24 deletions(-)
diff --git a/tests/compliance/check-json.i b/tests/compliance/check-json.i
index e6ae724ab7b..9aedb6eaca8 100644
--- a/tests/compliance/check-json.i
+++ b/tests/compliance/check-json.i
@@ -1,5 +1,6 @@
/*run.config
-MACRO: SHARE @FRAMAC_SHARE@/compliance
+ COMMENT: dependency to FRAMA-C share directory is implicit
+ MACRO: SHARE @FRAMAC_SHARE@/compliance
NOFRAMAC:
EXECNOW: LOG json_@PTEST_NAME@_1.txt python3 -m json.tool < @SHARE@/c11_functions.json | head -n 2 > json_@PTEST_NAME@_1.txt 2> @DEV_NULL@
EXECNOW: LOG json_@PTEST_NAME@_2.txt python3 -m json.tool < @SHARE@/glibc_functions.json | head -n 2 > json_@PTEST_NAME@_2.txt 2> @DEV_NULL@
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index 1c3eb23e2d5..eb3d139f636 100644
--- a/tests/jcdb/jcdb.c
+++ b/tests/jcdb/jcdb.c
@@ -6,7 +6,7 @@ DEPS: jcdb2.c with_arguments.json compile_commands.json file_without_main.c
MODULE: @PTEST_NAME@
OPT: -json-compilation-database with_arguments.json
MODULE:
- EXECNOW: LOG list_files.res LOG list_files.err ../../../../install/default/share/frama-c/share/analysis-scripts/list_files.py %{dep:compile_commands_working.json} > list_files.res 2> list_files.err
+ EXECNOW: LOG list_files.res LOG list_files.err @FRAMAC_SHARE@/analysis-scripts/list_files.py %{dep:compile_commands_working.json} > list_files.res 2> list_files.err
*/
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 095d4b93ae6..bb6de20c397 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,7 +1,7 @@
/* run.config*
- COMMENT: dependency to FRAMA-C share directory is implicit
- PLUGIN: metrics @EVA_PLUGINS@
- OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../../../install/default/share/frama-c/share/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
+ COMMENT: dependency to FRAMA-C share directory is implicit
+ PLUGIN: metrics @EVA_PLUGINS@
+ OPT: -eva-no-builtins-auto @EVA_OPTIONS@ @FRAMAC_SHARE@/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
#include "string.h"
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
index 4f14c569822..b353d89f4cc 100644
--- a/tests/libc/runtime.c
+++ b/tests/libc/runtime.c
@@ -1,8 +1,8 @@
/* run.config*
- COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
- COMMENT: dependency to FRAMA-C share directory is implicit
- CMD: gcc @PTEST_OPTIONS@
- OPT: -D__FC_MACHDEP_X86_64 ../../../../install/default/share/frama-c/share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o @DEV_NULL@ @PTEST_FILE@
+ COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
+ COMMENT: dependency to FRAMA-C share directory is implicit
+ CMD: gcc @PTEST_OPTIONS@
+ OPT: -D__FC_MACHDEP_X86_64 @FRAMAC_SHARE@/libc/__fc_runtime.c -Wno-attributes -std=c99 -o @DEV_NULL@ @PTEST_FILE@
*/
int main() {
diff --git a/tests/libc/string_c_generic.c b/tests/libc/string_c_generic.c
index eae5c35cb25..986afc994a3 100644
--- a/tests/libc/string_c_generic.c
+++ b/tests/libc/string_c_generic.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: dependency to FRAMA-C share directory is implicit
- STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include../../../../install/default/share/frama-c/share/libc/string.c -eva-slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
+ STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include@FRAMAC_SHARE@/libc/string.c -eva-slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/libc/string_c_strchr.c b/tests/libc/string_c_strchr.c
index b9a07386013..9832b705167 100644
--- a/tests/libc/string_c_strchr.c
+++ b/tests/libc/string_c_strchr.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: dependency to FRAMA-C share directory is implicit
- STDOPT: #"-cpp-extra-args=-include../../../../install/default/share/frama-c/share/libc/string.c -eva-slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
+ STDOPT: #"-cpp-extra-args=-include@FRAMAC_SHARE@/libc/string.c -eva-slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/libc/string_c_strstr.c b/tests/libc/string_c_strstr.c
index 28b3bdf7843..2d606eafb55 100644
--- a/tests/libc/string_c_strstr.c
+++ b/tests/libc/string_c_strstr.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: dependency to FRAMA-C share directory is implicit
- STDOPT: #"-cpp-extra-args=-include../../../../install/default/share/frama-c/share/libc/string.c -eva-slevel-function strstr:30 -eva-no-skip-stdlib-specs"
+ STDOPT: #"-cpp-extra-args=-include@FRAMAC_SHARE@/libc/string.c -eva-slevel-function strstr:30 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/misc/bts0541.c b/tests/misc/bts0541.c
index 213d4e2cd99..2258c905922 100644
--- a/tests/misc/bts0541.c
+++ b/tests/misc/bts0541.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -pp-annot -cpp-extra-args="-I./share/libc" -pp-annot -eva @EVA_OPTIONS@
+ MACRO: LIBC @FRAMAC_SHARE@/LIBC
+ OPT: -pp-annot -cpp-extra-args="-I@LIBC@" -pp-annot -eva @EVA_OPTIONS@
*/
-
#include <stdbool.h>
#include <stdint.h>
#include <stdlib.h>
diff --git a/tests/spec/clash_double_file_bts1598.c b/tests/spec/clash_double_file_bts1598.c
index 37446ed82f5..a588243239b 100644
--- a/tests/spec/clash_double_file_bts1598.c
+++ b/tests/spec/clash_double_file_bts1598.c
@@ -1,9 +1,9 @@
/* run.config
COMMENT: checks that linking string.h and its FC-pretty-printed version
COMMENT: does not get rejected by name clash in the logic. See bts 1598
-OPT: -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then @PTEST_FILE@ ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print
+ MACRO: LIBC @FRAMAC_SHARE@/libc
+ OPT: -cpp-extra-args " -I@LIBC@ -nostdinc" -print -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then @PTEST_FILE@ ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print
*/
-
#include "__fc_builtin.h"
#include "assert.h"
//#include "complex.h"
diff --git a/tests/syntax/multiple_decls_contracts.c b/tests/syntax/multiple_decls_contracts.c
index ab9b7a4c3b6..75a8c3046e9 100644
--- a/tests/syntax/multiple_decls_contracts.c
+++ b/tests/syntax/multiple_decls_contracts.c
@@ -1,13 +1,13 @@
/* run.config
-CMD: @frama-c-cmd@ @PTEST_OPTIONS@
-OPT: ../../../../install/default/share/frama-c/share/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -print
-OPT: @PTEST_FILE@ ../../../../install/default/share/frama-c/share/libc/string.h @PTEST_FILE@ -print
-OPT: @PTEST_FILE@ @PTEST_FILE@ ../../../../install/default/share/frama-c/share/libc/string.h -print
+ COMMENT: dependency to FRAMA-C share directory is implicit
+ MACRO: LIBC @FRAMAC_SHARE@/libc
+ CMD: @frama-c-cmd@ @PTEST_OPTIONS@
+ OPT: @LIBC@/string.h @PTEST_FILE@ @PTEST_FILE@ -print
+ OPT: @PTEST_FILE@ @LIBC@/string.h @PTEST_FILE@ -print
+ OPT: @PTEST_FILE@ @PTEST_FILE@ @LIBC@/string.h -print
*/
-
#include "string.h"
#include "stdlib.h"
-
char *
strdup(const char *str)
{
diff --git a/tests/syntax/offset.c b/tests/syntax/offset.c
index 271b4450362..7244aff6788 100644
--- a/tests/syntax/offset.c
+++ b/tests/syntax/offset.c
@@ -1,7 +1,7 @@
/* run.config
-OPT: -cpp-extra-args="-Ishare/libc" -print
+ COMMENT: dependency to FRAMA-C share directory is implicit
+ OPT: -cpp-extra-args="-I@FRAMAC_SHARE@/libc" -print
*/
-
#include "__fc_define_off_t.h"
off_t x = 0;
--
GitLab