diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c index e8eda467f288b9461285f737f220bff999e0243f..8f763f8658ee024a5764ed2177ccf2c0ff692b6f 100644 --- a/tests/libc/coverage.c +++ b/tests/libc/coverage.c @@ -1,6 +1,6 @@ /* run.config* PLUGIN: @PTEST_PLUGIN@ metrics - OPT: -eva-no-builtins-auto @EVA_OPTIONS@ @PTEST_SHARE_DIR@/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc + 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/fc_libc.c b/tests/libc/fc_libc.c index debe6f55696331ced5bb625a11b285dbec6a506c..f7f6b24ecaeb7b426ac9a6663366cfb7576b30a0 100644 --- a/tests/libc/fc_libc.c +++ b/tests/libc/fc_libc.c @@ -1,8 +1,8 @@ /* run.config* PLUGIN: @EVA_PLUGINS@ metrics - EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' @PTEST_FILE@ -save @PTEST_NAME@.sav >@PTEST_NAME@_sav.res 2>@PTEST_NAME@_sav.err + EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc' @PTEST_FILE@ -save @PTEST_NAME@.sav >@PTEST_NAME@_sav.res 2>@PTEST_NAME@_sav.err MODULE: check_libc_naming_conventions, check_const - OPT: -load %{dep:@PTEST_NAME@.sav} -print -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' -eva @EVA_CONFIG@ -then -lib-entry -no-print + OPT: -load %{dep:@PTEST_NAME@.sav} -print -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc' -eva @EVA_CONFIG@ -then -lib-entry -no-print MODULE: OPT: -print -print-libc -machdep x86_32 MODULE: check_parsing_individual_headers @@ -13,7 +13,7 @@ OPT: -kernel-msg-key printer:attrs MODULE: OPT: -load %{dep:@PTEST_NAME@.sav} -metrics -metrics-libc -then -lib-entry -metrics-no-libc | ./check_some_metrics.sh "> 100" "> 400" "< 2" "> 20" "= 1" "= 1" "= 0" "= 0" "= 0" "= 1" - CMD: %{dep:./check_full_libc.sh} @PTEST_SHARE_DIR@/libc + CMD: %{dep:./check_full_libc.sh} @FRAMAC_SHARE@/libc OPT: **/ #define __FC_REG_TEST diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c index 05600e9550914c4df46a46b4c5ee321fd43f6e38..ec7f02cf510f4293be5c1215a9fc6d403eae49ef 100644 --- a/tests/libc/runtime.c +++ b/tests/libc/runtime.c @@ -1,6 +1,6 @@ /* run.config* COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...) - CMD: gcc -D__FC_MACHDEP_X86_64 @PTEST_SHARE_DIR@/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@ + CMD: gcc -D__FC_MACHDEP_X86_64 @FRAMAC_SHARE@/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@ OPT: */ diff --git a/tests/libc/string_c_generic.c b/tests/libc/string_c_generic.c index e139d9e467d58148978c85c48be979fbe5a0030d..e09a90a447cf70bdf484fb3c4af31bbf2a308f0e 100644 --- a/tests/libc/string_c_generic.c +++ b/tests/libc/string_c_generic.c @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include@PTEST_SHARE_DIR@/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 4f1bd74747d116b089e6d0598cb2522e83263518..ee5473aa46e32dec6fcef85cb690df992a9df116 100644 --- a/tests/libc/string_c_strchr.c +++ b/tests/libc/string_c_strchr.c @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-cpp-extra-args=-include@PTEST_SHARE_DIR@/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 14f2597d49ab7e8c9417ac50aa31a84f2c275b82..fa321518a52a0966f3db7de4198da0684cbc22fd 100644 --- a/tests/libc/string_c_strstr.c +++ b/tests/libc/string_c_strstr.c @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-cpp-extra-args=-include@PTEST_SHARE_DIR@/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/libc/test_config b/tests/libc/test_config index 7ffaf3b052ad072e5dd60b64156040e8d2789475..38ea17980aea0c9aaacc4ae9e469b89269390763 100644 --- a/tests/libc/test_config +++ b/tests/libc/test_config @@ -1,2 +1,2 @@ PLUGIN: @EVA_PLUGINS@ -OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' +OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc'