diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c index 01abb7fe331a01e6e7a773cc21ac35d78206b525..b6249280cb5f01666a059cae1f6b5a5bfcd56b0a 100644 --- a/tests/libc/coverage.c +++ b/tests/libc/coverage.c @@ -1,7 +1,6 @@ /* run.config* PLUGIN: metrics - DEPS: ../../../share/libc/string.c - OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../../share/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc + OPT: -eva-no-builtins-auto @EVA_OPTIONS@ %{read:../../syntax/framac_share_path}/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc */ #include "string.h" diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle index 674a938e982f0cf1f6d53861960c95fab45dd5c0..3dd7624cf245d4f2284d152f0317e41a006620b6 100644 --- a/tests/libc/oracle/coverage.res.oracle +++ b/tests/libc/oracle/coverage.res.oracle @@ -1,12 +1,12 @@ [kernel] Parsing coverage.c (with preprocessing) -[kernel] Parsing FRAMA-C/share/libc/string.c (with preprocessing) +[kernel] Parsing FRAMAC_SHARE/libc/string.c (with preprocessing) [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed [eva:initial-state] Values of globals at initialization [eva] computing for function strlen <- main. - Called from coverage.c:11. + Called from coverage.c:10. [eva] Recording results for strlen [eva] Done for function strlen [eva] Recording results for main diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c index 38c627a79182c61127642f45f22e84978334a3b8..dcda53f027bd0131b11c92ffe20db6b71ce1afa8 100644 --- a/tests/syntax/cpp-command.c +++ b/tests/syntax/cpp-command.c @@ -1,5 +1,5 @@ /* run.config* - FILTER: sed -e 's:/\(tmp\|var\|build\)/[^ ]*\.i:/tmp/FILE.i:g; s:$PWD::g; s:-I.*share/frama-c/share/libc:-I LIBC:g' + FILTER: sed -e "s:/\(tmp\|var\|build\)/[^ ]*\.i:/tmp/FILE.i:g; s:$PWD:.:g; s:-I.*share/frama-c/share/libc:-I LIBC:g" OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']" OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'" OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\" \"using \\% has no effect : \$(basename \"\%input\")\"" diff --git a/tests/syntax/dune b/tests/syntax/dune new file mode 100644 index 0000000000000000000000000000000000000000..738b7fa0fd885fe9883f3c5bcd0157b83a840646 --- /dev/null +++ b/tests/syntax/dune @@ -0,0 +1,3 @@ +(rule + (action (with-stdout-to framac_share_path (pipe-stdout (run frama-c -print-share-path) (run tr -d '\n')))) +) diff --git a/tests/syntax/multiple_decls_contracts.c b/tests/syntax/multiple_decls_contracts.c index 23b7307cb2645a4d788f44986eec66d2dc33c93c..1b32185cfe8e78368411c15bda76e5b31ff7cea0 100644 --- a/tests/syntax/multiple_decls_contracts.c +++ b/tests/syntax/multiple_decls_contracts.c @@ -1,8 +1,7 @@ /* run.config -DEPS: ../../../share/libc/string.h -OPT: -add-symbolic-path SHARE:../../../share ../../../share/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -print -OPT: -add-symbolic-path SHARE:../../../share @PTEST_FILE@ ../../../share/libc/string.h @PTEST_FILE@ -print -OPT: -add-symbolic-path SHARE:../../../share @PTEST_FILE@ @PTEST_FILE@ ../../../share/libc/string.h -print +OPT:%{read:../framac_share_path}/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -print +OPT: @PTEST_FILE@ %{read:../framac_share_path}/libc/string.h @PTEST_FILE@ -print +OPT: @PTEST_FILE@ @PTEST_FILE@ %{read:../framac_share_path}/libc/string.h -print */ #include "string.h" diff --git a/tests/syntax/oracle/cpp-command.4.res.oracle b/tests/syntax/oracle/cpp-command.4.res.oracle index a85d472a341bae0007a9dee2eea0d46daf63501d..6ed0a35488bf005beac2a2946bb04fb3f761dab8 100644 --- a/tests/syntax/oracle/cpp-command.4.res.oracle +++ b/tests/syntax/oracle/cpp-command.4.res.oracle @@ -1,2 +1,2 @@ [kernel] Preprocessing command: - gcc -E -C -I LIBC -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 'FRAMA-C/tests/syntax/result/cpp-command.c' -o '/tmp/FILE.i' + gcc -E -C -I LIBC -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 './cpp-command.c' -o '/tmp/FILE.i' diff --git a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle index 9d50f76803e83700d56c593b7284ec8f4387a977..49e36a7bc9637e4de1698ba1149b6d9ff51b5f64 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle @@ -1,15 +1,10 @@ -[kernel] Parsing SHARE/libc/string.h (with preprocessing) +[kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) -[kernel] multiple_decls_contracts.c:11: Warning: - dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11 +[kernel] multiple_decls_contracts.c:10: Warning: + dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 /* Generated by Frama-C */ -#include "FRAMA-C/share/libc/__fc_alloc_axiomatic.h" -#include "FRAMA-C/share/libc/__fc_define_size_t.h" -#include "FRAMA-C/share/libc/__fc_define_wchar_t.h" -#include "FRAMA-C/share/libc/__fc_string_axiomatic.h" -#include "FRAMA-C/share/libc/string.h" -#include "FRAMA-C/share/libc/strings.h" +#include "stddef.h" #include "stdlib.h" #include "string.h" #include "strings.h" diff --git a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle index fdbaa0b6edca8027b612043785280b94a0c3c4bc..50638f1cb54fb1518b7f2c83c791765c3baa4be6 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle @@ -1,12 +1,9 @@ [kernel] Parsing multiple_decls_contracts.c (with preprocessing) -[kernel] Parsing SHARE/libc/string.h (with preprocessing) +[kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) -[kernel] multiple_decls_contracts.c:11: Warning: - dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11 +[kernel] multiple_decls_contracts.c:10: Warning: + dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 /* Generated by Frama-C */ -#include "FRAMA-C/share/libc/__fc_alloc_axiomatic.h" -#include "FRAMA-C/share/libc/string.h" -#include "FRAMA-C/share/libc/strings.h" #include "stddef.h" #include "stdlib.h" #include "string.h" diff --git a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle index fa23074d9ee2e35aa9deeb7a7697af756bb1cba6..364dd1fa5a6fd84939e45f8e31186c0869868d77 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle @@ -1,13 +1,9 @@ [kernel] Parsing multiple_decls_contracts.c (with preprocessing) [kernel] Parsing multiple_decls_contracts.c (with preprocessing) -[kernel] Parsing SHARE/libc/string.h (with preprocessing) -[kernel] multiple_decls_contracts.c:11: Warning: - dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11 +[kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing) +[kernel] multiple_decls_contracts.c:10: Warning: + dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 /* Generated by Frama-C */ -#include "FRAMA-C/share/libc/__fc_alloc_axiomatic.h" -#include "FRAMA-C/share/libc/__fc_string_axiomatic.h" -#include "FRAMA-C/share/libc/string.h" -#include "FRAMA-C/share/libc/strings.h" #include "stddef.h" #include "stdlib.h" #include "string.h"