diff --git a/bin/frama-c-script b/bin/frama-c-script
index 0179f39113f1bc5b953a841c2fc23a41f0d5fc72..022f9b140965db5b7d07cff1ccfba1ff712386b2 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -31,12 +31,44 @@ usage() {
echo ""
echo " where cmd is:"
echo ""
+ echo " - configure machdep"
+ echo " Runs an existing configure script to only consider files"
+ echo " in Frama-C's libc; this will hopefully disable non-essential"
+ echo " and non-POSIX external libraries."
+ echo " (run 'frama-c -machdep help' to get the list of machdeps)."
+ echo ""
+ echo " - estimate-difficulty file..."
+ echo " Applies several heuristics to try and estimate the difficulty"
+ echo " of analyzing the specified files with Frama-C."
+ echo ""
+ echo " - find-fun function-name [dir...]"
+ echo " Lists files in dir... declaring or defining function-name"
+ echo " [default: PWD /usr/include]."
+ echo " Heuristics-based: neither correct nor complete."
+ echo ""
+ echo " - flamegraph flamegraph.txt [dir]"
+ echo " Generates flamegraph.svg and flamegraph.html in dir"
+ echo " [default: FRAMAC_SESSION]."
+ echo " Also opens it in a browser, unless variable NOGUI is set."
+ echo ""
echo " - help"
- echo " Display this help message and exit."
+ echo " Displays this help message and exits."
echo ""
- echo " - make-template [dir]"
- echo " Interactively prepares a template for analyses,"
- echo " writing it to dir/GNUmakefile [default: .frama-c]."
+ echo " - heuristic-detect-recursion file..."
+ echo " Uses a heuristic, syntactic-based, callgraph to detect recursive"
+ echo " calls. Results are guaranteed neither correct nor complete."
+ echo ""
+ echo " - heuristic-list-functions want_defs want_decls file..."
+ echo " Uses heuristics to find possible function definitions and declarations."
+ echo " If [want_defs] is true, lists definitions."
+ echo " If [want_decls] is true, lists declarations."
+ echo " Results are guaranteed neither correct nor complete."
+ echo ""
+ echo " - heuristic-print-callgraph [--dot outfile] file..."
+ echo " Prints a heuristic, syntactic-based, callgraph for the"
+ echo " specified files. Use --dot outfile to print it in DOT"
+ echo " (Graphviz) format, to [outfile]. If [outfile] is '-',"
+ echo " prints to stdout."
echo ""
echo " - list-files [path/to/compile_commands.json]"
echo " Lists all sources in the given compile_commands.json"
@@ -49,26 +81,9 @@ usage() {
echo " definitions, with source location and number of statements."
echo " Accepts Frama-C options (e.g. -cpp-extra-args for parsing)."
echo ""
- echo " - flamegraph flamegraph.txt [dir]"
- echo " Generates flamegraph.svg and flamegraph.html in dir"
- echo " [default: FRAMAC_SESSION]."
- echo " Also opens it in a browser, unless variable NOGUI is set."
- echo ""
- echo " - find-fun function-name [dir...]"
- echo " Lists files in dir... declaring or defining function-name"
- echo " [default: PWD /usr/include]."
- echo " Heuristics-based: neither correct nor complete."
- echo ""
- echo " - summary [options]"
- echo " Monitors and summarizes multiple analyses dispatched by a Makefile"
- echo " in the current PWD."
- echo " Use $0 summary --help for more informations."
- echo ""
- echo " - configure machdep"
- echo " Runs an existing configure script to only consider files"
- echo " in Frama-C's libc; this will hopefully disable non-essential"
- echo " and non-POSIX external libraries."
- echo " (run 'frama-c -machdep help' to get the list of machdeps)."
+ echo " - make-template [dir]"
+ echo " Interactively prepares a template for analyses,"
+ echo " writing it to dir/GNUmakefile [default: .frama-c]."
echo ""
echo " - make-wrapper target arg..."
echo " Runs 'make target arg...', parsing the output to suggest"
@@ -78,6 +93,11 @@ usage() {
echo " Applies some transformations to an existing compile_commands.json"
echo " (such as relativizing paths) to improve portability."
echo " [default: ./compile_commands.json]"
+ echo ""
+ echo " - summary [options]"
+ echo " Monitors and summarizes multiple analyses dispatched by a Makefile"
+ echo " in the current PWD."
+ echo " Use $0 summary --help for more informations."
exit "$1"
}
@@ -215,6 +235,22 @@ case "$command" in
shift;
configure_for_frama_c "$@";
;;
+ "heuristic-print-callgraph")
+ shift;
+ ${FRAMAC_SHARE}/analysis-scripts/print_callgraph.py "$@";
+ ;;
+ "heuristic-detect-recursion")
+ shift;
+ ${FRAMAC_SHARE}/analysis-scripts/detect_recursion.py "$@";
+ ;;
+ "heuristic-list-functions")
+ shift;
+ ${FRAMAC_SHARE}/analysis-scripts/heuristic_list_functions.py "$@";
+ ;;
+ "estimate-difficulty")
+ shift;
+ ${FRAMAC_SHARE}/analysis-scripts/estimate_difficulty.py "$@";
+ ;;
"make-wrapper")
shift;
"${FRAMAC_SHARE}"/analysis-scripts/make_wrapper.py "$0" "$@";
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 4c33aba539b7f8afe6bf137ad3e8d23e07830666..fefab89f71c3fecec85cc19c091c4b28258040b3 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -204,6 +204,7 @@ share/libc/__fc_define_wint_t.h: CEA_LGPL
share/libc/__fc_gcc_builtins.h: CEA_LGPL
share/libc/__fc_inet.h: CEA_LGPL
share/libc/__fc_integer.h: CEA_LGPL
+share/libc/__fc_libc.h: CEA_LGPL
share/libc/__fc_machdep.h: CEA_LGPL
share/libc/__fc_machdep_linux_shared.h: CEA_LGPL
share/libc/__fc_runtime.c: CEA_LGPL
diff --git a/share/analysis-scripts/build_callgraph.py b/share/analysis-scripts/build_callgraph.py
new file mode 100755
index 0000000000000000000000000000000000000000..b53e0d33bb133f15413b096c368f0cc8701d3df2
--- /dev/null
+++ b/share/analysis-scripts/build_callgraph.py
@@ -0,0 +1,181 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# This script finds files containing likely declarations and definitions
+# for a given function name, via heuristic syntactic matching.
+
+import sys
+import os
+import re
+import function_finder
+
+MIN_PYTHON = (3, 5)
+if sys.version_info < MIN_PYTHON:
+ sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
+
+arg = ""
+if len(sys.argv) < 2:
+ print(f"usage: {sys.argv[0]} file...")
+ print(" builds a heuristic callgraph for the specified files.")
+ sys.exit(1)
+else:
+ files = sys.argv[1:]
+
+debug = os.getenv("DEBUG")
+
+class Callgraph:
+ """
+ Heuristics-based callgraphs.
+ Nodes are function names. Edges (caller, callee, locations) contain the source
+ and target nodes, plus a list of locations (file, line) where calls from
+ [caller] to [callee] occur.
+ """
+
+ # maps each caller to the list of its callees
+ succs = {}
+
+ # maps (caller, callee) to the list of call locations
+ edges = {}
+
+ def add_edge(self, caller, callee, loc):
+ if (caller, callee) in self.edges:
+ # edge already exists
+ self.edges[(caller, callee)].append(loc)
+ else:
+ # new edge: check if caller exists
+ if not caller in self.succs:
+ self.succs[caller] = []
+ # add callee as successor of caller
+ self.succs[caller].append(callee)
+ # add call location to edge information
+ self.edges[(caller, callee)] = [loc]
+
+ def nodes(self):
+ return self.succs.keys()
+
+ def __repr__(self):
+ return f"Callgraph({self.succs}, {self.edges})"
+
+def compute(files):
+ #print(f"Computing callgraph for {len(files)} file(s)...")
+ cg = Callgraph()
+ for f in files:
+ #print(f"Processing {os.path.relpath(f)}...")
+ newlines = function_finder.compute_newline_offsets(f)
+ defs = function_finder.find_definitions_and_declarations(True, False, f, newlines)
+ calls = function_finder.find_calls(f, newlines)
+ for call in calls:
+ caller = function_finder.find_caller(defs, call)
+ if caller:
+ called, line, _ = call
+ loc = (f, line)
+ if debug:
+ print(f"build_callgraph: {f}:{line}: {caller} -> {called}")
+ cg.add_edge(caller, called, loc)
+ #print(f"Callgraph computed ({len(cg.succs)} node(s), {len(cg.edges)} edge(s))")
+ return cg
+
+def print_edge(cg, caller, called, padding="", end="\n"):
+ locs = cg.edges[(caller, called)]
+ for (filename, line) in locs:
+ print(f"{padding}{os.path.relpath(filename)}:{line}: {caller} -> {called}", end=end)
+
+def print_cg(cg):
+ for (caller, called) in cg.edges:
+ print_edge(cg, caller, called)
+
+# note: out _must_ exist (the caller must create it if needed)
+def print_cg_dot(cg, out=sys.stdout):
+ print("digraph callgraph {", file=out)
+ for (caller, called) in cg.edges:
+ print(f" {caller} -> {called};", file=out)
+ print("}", file=out)
+
+# succs: dict, input, not modified
+# visited: set, input-output, modified
+# just_visited: set, input-output, modified
+# n: input, not modified
+#
+# The difference between visited and just_visited is that the latter refers
+# to the current bfs; nodes visited in previous bfs already had their cycles
+# reported, so we do not report them multiple times.
+def cycle_bfs(cg, visited, just_visited, n):
+ if debug:
+ print(f"cycle_bfs: visited = {visited}, just_visited = {just_visited}, n = {n}")
+ just_visited.add(n)
+ if n not in cg.succs:
+ return []
+ fifo = []
+ for succ in cg.succs[n]:
+ if succ in just_visited:
+ return [(n, succ)]
+ elif succ in visited:
+ # already reported in a previous iteration
+ continue
+ fifo.append(succ)
+ # no cycle found with direct successors, go to next level
+ for succ in fifo:
+ my_just_visited = just_visited.copy()
+ res = cycle_bfs(cg, visited, my_just_visited, succ)
+ if res:
+ # note that other cycles may not be reported
+ caller = res[0][0]
+ return [(n, caller)] + res
+ return []
+
+def compute_recursive_cycles(cg, acc):
+ to_visit = set(cg.nodes())
+ if not to_visit: # empty graph -> no recursion
+ return
+ visited = set()
+ while to_visit:
+ just_visited = set()
+ n = sorted(list(to_visit))[0]
+ cycle = cycle_bfs(cg, visited, just_visited, n)
+ visited = visited.union(just_visited)
+ if cycle:
+ (fst, snd) = cycle[0]
+ cycle_start_loc = cg.edges[(fst, snd)][0]
+ acc.append((cycle_start_loc, cycle))
+ to_visit -= visited
+
+def detect_recursion(cg):
+ to_visit = set(cg.nodes())
+ if not to_visit: # empty graph -> no recursion
+ return False
+ visited = set()
+ has_cycle = False
+ while to_visit:
+ just_visited = set()
+ n = sorted(list(to_visit))[0]
+ cycle = cycle_bfs(cg, visited, just_visited, n)
+ visited = visited.union(just_visited)
+ if cycle:
+ has_cycle = True
+ print(f"recursive cycle detected: ")
+ for (caller, called) in cycle:
+ print_edge(cg, caller, called, padding=" ")
+ to_visit -= visited
+ if not has_cycle:
+ print(f"no recursive calls detected")
diff --git a/share/analysis-scripts/detect_recursion.py b/share/analysis-scripts/detect_recursion.py
new file mode 100755
index 0000000000000000000000000000000000000000..332d80f3b8ca50eb555c5100b68d96dc7c880e4f
--- /dev/null
+++ b/share/analysis-scripts/detect_recursion.py
@@ -0,0 +1,44 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# This script finds files containing likely declarations and definitions
+# for a given function name, via heuristic syntactic matching.
+
+import sys
+import build_callgraph
+
+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)
+
+arg = ""
+if len(sys.argv) < 2:
+ print(f"usage: {sys.argv[0]} [file1 file2 ...]")
+ print(" prints a heuristic callgraph for the specified files.")
+ sys.exit(1)
+else:
+ files = sys.argv[1:]
+
+cg = build_callgraph.compute(files)
+build_callgraph.detect_recursion(cg)
diff --git a/share/analysis-scripts/estimate_difficulty.py b/share/analysis-scripts/estimate_difficulty.py
new file mode 100755
index 0000000000000000000000000000000000000000..dab975aabac5e7bf03d0de6a7f20bb4adac0a367
--- /dev/null
+++ b/share/analysis-scripts/estimate_difficulty.py
@@ -0,0 +1,267 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# This script uses several heuristics to try and estimate the difficulty
+# of analyzing a new code base with Frama-C.
+
+import argparse
+import build_callgraph
+import function_finder
+import json
+import os
+from pathlib import Path
+import re
+import subprocess
+import sys
+import tempfile
+
+#TODO : avoid relativizing paths when introducing too many ".." ;
+#TODO : accept directory as argument (--full-tree), and then do glob **/*.{c,i} inside
+#TODO : try to check the presence of compiler builtins
+#TODO : try to check for pragmas
+
+MIN_PYTHON = (3, 5)
+if sys.version_info < MIN_PYTHON:
+ sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
+
+parser = argparse.ArgumentParser(description="""
+Estimates the difficulty of analyzing a given code base""")
+parser.add_argument("--header-dirs", "-d", metavar='DIR', nargs='+',
+ help='directories containing headers (default: .frama-c)')
+parser.add_argument("files", nargs='+', help='source files')
+args = vars(parser.parse_args())
+
+header_dirs = args["header_dirs"]
+if not header_dirs:
+ header_dirs = []
+files = args["files"]
+
+# gather information from several sources
+
+def extract_keys(l):
+ return [list(key.keys())[0] for key in l]
+
+def get_framac_libc_function_statuses(framac, framac_share):
+ (_metrics_handler, metrics_tmpfile) = tempfile.mkstemp(prefix="fc_script_est_diff", suffix=".json")
+ if debug:
+ print(f"metrics_tmpfile: {metrics_tmpfile}")
+ fc_runtime = framac_share / "libc" / "__fc_runtime.c"
+ fc_libc_headers = framac_share / "libc" / "__fc_libc.h"
+ subprocess.run([framac, "-no-autoload-plugins", fc_runtime, fc_libc_headers,
+ "-load-module", "metrics", "-metrics", "-metrics-libc",
+ "-metrics-output", metrics_tmpfile], stdout=subprocess.DEVNULL, check=True)
+ with open(metrics_tmpfile) as f:
+ metrics_json = json.load(f)
+ os.remove(metrics_tmpfile)
+ defined = extract_keys(metrics_json["defined-functions"])
+ spec_only = extract_keys(metrics_json["specified-only-functions"])
+ return (defined, spec_only)
+
+re_include = re.compile(r'\s*#\s*include\s*("|<)([^">]+)("|>)')
+def grep_includes_in_file(file):
+ with open(file, "r", encoding="utf-8", errors='ignore') as f:
+ i = 0
+ for line in f.readlines():
+ i += 1
+ m = re_include.match(line)
+ if m:
+ kind = m.group(1)
+ header = m.group(2)
+ yield((i,kind,header))
+
+def get_includes(files):
+ quote_includes = {}
+ chevron_includes = {}
+ for filename in files:
+ for line, kind, header in grep_includes_in_file(filename):
+ if kind == '<':
+ includes = chevron_includes[header] if header in chevron_includes else []
+ else:
+ includes = quote_includes[header] if header in quote_includes else []
+ includes.append((filename, line))
+ if kind == '<':
+ chevron_includes[header] = includes
+ else:
+ quote_includes[header] = includes
+ return chevron_includes, quote_includes
+
+debug = os.getenv("DEBUG")
+verbose = False
+
+print("Building callgraph...")
+cg = build_callgraph.compute(files)
+
+framac_bin = os.getenv('FRAMAC_BIN')
+if not framac_bin:
+ sys.exit("error: FRAMAC_BIN not in environment")
+framac = Path(framac_bin) / "frama-c"
+
+framac_share = Path(subprocess.check_output([framac, '-no-autoload-plugins', '-print-share-path']).decode())
+
+print("Computing data about libc/POSIX functions...")
+libc_defined_functions, libc_specified_functions = get_framac_libc_function_statuses(framac, framac_share)
+
+with open(framac_share / "compliance" / "c11_functions.json") as f:
+ c11_functions = json.load(f)["data"]
+
+with open(framac_share / "compliance" / "c11_headers.json") as f:
+ c11_headers = json.load(f)["data"]
+
+with open(framac_share / "compliance" / "posix_identifiers.json") as f:
+ all_data = json.load(f)
+ posix_identifiers = all_data["data"]
+ posix_headers = all_data["headers"]
+
+recursive_cycles = []
+reported_recursive_pairs = set()
+build_callgraph.compute_recursive_cycles(cg, recursive_cycles)
+for (cycle_start_loc, cycle) in recursive_cycles:
+ # Note: in larger code bases, many cycles are reported for the same final
+ # function (e.g. for the calls 'g -> g', we may have 'f -> g -> g',
+ # 'h -> g -> g', etc; to minimize this, we print just the first one.
+ # This does not prevent 3-cycle repetitions, such as 'f -> g -> f',
+ # but these are less common.
+ if cycle[-1] in reported_recursive_pairs:
+ continue
+ reported_recursive_pairs.add(cycle[-1])
+ (filename, line) = cycle_start_loc
+ (x, y) = cycle[0]
+ pretty_cycle = f"{x} -> {y}"
+ for (x, y) in cycle[1:]:
+ pretty_cycle += f" -> {y}"
+ print(f"[recursion] found recursive cycle near {filename}:{line}: {pretty_cycle}")
+
+callees = [callee for (_, callee) in list(cg.edges.keys())]
+callees = set(callees)
+used_headers = set()
+print(f"Estimating difficulty for {len(callees)} function calls...")
+warnings = 0
+
+for callee in sorted(callees):
+ def callee_status(status, standard, reason):
+ global warnings
+ if status == "warning":
+ warnings += 1
+ if verbose or debug or status == "warning":
+ print(f"- {status}: {callee} ({standard}) {reason}")
+ #print(f"callee: {callee}")
+ if callee in posix_identifiers:
+ used_headers.add(posix_identifiers[callee]["header"])
+ if callee in c11_functions:
+ standard = "C11"
+ # check that the callee is not a macro or type (e.g. va_arg);
+ # a few functions, such as strcpy_s, are in C11 but not in POSIX,
+ # so we must test membership before checking the POSIX type
+ if callee in posix_identifiers and posix_identifiers[callee]["id_type"] != "function":
+ continue
+ #print(f"C11 function: {callee}")
+ if callee in libc_specified_functions:
+ callee_status("good", standard, "is specified in Frama-C's libc")
+ elif callee in libc_defined_functions:
+ callee_status("ok", standard, "is defined in Frama-C's libc")
+ else:
+ # Some functions without specification are actually variadic
+ # (and possibly handled by the Variadic plug-in)
+ if callee in posix_identifiers and "notes" in posix_identifiers[callee] and "variadic-plugin" in posix_identifiers[callee]["notes"]:
+ callee_status("ok", standard, "is handled by the Variadic plug-in")
+ else:
+ callee_status("warning", standard, "has neither code nor spec in Frama-C's libc")
+ elif callee in posix_identifiers:
+ standard = "POSIX"
+ # check that the callee is not a macro or type (e.g. va_arg)
+ if posix_identifiers[callee]["id_type"] != "function":
+ continue
+ #print(f"Non-C11, POSIX function: {callee}")
+ if callee in libc_specified_functions:
+ callee_status("good", standard, "specified in Frama-C's libc")
+ elif callee in libc_defined_functions:
+ callee_status("ok", standard, "defined in Frama-C's libc")
+ else:
+ callee_status("warning", standard, "has neither code nor spec in Frama-C's libc")
+print(f"Function-related warnings: {warnings}")
+
+if (verbose or debug) and used_headers:
+ print(f"used headers:")
+ for header in sorted(used_headers):
+ print(f" <{header}>")
+
+(chevron_includes, quote_includes) = get_includes(files)
+
+def is_local_header(header_dirs, header):
+ for d in header_dirs:
+ path = Path(d)
+ if Path(path / header).exists():
+ return True
+ return False
+
+print(f"Estimating difficulty for {len(chevron_includes)} '#include <header>' directives...")
+non_posix_headers = []
+for header in sorted(chevron_includes, key=str.casefold):
+ if header in posix_headers:
+ fc_support = posix_headers[header]["fc-support"]
+ if fc_support == "unsupported":
+ print(f"- WARNING: included header <{header}> is explicitly unsupported by Frama-C")
+ elif fc_support == "none":
+ print(f"- warning: included header <{header}> not currently included in Frama-C's libc")
+ else:
+ if verbose or debug:
+ c11_or_posix = "C11" if header in c11_headers else "POSIX"
+ print(f"- note: included {c11_or_posix} header ")
+ else:
+ if is_local_header(header_dirs, header):
+ if verbose or debug:
+ print(f"- ok: included header <{header}> seems to be available locally")
+ else:
+ non_posix_headers.append(header)
+ print(f"- warning: included non-POSIX header <{header}>")
+print(f"Header-related warnings: {len(non_posix_headers)}")
+
+
+# dynamic allocation
+
+dynalloc_functions = set(["malloc", "calloc", "free", "realloc", "alloca", "mmap"])
+dyncallees = dynalloc_functions.intersection(callees)
+if dyncallees:
+ print(f"- note: calls to dynamic allocation functions: {', '.join(sorted(dyncallees))}")
+
+
+# unsupported C11-specific features
+
+c11_unsupported = ["_Alignas", "_Alignof", "_Generic", "_Static_assert"]
+
+for keyword in c11_unsupported:
+ out = subprocess.Popen(["grep", "-n", '\\b' + keyword + '\\b'] + files + ["/dev/null"],
+ stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ lines = out.communicate()[0].decode('utf-8').splitlines()
+ if lines:
+ n = len(lines)
+ print(f"- warning: found {n} line{'s' if n > 1 else ''} with occurrences of unsupported C11 construct '{keyword}'")
+
+# assembly code
+
+if "asm" in callees or "__asm" in callees or "__asm__" in callees:
+ print(f"- warning: code seems to contain inline assembly ('asm(...)')")
+
+# TODO:
+# - detect absence of 'main' function (library)
diff --git a/share/analysis-scripts/find_fun.py b/share/analysis-scripts/find_fun.py
index 18588b293bd0452317f4ae72f90e8b396775c3a1..e50d3d3f287e7caa95998cc614ee3a82e8e9ff5b 100755
--- a/share/analysis-scripts/find_fun.py
+++ b/share/analysis-scripts/find_fun.py
@@ -73,9 +73,9 @@ print("Looking for '%s' inside %d file(s)..." % (fname, len(files)))
possible_declarators = []
possible_definers = []
-re_fun = function_finder.prepare(fname)
+re_fun = function_finder.prepare_re_specific_name(fname)
for f in files:
- found = function_finder.find(re_fun, f)
+ found = function_finder.find_specific_name(re_fun, f)
if found:
if found == 1:
possible_declarators.append(f)
@@ -95,7 +95,7 @@ else:
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]))
+ print(" " + "\n ".join(sorted([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]))
+ print(" " + "\n ".join(sorted([os.path.relpath(path, start=reldir) for path in possible_definers])))
diff --git a/share/analysis-scripts/function_finder.py b/share/analysis-scripts/function_finder.py
old mode 100644
new mode 100755
index ee43f29adfb7ac6b75544622045a75cbceb5b003..e68f15ee479361b58be8bbea9284b2538b0130e5
--- a/share/analysis-scripts/function_finder.py
+++ b/share/analysis-scripts/function_finder.py
@@ -4,7 +4,7 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2020 #
+# Copyright (C) 2007-2021 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
@@ -24,6 +24,8 @@
# Exports find_function_in_file, to be used by other scripts
+import bisect
+import os
import re
# To minimize the amount of false positives, we try to match the following:
@@ -37,18 +39,27 @@ import re
# - identifiers are allowed after the parentheses, to allow for some macros/
# modifiers
+# auxiliary regexes
+c_identifier = "[a-zA-Z_][a-zA-Z0-9_]*"
+c_id_maybe_pointer = c_identifier + "\**"
+optional_c_id = "(?:" + c_identifier + ")?"
+non_empty_whitespace = "[ \t\r\n]+" # includes newline/CR
+whitespace = "[ \t\r\n]*" # includes newline/CR
+type_prefix = c_id_maybe_pointer + "(?:\s+\**" + c_id_maybe_pointer + ")*" + non_empty_whitespace + "\**"
+optional_type_prefix = "(?:" + type_prefix + whitespace + ")?"
+argument_list = "\([^)]*\)"
+
+debug = bool(os.getenv("DEBUG", False))
+
# Precomputes the regex for 'fname'
-def prepare(fname):
- c_identifier = "[a-zA-Z_][a-zA-Z0-9_]*"
- c_id_maybe_pointer = c_identifier + "\**"
- type_prefix = c_id_maybe_pointer + "(?:\s+\**" + c_id_maybe_pointer + ")*\s+\**"
- parentheses_suffix = "\s*\([^)]*\)"
- re_fun = re.compile("^(?:" + type_prefix + "\s*)?" + fname + parentheses_suffix
- + "\s*(?:" + c_identifier + ")?\s*(;|{)", flags=re.MULTILINE)
+def prepare_re_specific_name(fname):
+ re_fun = re.compile("^" + optional_type_prefix + fname + whitespace +
+ argument_list + whitespace +
+ optional_c_id + whitespace + "(;|{)", flags=re.DOTALL | re.MULTILINE)
return re_fun
# Returns 0 if not found, 1 if declaration, 2 if definition
-def find(prepared_re, f):
+def find_specific_name(prepared_re, f):
with open(f, encoding="ascii", errors='ignore') as content_file:
content = content_file.read()
has_decl_or_def = prepared_re.search(content)
@@ -57,3 +68,145 @@ def find(prepared_re, f):
else:
is_decl = has_decl_or_def.group(1) == ";"
return 1 if is_decl else 2
+
+
+# matches function definitions
+re_fundef_or_decl = re.compile("^" + optional_type_prefix +
+ "(" + c_identifier + ")" + whitespace +
+ argument_list + whitespace +
+ optional_c_id + whitespace + "(;|{)",
+ flags=re.DOTALL | re.MULTILINE)
+
+# matches function calls
+re_funcall = re.compile("(" + c_identifier + ")" + whitespace + "\(")
+
+# Computes the offset (in bytes) of each '\n' in the file,
+# returning them as a list
+def compute_newline_offsets(filename):
+ offsets = []
+ current = 0
+ with open(filename, encoding="ascii", errors='ignore') as data:
+ for line in data:
+ current += len(line)
+ offsets.append(current)
+ return offsets
+
+# Returns the line number (starting at 1) containing the character
+# of offset [offset].
+# [offsets] is the sorted list of offsets for newline characters in the file.
+def line_of_offset(offsets, offset):
+ i = bisect.bisect_right(offsets, offset)
+ return i+1
+
+# Returns the line number (starting at 1) of each line starting with '}'
+# as its first character.
+#
+# This is a heuristic to attempt to detect function closing braces:
+# it assumes that the first '}' (without preceding whitespace) after a
+# function definition denotes its closing brace.
+def compute_closing_braces(filename):
+ braces = []
+ with open(filename, encoding="ascii", errors='ignore') as data:
+ for i, line in enumerate(data, start=1):
+ if line.startswith("}"):
+ braces.append(i)
+ return braces
+
+# Returns the first element of [line_numbers] greater than [n], or [None]
+# if all numbers are smaller than [n] (this may happen e.g. when no
+# closing braces were found).
+#
+# [line_numbers] must be sorted in ascending order.
+def get_first_line_after(line_numbers, n):
+ for line in line_numbers:
+ if line > n:
+ return line
+ return None
+
+# Returns a list of tuples (fname, is_def, line_start, line_end, terminator_offset)
+# for each function definition or declaration.
+# If [want_defs] is True, definitions are included.
+# If [want_decls] is True, declarations are included.
+# [terminator_offset] is the byte offset of the `{` or `;`.
+# The list is sorted w.r.t. line numbers (in ascending order).
+#
+# [terminator_offset] is used by the caller to filter the function prototype
+# itself and avoid considering it as a call. For function definitions,
+# this is the opening brace; for function declarations, this is the semicolon.
+def find_definitions_and_declarations(want_defs, want_decls, filename, newlines):
+ braces = compute_closing_braces(filename)
+ with open(filename, encoding="ascii", errors='ignore') as data:
+ content = data.read()
+ res = []
+ for match in re.finditer(re_fundef_or_decl, content):
+ funcname = match.group(1)
+ is_def = match.group(2) == "{"
+ is_decl = match.group(2) == ";"
+ assert is_def or is_decl
+ start = line_of_offset(newlines, match.start(1))
+ if is_decl:
+ if not want_decls:
+ continue
+ end = line_of_offset(newlines, match.start(2))
+ else:
+ if not want_defs:
+ continue
+ definition = content[match.start(1):newlines[start-1]]
+ # try "single-line function heuristic":
+ # assume the function is defined as 'type f(...) { code; }',
+ # in a single line
+ if definition.strip().endswith("}"):
+ end = line_of_offset(newlines, match.start(2))
+ else:
+ end = get_first_line_after(braces, start)
+ if not end:
+ # no closing braces found; try again the "single-line function heuristic"
+ def_start_newline_offset = newlines[start-1]
+ line_of_opening_brace = line_of_offset(newlines, match.start(2))
+ if start == line_of_opening_brace and definition.rstrip().endswith("}"):
+ # assume the '}' is closing the '{' from the same line
+ end = line_of_opening_brace
+ else:
+ # no opening brace; assume a false positive and skip definition
+ print(f"{os.path.relpath(filename)}:{start}:closing brace not found, " +
+ f"skipping potential definition of '{funcname}'")
+ continue
+ terminator_offset = match.start(2)
+ if debug:
+ print(f"function_finder: {'def' if is_def else 'decl'} of {funcname} between {start} and {end}")
+ res.append((funcname, is_def, start, end, terminator_offset))
+ return res
+
+# list of identifiers which are never function calls
+calls_blacklist = ["if", "while", "for", "return", "sizeof", "switch", "_Alignas"]
+
+# Returns a list of tuples (fname, line, offset) for each function call.
+#
+# Note: this may include the function prototype itself;
+# it must be filtered by the caller.
+def find_calls(filename, newlines):
+ with open(filename, encoding="ascii", errors='ignore') as data:
+ content = data.read()
+ # create a list of Match objects that fit "pattern" regex
+ res = []
+ for match in re.finditer(re_funcall, content):
+ funcname = match.group(1)
+ offset = match.start(1)
+ line = line_of_offset(newlines, offset)
+ if funcname not in calls_blacklist:
+ res.append((funcname, line, offset))
+ return res
+
+# Returns the caller of [call], that is, the function whose definition
+# contains the line where [call] happens.
+# Returns [None] if there is no function at such line (i.e. a false positive).
+#
+# [defs] must be sorted in ascending order.
+def find_caller(defs, call):
+ (called, line, offset) = call
+ for (fname, _is_def, start, end, brace_offset) in defs:
+ if line >= start and line <= end and offset > brace_offset:
+ return fname
+ elif start > line:
+ return None
+ return None
diff --git a/share/analysis-scripts/heuristic_list_functions.py b/share/analysis-scripts/heuristic_list_functions.py
new file mode 100755
index 0000000000000000000000000000000000000000..ceee3fd5a3cf2892f1ed5c8fc8de5b8e76ce3c82
--- /dev/null
+++ b/share/analysis-scripts/heuristic_list_functions.py
@@ -0,0 +1,64 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# This script uses heuristics to list all function definitions and
+# declarations in a set of files.
+
+import sys
+import os
+import re
+import function_finder
+
+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 = bool(os.getenv("DEBUG", False))
+
+arg = ""
+if len(sys.argv) < 4:
+ print("usage: %s want_defs want_decls file..." % sys.argv[0])
+ print(" looks for likely function definitions and/or declarations")
+ print(" in the specified files.")
+ sys.exit(1)
+
+def boolish_string(s):
+ if s.lower() == "true" or s == "1":
+ return True
+ if s.lower() == "false" or s == "0":
+ return False
+ sys.exit(f"error: expected 'true', 'false', 0 or 1; got: {s}")
+
+want_defs = boolish_string(sys.argv[1])
+want_decls = boolish_string(sys.argv[2])
+files = sys.argv[3:]
+
+for f in files:
+ newlines = function_finder.compute_newline_offsets(f)
+ defs_and_decls = function_finder.find_definitions_and_declarations(want_defs, want_decls, f, newlines)
+ for (funcname, is_def, start, end, _offset) in defs_and_decls:
+ if is_def:
+ print(f"{os.path.relpath(f)}:{start}:{end}: {funcname} (definition)")
+ else:
+ print(f"{os.path.relpath(f)}:{start}:{end}: {funcname} (declaration)")
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index c986e4551c446b47caff148e869d65ef1713c58d..6e47b60c60993be74bbc2d40a32e9cd45150f880 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -98,11 +98,11 @@ main = input("Main target name: ")
if not re.match("^[a-zA-Z_0-9-]+$", main):
sys.exit("error: invalid main target name (can only contain letters, digits, dash or underscore)")
-main_fun_finder_re = function_finder.prepare("main")
+main_fun_finder_re = function_finder.prepare_re_specific_name("main")
# returns 0 if none, 1 if declaration, 2 if definition
def defines_or_declares_main(f):
- return function_finder.find(main_fun_finder_re, f)
+ return function_finder.find_specific_name(main_fun_finder_re, f)
def expand_and_normalize_sources(expression, relprefix):
subexps = shlex.split(expression)
diff --git a/share/analysis-scripts/print_callgraph.py b/share/analysis-scripts/print_callgraph.py
new file mode 100755
index 0000000000000000000000000000000000000000..9c5451669dc0955757608d50db117bb2249b7923
--- /dev/null
+++ b/share/analysis-scripts/print_callgraph.py
@@ -0,0 +1,60 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# This script finds files containing likely declarations and definitions
+# for a given function name, via heuristic syntactic matching.
+
+import sys
+import build_callgraph
+
+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)
+
+dotfile = None
+args = sys.argv[1:]
+if "--dot" in args:
+ dotarg = args.index("--dot")
+ dotfile = args[dotarg+1]
+ args_before = args[:dotarg-1] if dotarg > 0 else []
+ args_after = args[dotarg+2:]
+ args = args_before + args_after
+if not args:
+ print(f"usage: {sys.argv[0]} [--dot outfile] file1 file2 ...")
+ print(" prints a heuristic callgraph for the specified files.")
+ print(" If --dot is specified, print in DOT (Graphviz) format")
+ print(" to file outfile, or to stdout if outfile is '-'.")
+ sys.exit(1)
+
+cg = build_callgraph.compute(args)
+if dotfile:
+ if dotfile == "-":
+ out = sys.stdout
+ else:
+ out = open(dotfile, 'w')
+ build_callgraph.print_cg_dot(cg, out)
+ if dotfile != "-":
+ print(f"wrote {dotfile}")
+else:
+ build_callgraph.print_cg(cg)
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
new file mode 100644
index 0000000000000000000000000000000000000000..f9677ee2920415c3d8636d49de0dcd153fac5844
--- /dev/null
+++ b/share/libc/__fc_libc.h
@@ -0,0 +1,109 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+// This file includes all compatible libc/POSIX/BSD headers known by the
+// Frama-C standard library. It is used by some Frama-C scripts.
+
+#define _XOPEN_SOURCE 600
+#define _POSIX_C_SOURCE 200112L
+#define _GNU_SOURCE 1
+
+#include "alloca.h"
+#include "arpa/inet.h"
+#include "assert.h"
+#include "byteswap.h"
+#include "ctype.h"
+#include "dirent.h"
+#include "dlfcn.h"
+#include "endian.h"
+#include "errno.h"
+#include "fcntl.h"
+#include "features.h"
+#include "fenv.h"
+#include "float.h"
+#include "fnmatch.h"
+#include "ftw.h"
+#include "getopt.h"
+#include "glob.h"
+#include "grp.h"
+#include "iconv.h"
+#include "ifaddrs.h"
+#include "inttypes.h"
+#include "iso646.h"
+#include "libgen.h"
+#include "limits.h"
+#include "locale.h"
+#include "malloc.h"
+#include "math.h"
+#include "memory.h"
+#include "netdb.h"
+#include "net/if.h"
+#include "netinet/in.h"
+#include "netinet/ip.h"
+#include "netinet/tcp.h"
+#include "nl_types.h"
+#include "poll.h"
+#include "pthread.h"
+#include "pwd.h"
+#include "regex.h"
+#include "resolv.h"
+#include "sched.h"
+#include "semaphore.h"
+#include "setjmp.h"
+#include "signal.h"
+#include "stdarg.h"
+#include "stdbool.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+#include "stropts.h"
+#include "sys/file.h"
+#include "sys/ioctl.h"
+#include "sys/ipc.h"
+#include "syslog.h"
+#include "sys/mman.h"
+#include "sys/param.h"
+#include "sys/random.h"
+#include "sys/resource.h"
+#include "sys/select.h"
+#include "sys/shm.h"
+#include "sys/signal.h"
+#include "sys/socket.h"
+#include "sys/stat.h"
+#include "sys/time.h"
+#include "sys/times.h"
+#include "sys/timex.h"
+#include "sys/types.h"
+#include "sys/uio.h"
+#include "sys/un.h"
+#include "sys/utsname.h"
+#include "sys/wait.h"
+#include "termios.h"
+#include "time.h"
+#include "unistd.h"
+#include "utime.h"
+#include "utmpx.h"
+#include "wchar.h"
+#include "wctype.h"
diff --git a/tests/fc_script/build-callgraph.i b/tests/fc_script/build-callgraph.i
new file mode 100644
index 0000000000000000000000000000000000000000..b8105502931616ce2861af2459303855112b449a
--- /dev/null
+++ b/tests/fc_script/build-callgraph.i
@@ -0,0 +1,69 @@
+/* run.config
+ NOFRAMAC: testing frama-c-script, not frama-c itself
+ EXECNOW: LOG build-callgraph.res LOG build-callgraph.err bin/frama-c-script heuristic-print-callgraph @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_DIR@/result/build-callgraph.res 2> @PTEST_DIR@/result/build-callgraph.err
+ */
+
+#include <stdio.h>
+void main() {
+ strlen("");
+}
+struct s {
+ int a; int b;
+} s;
+
+volatile int v;
+
+int fn2(int, int);
+
+int fn1(int x, int y)
+{
+ Frama_C_show_each_1(x);
+ Frama_C_show_each_2(y);
+ return x + y;
+}
+
+int X, Y;
+int main1 () {
+ R1 = fn1(G, G|0);
+ R2 = fn2(G, G|0);
+ Frama_C_show_each_d(G);
+ pv = (int *) &X;
+ return Y;
+}
+
+int * main2() {
+ return 0;
+}
+
+#define not_a_function_call(v) \
+ yes_a_function_call(v)
+
+#define yet_another_not_a_call(v) do { \
+ yes_again(); \
+ } while (0)
+
+/* call_inside_comment(evaluation); */
+void main3 () {
+ //@ not_a_function_call(v);
+ yet_another_not_a_call(v);
+}
+
+/* Tests the initialization of local variables. */
+void main4 () {
+ f(g(h(i, j), k (l, m ( n(
+ o, p(
+ q)
+ )
+ )
+ )
+ )
+ );
+ f();
+ g();
+}
+void main() {
+ main1();
+ main2();
+ main3();
+ main4();
+}
diff --git a/tests/fc_script/list_functions.i b/tests/fc_script/list_functions.i
new file mode 100644
index 0000000000000000000000000000000000000000..aab65784552e38fdecd78fed6fd1ead8744f654d
--- /dev/null
+++ b/tests/fc_script/list_functions.i
@@ -0,0 +1,4 @@
+/* run.config
+ NOFRAMAC: testing frama-c-script, not frama-c itself
+ EXECNOW: LOG heuristic_list_functions.res LOG heuristic_list_functions.err bin/frama-c-script heuristic-list-functions true true @PTEST_DIR@/*.c @PTEST_DIR@/*.i > @PTEST_DIR@/result/heuristic_list_functions.res 2> @PTEST_DIR@/result/heuristic_list_functions.err
+ */
diff --git a/tests/fc_script/oracle/build-callgraph.err b/tests/fc_script/oracle/build-callgraph.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fc_script/oracle/build-callgraph.res b/tests/fc_script/oracle/build-callgraph.res
new file mode 100644
index 0000000000000000000000000000000000000000..145f1bccaf869fe75bcfed8dbd2834e13396ee33
--- /dev/null
+++ b/tests/fc_script/oracle/build-callgraph.res
@@ -0,0 +1,21 @@
+tests/fc_script/build-callgraph.i:8: main -> strlen
+tests/fc_script/build-callgraph.i:20: fn1 -> Frama_C_show_each_1
+tests/fc_script/build-callgraph.i:21: fn1 -> Frama_C_show_each_2
+tests/fc_script/build-callgraph.i:27: main1 -> fn1
+tests/fc_script/build-callgraph.i:28: main1 -> fn2
+tests/fc_script/build-callgraph.i:29: main1 -> Frama_C_show_each_d
+tests/fc_script/build-callgraph.i:47: main3 -> not_a_function_call
+tests/fc_script/build-callgraph.i:48: main3 -> yet_another_not_a_call
+tests/fc_script/build-callgraph.i:53: main4 -> f
+tests/fc_script/build-callgraph.i:61: main4 -> f
+tests/fc_script/build-callgraph.i:53: main4 -> g
+tests/fc_script/build-callgraph.i:62: main4 -> g
+tests/fc_script/build-callgraph.i:53: main4 -> h
+tests/fc_script/build-callgraph.i:53: main4 -> k
+tests/fc_script/build-callgraph.i:53: main4 -> m
+tests/fc_script/build-callgraph.i:53: main4 -> n
+tests/fc_script/build-callgraph.i:54: main4 -> p
+tests/fc_script/build-callgraph.i:65: main -> main1
+tests/fc_script/build-callgraph.i:66: main -> main2
+tests/fc_script/build-callgraph.i:67: main -> main3
+tests/fc_script/build-callgraph.i:68: main -> main4
diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res
index 0ceb3c8c68b411868c7fd156287a3c668e09466c..7d423014f36cda2c6e9e7f405bb272dd0f42d8e3 100644
--- a/tests/fc_script/oracle/find_fun1.res
+++ b/tests/fc_script/oracle/find_fun1.res
@@ -1,5 +1,6 @@
-Looking for 'main2' inside 11 file(s)...
+Looking for 'main2' inside 14 file(s)...
Possible declarations for function 'main2' in the following file(s):
tests/fc_script/for-find-fun.c
Possible definitions for function 'main2' in the following file(s):
+ tests/fc_script/build-callgraph.i
tests/fc_script/main2.c
diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res
index e59924a72f49f8278f2ff8fcec02062b9c68b2e3..ded016c9272e4dccb55c80cbb45e4fe3115c214b 100644
--- a/tests/fc_script/oracle/find_fun2.res
+++ b/tests/fc_script/oracle/find_fun2.res
@@ -1,5 +1,6 @@
-Looking for 'main3' inside 11 file(s)...
+Looking for 'main3' inside 14 file(s)...
Possible declarations for function 'main3' in the following file(s):
tests/fc_script/for-find-fun2.c
Possible definitions for function 'main3' in the following file(s):
+ tests/fc_script/build-callgraph.i
tests/fc_script/for-find-fun.c
diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res
index 6d151d463efe8d8df1a1ac874653880564ee4eb1..4a42d9117089960eb086c47a8e4b07b44795e3c3 100644
--- a/tests/fc_script/oracle/find_fun3.res
+++ b/tests/fc_script/oracle/find_fun3.res
@@ -1,2 +1,2 @@
-Looking for 'false_positive' inside 11 file(s)...
+Looking for 'false_positive' inside 14 file(s)...
No declaration/definition found for function 'false_positive'
diff --git a/tests/fc_script/oracle/heuristic_list_functions.err b/tests/fc_script/oracle/heuristic_list_functions.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fc_script/oracle/heuristic_list_functions.res b/tests/fc_script/oracle/heuristic_list_functions.res
new file mode 100644
index 0000000000000000000000000000000000000000..fe8495493cd286842024661ea2ed28407625a805
--- /dev/null
+++ b/tests/fc_script/oracle/heuristic_list_functions.res
@@ -0,0 +1,50 @@
+tests/fc_script/for-find-fun.c:6:7: main2 (declaration)
+tests/fc_script/for-find-fun.c:13:17: main3 (definition)
+tests/fc_script/for-find-fun2.c:5:7: main3 (declaration)
+tests/fc_script/for-find-fun2.c:10:12: f (definition)
+tests/fc_script/for-find-fun2.c:14:17: g (definition)
+tests/fc_script/for-find-fun2.c:19:21: h (definition)
+tests/fc_script/for-find-fun2.c:28:31: static_fun (definition)
+tests/fc_script/for-list-functions.c:8:15: static_fun (definition)
+tests/fc_script/for-list-functions.c:17:22: k (definition)
+tests/fc_script/main.c:12:14: main (definition)
+tests/fc_script/main2.c:6:8: fake_main (definition)
+tests/fc_script/main2.c:10:12: domain (definition)
+tests/fc_script/main2.c:14:16: main2 (definition)
+tests/fc_script/main3.c:6:9: main (definition)
+tests/fc_script/make-wrapper.c:7:7: defined (declaration)
+tests/fc_script/make-wrapper.c:9:9: specified (declaration)
+tests/fc_script/make-wrapper.c:11:11: external (declaration)
+tests/fc_script/make-wrapper.c:13:18: main (definition)
+tests/fc_script/make-wrapper2.c:5:7: defined (definition)
+tests/fc_script/make-wrapper2.c:13:13: specified (declaration)
+tests/fc_script/make-wrapper2.c:16:16: external (declaration)
+tests/fc_script/make-wrapper3.c:7:9: external (definition)
+tests/fc_script/build-callgraph.i:7:9: main (definition)
+tests/fc_script/build-callgraph.i:16:16: fn2 (declaration)
+tests/fc_script/build-callgraph.i:18:23: fn1 (definition)
+tests/fc_script/build-callgraph.i:26:32: main1 (definition)
+tests/fc_script/build-callgraph.i:34:36: main2 (definition)
+tests/fc_script/build-callgraph.i:46:49: main3 (definition)
+tests/fc_script/build-callgraph.i:52:63: main4 (definition)
+tests/fc_script/build-callgraph.i:64:69: main (definition)
+tests/fc_script/recursions.i:8:10: g (definition)
+tests/fc_script/recursions.i:12:15: f (definition)
+tests/fc_script/recursions.i:17:20: h (definition)
+tests/fc_script/recursions.i:22:24: i (definition)
+tests/fc_script/recursions.i:26:28: j (definition)
+tests/fc_script/recursions.i:30:30: l (declaration)
+tests/fc_script/recursions.i:31:31: m (declaration)
+tests/fc_script/recursions.i:33:35: k (definition)
+tests/fc_script/recursions.i:37:39: l (definition)
+tests/fc_script/recursions.i:41:43: m (definition)
+tests/fc_script/recursions.i:45:46: norec (definition)
+tests/fc_script/recursions.i:48:50: direct_rec (definition)
+tests/fc_script/recursions.i:52:52: indirect_rec1 (declaration)
+tests/fc_script/recursions.i:54:56: indirect_rec2 (definition)
+tests/fc_script/recursions.i:58:60: indirect_rec1 (definition)
+tests/fc_script/recursions.i:62:62: decl_only (declaration)
+tests/fc_script/recursions.i:64:64: one_liner_function (definition)
+tests/fc_script/recursions.i:66:66: multiple_indirect1 (declaration)
+tests/fc_script/recursions.i:68:71: multiple_indirect2 (definition)
+tests/fc_script/recursions.i:73:76: multiple_indirect1 (definition)
diff --git a/tests/fc_script/oracle/recursions.err b/tests/fc_script/oracle/recursions.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fc_script/oracle/recursions.res b/tests/fc_script/oracle/recursions.res
new file mode 100644
index 0000000000000000000000000000000000000000..af11f5fead4d3586b970c25f0d6301a1ad632348
--- /dev/null
+++ b/tests/fc_script/oracle/recursions.res
@@ -0,0 +1,18 @@
+recursive cycle detected:
+ tests/fc_script/recursions.i:49: direct_rec -> direct_rec
+recursive cycle detected:
+ tests/fc_script/recursions.i:13: f -> f
+recursive cycle detected:
+ tests/fc_script/recursions.i:18: h -> h
+recursive cycle detected:
+ tests/fc_script/recursions.i:59: indirect_rec1 -> indirect_rec2
+ tests/fc_script/recursions.i:55: indirect_rec2 -> indirect_rec1
+recursive cycle detected:
+ tests/fc_script/recursions.i:34: k -> l
+ tests/fc_script/recursions.i:38: l -> m
+ tests/fc_script/recursions.i:42: m -> k
+recursive cycle detected:
+ tests/fc_script/recursions.i:74: multiple_indirect1 -> multiple_indirect2
+ tests/fc_script/recursions.i:75: multiple_indirect1 -> multiple_indirect2
+ tests/fc_script/recursions.i:69: multiple_indirect2 -> multiple_indirect1
+ tests/fc_script/recursions.i:70: multiple_indirect2 -> multiple_indirect1
diff --git a/tests/fc_script/recursions.i b/tests/fc_script/recursions.i
new file mode 100644
index 0000000000000000000000000000000000000000..841d609939737908e7378823b9642e55af7fb2bb
--- /dev/null
+++ b/tests/fc_script/recursions.i
@@ -0,0 +1,76 @@
+/* run.config
+ NOFRAMAC: testing frama-c-script, not frama-c itself
+ EXECNOW: LOG recursions.res LOG recursions.err bin/frama-c-script heuristic-detect-recursion @PTEST_FILE@ > @PTEST_DIR@/result/recursions.res 2> @PTEST_DIR@/result/recursions.err
+*/
+
+volatile int v;
+
+void g() {
+ int g = 42;
+}
+
+void f() {
+ if (v) f();
+ else g();
+}
+
+void h() {
+ if (v) h();
+ else g();
+}
+
+void i() {
+ g();
+}
+
+void j() {
+ f();
+}
+
+void l(void);
+void m(void);
+
+void k() {
+ if (v) l();
+}
+
+void l() {
+ if (v) m();
+}
+
+void m() {
+ if (v) k();
+}
+
+void norec() {
+}
+
+int direct_rec() {
+ return direct_rec();
+}
+
+void indirect_rec1();
+
+void indirect_rec2() {
+ indirect_rec1();
+}
+
+void indirect_rec1() {
+ indirect_rec2();
+}
+
+void decl_only();
+
+void one_liner_function() { decl_only(); }
+
+void multiple_indirect1();
+
+void multiple_indirect2() {
+ multiple_indirect1();
+ multiple_indirect1();
+}
+
+void multiple_indirect1() {
+ multiple_indirect2();
+ multiple_indirect2();
+}
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 06372c7bffc52bdd4752aa4f83bb1b3fc3a3277e..3061c00a62693b3c162c1ee0902ec050b76d8b3a 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -38,6 +38,7 @@
[kernel] Parsing share/libc/__fc_gcc_builtins.h (with preprocessing)
[kernel] Parsing share/libc/__fc_inet.h (with preprocessing)
[kernel] Parsing share/libc/__fc_integer.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_libc.h (with preprocessing)
[kernel] Parsing share/libc/__fc_machdep.h (with preprocessing)
skipping share/libc/__fc_machdep_linux_shared.h
[kernel] Parsing share/libc/__fc_select.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index 73dac90425a73c971fb285476320f30bc36be7d1..ee4ef42c99932124f83b4c3b138d25035db3e95b 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -1 +1,2 @@
#include "__fc_integer.h"
+#include "__fc_libc.h"