diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c index 2c92c84fd993ffebd379ff646c569a9754628652..a853b488b3121d991f4d59ed72268c9f9baafc27 100644 --- a/tests/jcdb/jcdb.c +++ b/tests/jcdb/jcdb.c @@ -1,4 +1,5 @@ /* run.config +COMMENT: dependency to FRAMA-C share directory is implicit DEPS: jcdb2.c with_arguments.json compile_commands.json file_without_main.c CMXS: @PTEST_NAME@ OPT: -json-compilation-database ./ -print @@ -6,6 +7,9 @@ OPT: jcdb2.c -json-compilation-database with_arguments.json -print OPT: -json-compilation-database with_arguments.json -load-module %{dep:@PTEST_NAME@.cmxs} 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 */ + + + #include <stdio.h> #ifdef TOUNDEF diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c index ad5724293253a5e2365b978187cab697e46d37a2..095d4b93ae6681f15af5c0c7b64aac282d18879e 100644 --- a/tests/libc/coverage.c +++ b/tests/libc/coverage.c @@ -1,8 +1,8 @@ /* 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 */ - #include "string.h" void main() { diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c index 8c3522845b4a730f3d91a564c707fc7365124237..5534de98b5bd8408f85718df6f33bb85f8a28217 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, ...) - DEPS: ../../../share/libc/__fc_runtime.c + COMMENT: dependency to FRAMA-C share directory is implicit CMD: gcc @OPTIONS@ - OPT: -D__FC_MACHDEP_X86_64 ../../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null @PTEST_FILE@ + 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@ */ int main() { diff --git a/tests/libc/string_c_generic.c b/tests/libc/string_c_generic.c index 0939e6721a7b4b1df9e339ce7ea5b83e2d33dd2d..eae5c35cb25a52260f5a03cc9fedeb034fda8b18 100644 --- a/tests/libc/string_c_generic.c +++ b/tests/libc/string_c_generic.c @@ -1,6 +1,6 @@ /* run.config - DEPS: ../../../share/libc/string.c - STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include../../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" + 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" */ /* 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 a94bf5f192f22d7d0c40b3c557e5d4fbd98e7929..b9a07386013d87b36bd7e1da7e70f0d5a20952fb 100644 --- a/tests/libc/string_c_strchr.c +++ b/tests/libc/string_c_strchr.c @@ -1,6 +1,6 @@ /* run.config - DEPS: ../../../share/libc/string.c - STDOPT: #"-cpp-extra-args=-include../../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" + 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" */ /* 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 9f4e89d682b66ce5d186405e2bcd91ad75f6a0e1..28b3bdf7843809641ccbb237415a64caadab726c 100644 --- a/tests/libc/string_c_strstr.c +++ b/tests/libc/string_c_strstr.c @@ -1,6 +1,6 @@ /* run.config - DEPS: ../../../share/libc/string.c - STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -eva-slevel-function strstr:30 -eva-no-skip-stdlib-specs" + 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" */ /* This file has been adapted from libc-test, which is licensed under the following standard MIT license: