diff --git a/bin/frama-c-script b/bin/frama-c-script
index 0b1035fe64775973a4df9c614c36fc8c93408d83..7b137a3d4f849a7c4b41c0a68036bf7645651d04 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -85,6 +85,9 @@ if [ $# -lt 1 ]; then
fi
DIR="$( cd "$( dirname "$0" )" && pwd )"
+# All scripts called by frama-c-script may rely on FRAMAC_BIN pointing to the
+# directory containing frama-c, frama-c-config and frama-c-script.
+export FRAMAC_BIN="$DIR"
FRAMAC_SHARE=$("${DIR}/frama-c-config" -share)
if [ -z ${FRAMAC_SESSION+x} ]; then
FRAMAC_SESSION="./.frama-c";
@@ -137,12 +140,12 @@ make_path() {
esac
fi
cat <<EOF > "${dir}/path.mk"
-FRAMAC_DIR=${DIR}
-ifeq (\$(wildcard \$(FRAMAC_DIR)),)
+FRAMAC_BIN=${DIR}
+ifeq (\$(wildcard \$(FRAMAC_BIN)),)
# Frama-C not installed locally; using the version in the PATH
else
-FRAMAC=\$(FRAMAC_DIR)/frama-c
-FRAMAC_GUI=\$(FRAMAC_DIR)/frama-c-gui
+FRAMAC=\$(FRAMAC_BIN)/frama-c
+FRAMAC_GUI=\$(FRAMAC_BIN)/frama-c-gui
endif
EOF
echo "Wrote to: ${dir}/path.mk"
diff --git a/share/analysis-scripts/find_fun.py b/share/analysis-scripts/find_fun.py
index 5cb0b65863adcf8606a34d59d9156200b73a8f39..7324da49ef2db73bb3a0ed87b50c8cd8c426ab8d 100755
--- a/share/analysis-scripts/find_fun.py
+++ b/share/analysis-scripts/find_fun.py
@@ -25,6 +25,7 @@
# This script finds files containing likely declarations and definitions
# for a given function name, via heuristic syntactic matching.
+import argparse
import sys
import os
import re
@@ -35,37 +36,38 @@ MIN_PYTHON = (3, 5) # for glob(recursive)
if sys.version_info < MIN_PYTHON:
sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
-debug = False
+parser = argparse.ArgumentParser(description="""
+Looks for likely declarations/definitions of a function
+in files with extensions '.c', '.h' and '.i'.
+If any directories are specified, looks inside them,
+otherwise looks inside PWD and /usr/include.
+Subdirectories are always considered recursively.""")
-arg = ""
-if len(sys.argv) < 2:
- print("usage: %s fname [dir1 dir2 ...]" % sys.argv[0])
- print(" looks for likely declarations/definitions of function fname")
- print(" in files with extensions '.c', '.h' and '.i';")
- print(" if dir1, dir2, etc, are specified, looks inside them,")
- print(" otherwise looks inside PWD and /usr/include.")
- print(" Subdirectories are always considered recursively.")
- sys.exit(1)
-else:
- fname = sys.argv[1]
- if re.match('[a-zA-Z_][a-zA-Z0-9_]*$', fname) == None:
- print("error: function name contains invalid characters: %s" % fname)
- print(" (only letters/digits/underscore allowed)")
- sys.exit(1)
+parser.add_argument('--directory', '-C', metavar='DIR', default=".", nargs=1,
+ help='print paths relative to directory DIR (default: .)')
+parser.add_argument('funcname', help='function name to search')
+parser.add_argument('dir', nargs='*', help='directories where to search (if empty: PWD /usr/include)')
+args = vars(parser.parse_args())
-dirs = set()
-if len(sys.argv) < 3:
- pwd = os.getcwd()
- dirs = [pwd, "/usr/include"]
-else:
- dirs = set(sys.argv[2:])
+reldir = args["directory"][0]
+fname = args["funcname"]
+dirs = args["dir"]
-if debug:
- print("Looking for files in dirs (and their subdirs): %s" % dirs)
+if re.match('[a-zA-Z_][a-zA-Z0-9_]*$', fname) == None:
+ print("error: function name contains invalid characters: %s" % fname)
+ print(" (only letters/digits/underscore allowed)")
+ sys.exit(1)
+
+dirs = set(dirs)
+if not dirs:
+ pwd = os.getcwd()
+ dirs = [pwd, "/usr/include"]
+else:
+ dirs = set(sys.argv[2:])
files = []
for d in dirs:
- files += glob.glob(d + "/**/*.[ich]", recursive=True)
+ files += glob.glob(d + "/**/*.[ich]", recursive=True)
print("Looking for '%s' inside %d file(s)..." % (fname, len(files)))
@@ -80,14 +82,20 @@ for f in files:
else:
possible_definers.append(f)
+def relative_path_to(start):
+ return lambda p: os.path.relpath(p, start=start)
+
if possible_declarators == [] and possible_definers == []:
- print("No declaration/definition found for function '%s'" % fname)
+ print("No declaration/definition found for function '%s'" % fname)
else:
- if possible_declarators != []:
- print("Possible declarations for function '%s' in the following file(s):"
- % fname)
- print(" " + "\n ".join(map(os.path.relpath, possible_declarators)))
- if possible_definers != []:
- print("Possible definitions for function '%s' in the following file(s):"
- % fname)
- print(" " + "\n ".join(map(os.path.relpath, possible_definers)))
+ if reldir != ".":
+ reldir_msg = f" (relative to '{reldir}')"
+ else:
+ reldir_msg = ""
+ relative_path = relative_path_to(reldir)
+ if possible_declarators != []:
+ print(f"Possible declarations for function '{fname}' in the following file(s){reldir_msg}:")
+ print(" " + "\n ".join([os.path.relpath(path, start=reldir) for path in possible_declarators]))
+ if possible_definers != []:
+ print(f"Possible definitions for function '{fname}' in the following file(s){reldir_msg}:")
+ print(" " + "\n ".join([os.path.relpath(path, start=reldir) for path in possible_definers]))
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index 95046dbc58df060ba4ed390d1bf93ca9a6845a1d..fb4f76ada7731db4664f3846ab670f0173ca86ac 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -26,25 +26,33 @@
# GNUmakefile template): it parses the output and suggests useful commands
# whenever it can, by calling frama-c-script itself.
-import subprocess
-import sys
+import argparse
import os
import re
+import subprocess
+import sys
from functools import partial
-if len(sys.argv) < 3:
- print("usage: %s path-to-frama-c-script target" % sys.argv[0])
- print(" Builds the specified target, parsing the output to")
- print(" identify and recommend actions in case of failure.")
- print(" The first argument must be the path to the frama-c-script")
- print(" binary.")
- sys.exit(1)
+MIN_PYTHON = (3, 6) # for automatic Path conversions
+if sys.version_info < MIN_PYTHON:
+ sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
+
+parser = argparse.ArgumentParser(description="""
+Builds the specified target, parsing the output to identify and recommend
+actions in case of failure.""")
+parser.add_argument('--make-dir', metavar='DIR', default=".frama-c", nargs=1,
+ help='directory containing the makefile (default: .frama-c)')
+
+(make_dir_arg, args) = parser.parse_known_args()
+make_dir = vars(make_dir_arg)["make_dir"]
+args = args[1:]
-framac_script = sys.argv[1]
-target = sys.argv[2]
-args = sys.argv[3:]
+framac_bin = os.getenv('FRAMAC_BIN')
+if not framac_bin:
+ sys.exit("error: FRAMAC_BIN not in environment")
+framac_script = f"{framac_bin}/frama-c-script"
-out = subprocess.Popen(['make', target] + args,
+out = subprocess.Popen(['make', "-C", make_dir] + args,
stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
output = out.communicate()[0].decode('utf-8')
@@ -62,7 +70,7 @@ for line in lines:
if match:
fname = match.group(1)
def action(fname):
- out = subprocess.Popen([framac_script, "find-fun", fname],
+ out = subprocess.Popen([framac_script, "find-fun", "-C", make_dir, fname],
stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
output = out.communicate()[0].decode('utf-8')
re_possible_definers = re.compile("Possible definitions for function")
diff --git a/share/analysis-scripts/summary.py b/share/analysis-scripts/summary.py
index 6c0e9790e457e66562005c1ee7e75fc8ddb43b41..c3b309e80e0d7eaf771008144f5de9dcc4ff609a 100755
--- a/share/analysis-scripts/summary.py
+++ b/share/analysis-scripts/summary.py
@@ -45,7 +45,7 @@ def build_make_environment(framac):
else:
env = { **os.environ, 'PATH' : f"{framac}/bin:{os.environ['PATH']}" }
args = [
- f"FRAMAC_DIR={framac}/bin",
+ f"FRAMAC_BIN={framac}/bin",
f"FRAMAC={framac}/bin/frama-c"
]
return env, args