From 28eaec9986f47a9354a1f7a82eeda968d9ed4f07 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 19 Mar 2021 15:39:07 +0100
Subject: [PATCH] [Ptests] homogeneous workaround about acces to frama-c share"
---
tests/jcdb/jcdb.c | 4 ++++
tests/libc/coverage.c | 2 +-
tests/libc/runtime.c | 4 ++--
tests/libc/string_c_generic.c | 4 ++--
tests/libc/string_c_strchr.c | 4 ++--
tests/libc/string_c_strstr.c | 4 ++--
6 files changed, 13 insertions(+), 9 deletions(-)
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index 2c92c84fd99..a853b488b31 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 ad572429325..095d4b93ae6 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 8c3522845b4..5534de98b5b 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 0939e6721a7..eae5c35cb25 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 a94bf5f192f..b9a07386013 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 9f4e89d682b..28b3bdf7843 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:
--
GitLab