From 277d01d8cb02e7e3d811e24bde95453264adf280 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 25 Aug 2022 16:02:39 +0200
Subject: [PATCH] FRAMAC_WP_(QUALIF|CACHEDIR) must be set to an absolute
pathname
---
bin/test.sh | 9 +++++++--
src/plugins/wp/tests/README.md | 2 ++
2 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index 1b8254771f1..4192edf44b6 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -31,7 +31,7 @@ SAVE=
DUNE_OPT=
DUNE_LOG=./.test-errors.log
-CACHEDIR=./.wp-cache
+CACHEDIR=$(pwd -P)/.wp-cache
FRAMAC_WP_CACHE_GIT=git@git.frama-c.com:frama-c/wp-cache.git
# --------------------------------------------------------------------------
@@ -73,7 +73,7 @@ function Usage
echo ""
echo " FRAMAC_WP_QUALIF"
echo " FRAMAC_WP_CACHEDIR"
- echo " Location of wp-cache ($FRAMAC_WP_CACHEDIR)"
+ echo " Absolute path to wp-cache directory ($FRAMAC_WP_CACHEDIR)"
if [ ! -d $FRAMAC_WP_CACHEDIR ]; then
echo " About to clone from $FRAMAC_WP_CACHE_GIT"
fi
@@ -142,6 +142,11 @@ function SetEnv
[ ! -f "$FRAMAC_WP_CACHEDIR" ] || [ -d "$FRAMAC_WP_CACHEDIR" ] \
|| Error "$FRAMAC_WP_CACHEDIR is not a directory"
+ case "$FRAMAC_WP_CACHEDIR" in
+ /*);;
+ *) Error "Requires an absolute path to $FRAMAC_WP_CACHEDIR";;
+ esac
+
}
function CloneCache
diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index 3d90fddfa98..f1d1bc29cf9 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -48,6 +48,8 @@ The `./bin/test.sh` uses, in order of proprity:
- `FRAMAC_WP_CACHEDIR` environement variable,
- local `./.wp-cache` directory.
+Of course, these environment variables must be set to an absolute path to prevent from different execution locations of Frama-C.
+
It is _not_ recommended to use the `FRAMAC_WP_CACHEDIR` variable in your default
shell setup, unless is it a temporary directory (eg. `/tmp/wp-sandbox`) since
_every_ run of `frama-c -wp` might then use it by default. Be carefull if you do so.
--
GitLab