diff --git a/Makefile b/Makefile
index 9af6317689253cc9dbda1c8f09bc45b47fbbd540..b05a3d65d5433327a68e21afe5e58faed796ed1f 100644
--- a/Makefile
+++ b/Makefile
@@ -257,6 +257,7 @@ DISTRIB_FILES:=\
$(LIBC_FILES) \
share/analysis-scripts/analysis.mk \
share/analysis-scripts/benchmark_database.py \
+ share/analysis-scripts/build.py \
share/analysis-scripts/build_callgraph.py \
share/analysis-scripts/cmd-dep.sh \
share/analysis-scripts/concat-csv.sh \
@@ -274,7 +275,6 @@ DISTRIB_FILES:=\
share/analysis-scripts/heuristic_list_functions.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/list_functions.ml \
- share/analysis-scripts/make_template.py \
share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/normalize_jcdb.py \
share/analysis-scripts/parse-coverage.sh \
@@ -284,6 +284,7 @@ DISTRIB_FILES:=\
share/analysis-scripts/results_display.py \
share/analysis-scripts/script_for_creduce_fatal.sh \
share/analysis-scripts/script_for_creduce_non_fatal.sh \
+ share/analysis-scripts/source_filter.py \
share/analysis-scripts/summary.py \
share/analysis-scripts/template.mk \
$(wildcard share/emacs/*.el) share/autocomplete_frama-c \
@@ -1973,6 +1974,8 @@ install:: install-lib-$(OCAMLBEST)
$(CP) \
share/analysis-scripts/analysis.mk \
share/analysis-scripts/benchmark_database.py \
+ share/analysis-scripts/build.py \
+ share/analysis-scripts/build_callgraph.py \
share/analysis-scripts/cmd-dep.sh \
share/analysis-scripts/concat-csv.sh \
share/analysis-scripts/clone.sh \
@@ -1986,7 +1989,6 @@ install:: install-lib-$(OCAMLBEST)
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/list_functions.ml \
- share/analysis-scripts/make_template.py \
share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/normalize_jcdb.py \
share/analysis-scripts/parse-coverage.sh \
@@ -1995,6 +1997,7 @@ install:: install-lib-$(OCAMLBEST)
share/analysis-scripts/results_display.py \
share/analysis-scripts/script_for_creduce_fatal.sh \
share/analysis-scripts/script_for_creduce_non_fatal.sh \
+ share/analysis-scripts/source_filter.py \
share/analysis-scripts/summary.py \
share/analysis-scripts/template.mk \
$(FRAMAC_DATADIR)/analysis-scripts
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 4a4c1d16e9c420bf663462df85fcfaa27dd044d7..014772a4d0b9acd3bd1918dcaa00670f64dea5b9 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -36,6 +36,10 @@ usage() {
echo ""
echo " where cmd is:"
echo ""
+ echo " - build [--jbdb build_commands.json] [--sources file...]"
+ echo " Produces a GNUmakefile for Frama-C analyses."
+ echo " Uses a build_commands.json if available."
+ 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"
@@ -91,10 +95,6 @@ usage() {
echo " definitions, with source location and number of statements."
echo " Accepts Frama-C options (e.g. -cpp-extra-args for parsing)."
echo ""
- 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"
echo " useful commands in case of failure."
@@ -217,9 +217,9 @@ case "$command" in
"help" | "-help" | "--help" | "-h")
usage 0;
;;
- "make-template")
+ "build")
shift;
- "${FRAMAC_SHARE}"/analysis-scripts/make_template.py "$@";
+ ${FRAMAC_SHARE}/analysis-scripts/build.py "$@";
;;
"list-files")
shift;
diff --git a/doc/userman/analysis-scripts.graphml b/doc/userman/analysis-scripts.graphml
index 2c798633e54136b20090b02b064c625b8167cfdc..1a5c42041381b8a2a670fda6d7817782016047f3 100644
--- a/doc/userman/analysis-scripts.graphml
+++ b/doc/userman/analysis-scripts.graphml
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:java="http://www.yworks.com/xml/yfiles-common/1.0/java" xmlns:sys="http://www.yworks.com/xml/yfiles-common/markup/primitives/2.0" xmlns:x="http://www.yworks.com/xml/yfiles-common/markup/2.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:y="http://www.yworks.com/xml/graphml" xmlns:yed="http://www.yworks.com/xml/yed/3" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://www.yworks.com/xml/schema/graphml/1.1/ygraphml.xsd">
- <!--Created by yEd 3.19-->
+ <!--Created by yEd 3.21.1-->
<key attr.name="Description" attr.type="string" for="graph" id="d0"/>
<key for="port" id="d1" yfiles.type="portgraphics"/>
<key for="port" id="d2" yfiles.type="portgeometry"/>
@@ -13,7 +13,7 @@
<key attr.name="description" attr.type="string" for="edge" id="d9"/>
<key for="edge" id="d10" yfiles.type="edgegraphics"/>
<graph edgedefault="directed" id="G">
- <data key="d0"/>
+ <data key="d0" xml:space="preserve"/>
<node id="n0">
<data key="d6">
<y:ShapeNode>
@@ -64,7 +64,6 @@ OS)<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelP
</node>
<node id="n4" yfiles.foldertype="group">
<data key="d4" xml:space="preserve"/>
- <data key="d5"/>
<data key="d6">
<y:ProxyAutoBoundsNode>
<y:Realizers active="0">
@@ -142,12 +141,11 @@ metrics.log<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><
</node>
<node id="n5" yfiles.foldertype="group">
<data key="d4" xml:space="preserve"/>
- <data key="d5"/>
<data key="d6">
<y:ProxyAutoBoundsNode>
<y:Realizers active="0">
<y:GroupNode>
- <y:Geometry height="254.93886947631842" width="159.0" x="909.7975425720215" y="426.6656832358396"/>
+ <y:Geometry height="254.9388694763183" width="159.0" x="909.7975425720215" y="426.6656832358397"/>
<y:Fill color="#F5F5F5" transparent="false"/>
<y:BorderStyle color="#000000" type="dashed" width="1.0"/>
<y:NodeLabel alignment="right" autoSizePolicy="node_width" backgroundColor="#EBEBEB" borderDistance="0.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="internal" modelPosition="t" textColor="#000000" verticalTextPosition="bottom" visible="true" width="159.0" x="0.0" xml:space="preserve" y="0.0"><target>.eva </y:NodeLabel>
@@ -176,7 +174,7 @@ metrics.log<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><
<y:Geometry height="123.69433229296885" width="149.0" x="914.7975425720215" y="465.51937416674775"/>
<y:Fill color="#99CCFF" transparent="false"/>
<y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
- <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="126.57923126220703" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="149.0" x="0.0" xml:space="preserve" y="-1.4424494846191465">alarms.csv
+ <y:NodeLabel alignment="left" autoSizePolicy="node_size" fontFamily="Noto Sans" fontSize="18" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="126.57923126220703" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="149.0" x="0.0" xml:space="preserve" y="-1.4424494846190328">alarms.csv
eva.log
warnings.log
metrics.log
@@ -273,7 +271,7 @@ Results<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:Mo
<node id="n11">
<data key="d6">
<y:ShapeNode>
- <y:Geometry height="93.0" width="284.0" x="178.625" y="601.8519359999999"/>
+ <y:Geometry height="93.0" width="284.0" x="178.625" y="595.6158232777708"/>
<y:Fill color="#C0C0C0" transparent="false"/>
<y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="85.71992492675781" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="264.419677734375" x="9.7901611328125" xml:space="preserve" y="3.6400375366210938">(Optional)
@@ -283,6 +281,19 @@ JSON Compilation Database
</y:ShapeNode>
</data>
</node>
+ <node id="n12">
+ <data key="d6">
+ <y:ShapeNode>
+ <y:Geometry height="93.0" width="284.0" x="209.625" y="700.8797105555417"/>
+ <y:Fill color="#C0C0C0" transparent="false"/>
+ <y:BorderStyle hasColor="false" raised="false" type="line" width="1.0"/>
+ <y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="85.71992492675781" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" verticalTextPosition="bottom" visible="true" width="221.27976989746094" x="31.36011505126953" xml:space="preserve" y="3.6400375366210938">(Optional)
+JSON Build Database
+(build_commands.json)<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
+ <y:Shape type="rectangle"/>
+ </y:ShapeNode>
+ </data>
+ </node>
<edge id="e0" source="n0" target="n1">
<data key="d10">
<y:PolyLineEdge>
@@ -373,7 +384,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e5" source="n5::n1" target="n6">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="74.5" sy="0.0" tx="-79.0" ty="0.0"/>
@@ -384,7 +394,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e6" source="n4::n2" target="n6">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="75.21875" sy="0.0" tx="-79.0" ty="0.0"/>
@@ -395,7 +404,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e7" source="n4::n0" target="n8">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="74.859375" sy="0.0" tx="-79.0" ty="0.0"/>
@@ -406,7 +414,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e8" source="n5::n0" target="n8">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="74.5" sy="0.0" tx="-79.0" ty="0.0"/>
@@ -417,7 +424,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e9" source="n4::n1" target="n7">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
@@ -428,7 +434,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e10" source="n4" target="n5">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
@@ -439,7 +444,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e11" source="n5" target="n9">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.7024574279785156" sy="-15.095404432332202" tx="-71.29754257202148" ty="-7.339997013875063"/>
@@ -450,7 +454,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e12" source="n1" target="n9">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="58.97499999999991" sy="2.6637775416665477" tx="0.0" ty="0.0">
@@ -465,7 +468,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e13" source="n4::n3" target="n10">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="75.21875" sy="0.0" tx="-88.5" ty="0.0"/>
@@ -476,7 +478,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e14" source="n5::n2" target="n10">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="74.5" sy="0.0" tx="-88.5" ty="0.0"/>
@@ -496,7 +497,6 @@ JSON Compilation Database
</data>
</edge>
<edge id="e15" source="n11" target="n1">
- <data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="43.375" sy="-37.35619205833348" tx="7.111959999999954" ty="1.600377541666603">
@@ -504,7 +504,22 @@ JSON Compilation Database
</y:Path>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
- <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="146.69981384277344" x="7.325258240567905" xml:space="preserve" y="-209.49274718831396">make-template<y:LabelModel><y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/></y:LabelModel><y:ModelParameter><y:SmartEdgeLabelModelParameter angle="0.0" distance="30.0" distanceToCenter="true" position="center" ratio="0.8467602870289302" segment="-1"/></y:ModelParameter><y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/></y:EdgeLabel>
+ <y:EdgeLabel alignment="center" backgroundColor="#FFFFFF" configuration="AutoFlippingLabel" distance="2.0" fontFamily="Noto Sans" fontSize="20" fontStyle="plain" hasLineColor="false" height="31.239974975585938" horizontalTextPosition="center" iconTextGap="4" modelName="custom" preferredPlacement="anywhere" ratio="0.5" textColor="#000000" verticalTextPosition="bottom" visible="true" width="51.279937744140625" x="95.43407712665595" xml:space="preserve" y="-203.2500103719077">build<y:LabelModel><y:SmartEdgeLabelModel autoRotationEnabled="false" defaultAngle="0.0" defaultDistance="10.0"/></y:LabelModel><y:ModelParameter><y:SmartEdgeLabelModelParameter angle="0.0" distance="30.0" distanceToCenter="true" position="center" ratio="0.8467602870289302" segment="-1"/></y:ModelParameter><y:PreferredPlacementDescriptor angle="0.0" angleOffsetOnRightSide="0" angleReference="absolute" angleRotationOnRightSide="co" distance="-1.0" frozen="true" placement="anywhere" side="anywhere" sideReference="relative_to_edge_flow"/></y:EdgeLabel>
+ <y:BendStyle smoothed="false"/>
+ </y:PolyLineEdge>
+ </data>
+ </edge>
+ <edge id="e16" source="n12" target="n0">
+ <data key="d10">
+ <y:PolyLineEdge>
+ <y:Path sx="124.53899999999999" sy="-14.479710555541715" tx="79.0" ty="0.0">
+ <y:Point x="476.164" y="556.9"/>
+ <y:Point x="364.0" y="556.9"/>
+ <y:Point x="364.0" y="407.9523135416665"/>
+ <y:Point x="364.0" y="314.8519359999999"/>
+ </y:Path>
+ <y:LineStyle color="#000000" type="line" width="1.0"/>
+ <y:Arrows source="none" target="none"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
diff --git a/doc/userman/analysis-scripts.pdf b/doc/userman/analysis-scripts.pdf
index 853e0e687779bd694aa87a1786e28038948769d2..1f8ade25fb74ecba20ff4dccf9bbe7ea9efdfd4e 100644
Binary files a/doc/userman/analysis-scripts.pdf and b/doc/userman/analysis-scripts.pdf differ
diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
index 459e17d0d4ef48f152bd9f82ff72ca7bc046e258..05a4b6b60d39eb91a24d6043e0bd7db42fde673a 100644
--- a/doc/userman/user-analysis-scripts.tex
+++ b/doc/userman/user-analysis-scripts.tex
@@ -77,9 +77,11 @@ and presents an illustrative diagram.
\subsection{Necessary Build Information}
\label{sec:necessary-build-information}
-The command \texttt{frama-c-script make-template} can be used to generate the
-Makefile from a template. The user must fill in the following information,
-required for running an \Value analysis:
+The command \texttt{frama-c-script build} can be used to generate the
+Makefile from a template. To run an analysis with \Value, the following
+information is necessary\footnote{If a \texttt{build\_commands.json} file is
+available, \texttt{frama-c-script build} will try to fill in some of the data
+automatically.}:
\begin{description}
\item[machdep]: architectural information about the system where the code will
@@ -164,9 +166,9 @@ in section~\ref{sec:preprocessing}). This leads to a different workflow:
In both cases, you will obtain a \texttt{compile\_commands.json} file.
\item Run \texttt{frama-c-script list-files}. A list of the compiled files,
along with files defining a \texttt{main} function, will be presented.
-\item Run \texttt{frama-c-script make-template} to create a template for
- \FramaC/\Value. Answer ``yes'' when asked about using the
- \texttt{compile\_commands.json} file.
+\item Run \texttt{frama-c-script build} to create a template for
+ \FramaC/\Value. It should detect the \texttt{compile\_commands.json} file
+ and add the option to enable it.
\end{enumerate}
Ideally, the above approach should result in a working template. In practice,
@@ -382,10 +384,11 @@ The most useful commands are described below.
Run \texttt{frama-c-script help} for more details and optional arguments.
\begin{description}
-\item[make-template]: creates the initial Makefile, based on a template.
+\item[build]: creates the initial Makefile, based on a template.
This command creates a file named \texttt{.frama-c/GNUmakefile} with some
- hardcoded sections, some sections filled in interactively by the user,
- and comments indicating which parts may need change.
+ hardcoded sections, some sections filled in according to command-line
+ options, and some sections filled automatically with build information
+ (via a \texttt{build\_commands.json} file), if available.
Once created, it enables the general workflow mentioned earlier.
\item[make-wrapper <target> <args>]: calls \texttt{make <target> <args>} with
a special wrapper: when running \Value, upon encountering one of a few known
@@ -421,8 +424,7 @@ Other commands, only useful in a few cases, are described below.
The following commands require a JSON Compilation Database.
\begin{description}
-\item[list-files]: lists all files in the given JCDB. Useful for filling
- out the Makefile template when running \texttt{make-template}.
+\item[list-files]: lists all files in the given JCDB.
\item[normalize-jcdb]: converts absolute paths inside a
\texttt{compile\_commands.json} file into relative paths (w.r.t. PWD)
when possible. Used to allow moving/versioning the directory containing
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 0d0c951d48b04dbdbd428528415e6281ccd9258c..0e623c2b82e255ecf0ec4a95f84a706cfe3503cb 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -116,6 +116,7 @@ ptests/ptests.ml: CEA_LGPL
share/_frama-c: CEA_LGPL
share/analysis-scripts/analysis.mk: CEA_LGPL
share/analysis-scripts/benchmark_database.py: CEA_LGPL
+share/analysis-scripts/build.py: CEA_LGPL
share/analysis-scripts/build_callgraph.py: CEA_LGPL
share/analysis-scripts/clone.sh: .ignore
share/analysis-scripts/creduce.sh: CEA_LGPL
@@ -133,7 +134,6 @@ share/analysis-scripts/git_utils.py: CEA_LGPL
share/analysis-scripts/heuristic_list_functions.py: CEA_LGPL
share/analysis-scripts/list_files.py: CEA_LGPL
share/analysis-scripts/list_functions.ml: CEA_LGPL
-share/analysis-scripts/make_template.py: CEA_LGPL
share/analysis-scripts/make_wrapper.py: CEA_LGPL
share/analysis-scripts/normalize_jcdb.py: CEA_LGPL
share/analysis-scripts/parse-coverage.sh: .ignore
@@ -143,6 +143,7 @@ share/analysis-scripts/README.md: .ignore
share/analysis-scripts/results_display.py: CEA_LGPL
share/analysis-scripts/script_for_creduce_fatal.sh: .ignore
share/analysis-scripts/script_for_creduce_non_fatal.sh: .ignore
+share/analysis-scripts/source_filter.py: CEA_LGPL
share/analysis-scripts/summary.py: CEA_LGPL
share/analysis-scripts/template.mk: .ignore
share/compliance/c11_functions.json: .ignore
diff --git a/share/analysis-scripts/build.py b/share/analysis-scripts/build.py
new file mode 100755
index 0000000000000000000000000000000000000000..768082a01d42c21ea3621d7dc92bebf382ecf79b
--- /dev/null
+++ b/share/analysis-scripts/build.py
@@ -0,0 +1,352 @@
+#!/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 blug and a build_commands.json file to produce an
+# analysis GNUmakefile, as automatically as possible.
+
+import argparse
+import json
+import logging
+import os
+from pathlib import Path
+import re
+import shutil
+import sys
+import subprocess
+
+import function_finder
+import source_filter
+
+script_dir = os.path.dirname(sys.argv[0])
+
+# Command-line parsing ########################################################
+
+parser = argparse.ArgumentParser(description="""Produces a GNUmakefile
+for analysis with Frama-C. Tries to use a build_commands.json file if
+available.""")
+parser.add_argument('--debug', metavar='FILE',
+ help='enable debug mode and redirect output to the specified file')
+parser.add_argument('--force', action="store_true",
+ help='overwrite files without prompting')
+parser.add_argument('--jbdb', metavar='FILE', default="build_commands.json",
+ help='path to JBDB (default: build_commands.json)')
+parser.add_argument('--machdep', metavar='MACHDEP',
+ help="analysis machdep (default: Frama-C's default)")
+parser.add_argument('--main', metavar='FUNCTION', default="main",
+ help='name of the main function (default: main)')
+parser.add_argument('--sources', metavar='FILE', nargs='+',
+ help='list of sources to parse (overrides --jbdb)',
+ type=Path)
+parser.add_argument('--targets', metavar='FILE', nargs='+',
+ help='targets to build. When using --sources, ' +
+ 'only a single target is allowed.',
+ type=Path)
+
+args = parser.parse_args()
+force = args.force
+jbdb_path = args.jbdb
+machdep = args.machdep
+main = args.main
+sources = args.sources
+targets = args.targets
+debug = args.debug
+
+debug_level = logging.DEBUG if debug else logging.INFO
+# special values for debug filename
+if debug == "stdout":
+ logging.basicConfig(stream=sys.stdout, level=debug_level,
+ format='[%(levelname)s] %(message)s')
+elif debug == "stderr":
+ logging.basicConfig(stream=sys.stderr, level=debug_level,
+ format='[%(levelname)s] %(message)s')
+elif debug:
+ logging.basicConfig(filename=debug, level=debug_level, filemode='w',
+ format='[%(levelname)s] %(message)s')
+else:
+ logging.basicConfig(level=logging.INFO,
+ format='[%(levelname)s] %(message)s')
+
+dot_framac_dir = Path(".frama-c")
+
+# Check required environment variables and commands in the PATH ###############
+
+framac_bin = os.getenv('FRAMAC_BIN')
+if not framac_bin:
+ sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
+framac_bin = Path(framac_bin)
+
+under_test = os.getenv("PTESTS_TESTING")
+
+# Prepare blug-related variables and functions ################################
+
+blug = os.getenv('BLUG')
+if not blug:
+ blug = shutil.which("blug")
+ if not blug:
+ sys.exit("error: path to 'blug' binary must be in PATH or variable BLUG")
+blug = Path(blug)
+blug_dir = blug.resolve().parent
+blug_print = blug_dir / "blug-print"
+# to import blug_jbdb
+sys.path.insert(0, blug_dir.as_posix())
+import blug_jbdb
+from blug_jbdb import prettify
+
+
+# Auxiliary functions #########################################################
+
+def call_and_get_output(command_and_args):
+ try:
+ return subprocess.check_output(command_and_args, stderr=subprocess.STDOUT).decode()
+ except subprocess.CalledProcessError as e:
+ sys.exit(f"error running command: {command_and_args}\n{e}")
+
+def ask_if_overwrite(path):
+ yn = input(f"warning: {path} already exists. Overwrite? [y/N] ")
+ if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
+ sys.exit("Exiting without overwriting.")
+
+def insert_lines_after(lines, line_pattern, new_lines):
+ re_line = re.compile(line_pattern)
+ for i, line in enumerate(lines):
+ if re_line.search(line):
+ for j, new_line in enumerate(new_lines):
+ lines.insert(i+1+j, new_line)
+ return
+ sys.exit(f"error: no lines found matching pattern: {line_pattern}")
+
+# delete the first occurrence of [line_pattern]
+def delete_line(lines, line_pattern):
+ re_line = re.compile(line_pattern)
+ for i, line in enumerate(lines):
+ if re_line.search(line):
+ del lines[i]
+ return
+ sys.exit(f"error: no lines found matching pattern: {line_pattern}")
+
+def replace_line(lines, line_pattern, value, all_occurrences=False):
+ replaced = False
+ re_line = re.compile(line_pattern)
+ for i, line in enumerate(lines):
+ if re_line.search(line):
+ lines[i] = value
+ replaced = True
+ if not all_occurrences:
+ return
+ if replaced:
+ return
+ sys.exit(f"error: no lines found matching pattern: {line_pattern}")
+
+# replaces '/' and '.' with '_' so that a valid target name is created
+def make_target_name(target):
+ return prettify(target).replace('/', '_').replace('.', '_')
+
+# sources are pretty-printed relatively to the .frama-c directory, where the
+# GNUmakefile will reside
+def rel_prefix(path):
+ return path if os.path.isabs(path) else os.path.relpath(path, start=dot_framac_dir)
+
+def pretty_sources(sources):
+ return [f" {rel_prefix(source)} \\" for source in sources]
+
+def lines_of_file(path):
+ return path.read_text().splitlines()
+
+fc_stubs_copied = False
+def copy_fc_stubs():
+ global fc_stubs_copied
+ dest = dot_framac_dir / "fc_stubs.c"
+ if not fc_stubs_copied:
+ fc_stubs = lines_of_file(share_dir / "analysis-scripts" / "fc_stubs.c")
+ re_main = re.compile(r"\bmain\b")
+ for i, line in enumerate(fc_stubs):
+ if line.startswith("//"):
+ continue
+ fc_stubs[i] = re.sub(re_main, main, line)
+ if not force and dest.exists():
+ ask_if_overwrite(dest)
+ with open(dest,"w") as f:
+ f.write("\n".join(fc_stubs))
+ logging.info("wrote: %s", dest)
+ fc_stubs_copied = True
+ return dest
+
+# Returns pairs (line_number, has_args) for each likely definition of
+# [funcname] in [filename].
+# [has_args] is used to distinguish between main(void) and main(int, char**).
+def find_definitions(funcname, filename):
+ file_content = source_filter.open_and_filter(filename, not under_test)
+ file_lines = file_content.splitlines(keepends=True)
+ newlines = function_finder.compute_newline_offsets(file_lines)
+ defs = function_finder.find_definitions_and_declarations(True, False, filename, file_content, file_lines, newlines, funcname)
+ res = []
+ for d in defs:
+ defining_line = file_lines[d[2]-1]
+ after_funcname = defining_line[defining_line.find(funcname)+len(funcname):]
+ # heuristics: if there is a comma after the function name,
+ # it is very likely the signature contains arguments;
+ # otherwise, the function is either defined in several lines,
+ # or we somehow missed it. By default, we assume it has no arguments
+ # if we miss it.
+ has_args = ',' in after_funcname
+ res.append((d[2], has_args))
+ return res
+
+# End of auxiliary functions ##################################################
+
+sources_map = dict()
+if sources:
+ if not targets:
+ sys.exit("error: option --targets is mandatory when --sources is specified")
+ if len(targets) > 1:
+ sys.exit("error: option --targets can only have a single target when --sources is specified")
+ sources_map[targets[0]] = [s for s in sources if blug_jbdb.filter_source(s)]
+elif os.path.isfile(jbdb_path):
+ # JBDB exists
+ with open(jbdb_path, "r") as data:
+ jbdb = json.load(data)
+ blug_jbdb.absolutize_jbdb(jbdb)
+ jbdb_targets = []
+ for f in jbdb:
+ jbdb_targets += [t for t in f["targets"] if blug_jbdb.filter_target(t)]
+ if not jbdb_targets:
+ sys.exit(f"no targets found in JBDB ({jbdb_path})")
+ if not targets:
+ # no targets specified in command line; use all from JBDB
+ targets = jbdb_targets
+ logging.info("Computing sources for each target (%d target(s))...", len(targets))
+ unknown_targets = []
+ graph = blug_jbdb.build_graph(jbdb)
+ for target in targets:
+ if target not in jbdb_targets:
+ unknown_targets.append(target)
+ else:
+ if unknown_targets != []:
+ continue # already found a problem; avoid useless computations
+ sources = [s for s in blug_jbdb.collect_leaves(graph, [target]) if blug_jbdb.filter_source(s)]
+ sources_map[target] = sorted(sources)
+ if unknown_targets:
+ targets_pretty = "\n".join(unknown_targets)
+ sys.exit("target(s) not found in JBDB:\n{targets_pretty}")
+else:
+ if not jbdb_path:
+ sys.exit("error: either a JBDB or option --sources are required")
+ else:
+ sys.exit(f"error: invalid JBDB path: '{jbdb_path}'")
+
+logging.debug("sources_map: %s", sorted([prettify(k) + ": " + ', '.join(sorted([prettify(s) for s in v])) for (k, v) in sources_map.items()]))
+logging.debug("targets: %s", sorted([prettify(t) for t in targets]))
+
+# check that source files exist
+unknown_sources = sorted({s for sources in sources_map.values() for s in sources if not s.exists()})
+if unknown_sources:
+ sys.exit("error: source(s) not found:\n" + "\n".join([prettify(s) for s in unknown_sources]))
+
+# Check that the main function is defined exactly once per target.
+# note: this is only based on heuristics (and fails on a few real case studies),
+# so we cannot emit errors, only warnings.
+# We also need to check if the main function uses a 'main(void)'-style
+# signature, to patch fc_stubs.c.
+
+main_definitions = {}
+for target, sources in sources_map.items():
+ main_definitions[target] = []
+ for source in sources:
+ fundefs = find_definitions(main, source)
+ main_definitions[target] += [(source, fundef[0], fundef[1]) for fundef in fundefs]
+ if main_definitions[target] == []:
+ logging.warning("function '%s' seems to be never defined in the sources of target '%s'", main, prettify(target))
+ elif len(main_definitions[target]) > 1:
+ logging.warning("function '%s' seems to be defined multiple times in the sources of target '%s':", main, prettify(target))
+ for (filename, line, _) in main_definitions[target]:
+ print(f"- definition at {filename}:{line}")
+
+# End of checks; start writing GNUmakefile and stubs from templates ###########
+
+if not dot_framac_dir.is_dir():
+ logging.debug("creating %s", dot_framac_dir)
+ dot_framac_dir.mkdir(parents=True, exist_ok=False)
+
+fc_config = json.loads(call_and_get_output([framac_bin / "frama-c", "-print-config-json"]))
+share_dir = Path(fc_config['datadir'])
+
+# copy fc_stubs if at least one main function has arguments
+any_has_arguments = False
+for defs in main_definitions.values():
+ if any(d[2] for d in defs):
+ any_has_arguments = True
+ break
+
+if any_has_arguments:
+ fc_stubs = copy_fc_stubs()
+ for target in targets:
+ if any(d[2] for d in main_definitions[target]):
+ logging.debug("target %s has main with args, adding fc_stubs.c to its sources", prettify(target))
+ sources_map[target].insert(0, fc_stubs)
+
+gnumakefile = dot_framac_dir / "GNUmakefile"
+
+template = lines_of_file(share_dir / "analysis-scripts" / "template.mk")
+
+if machdep:
+ machdeps = fc_config['machdeps']
+ if machdep not in machdeps:
+ logging.warning("unknown machdep (%s) not in Frama-C's default machdeps:\n%s", machdep, " ".join(machdeps))
+ replace_line(template, "^MACHDEP = .*", f"MACHDEP = {machdep}")
+
+if jbdb_path:
+ insert_lines_after(template, "^FCFLAGS", [f" -json-compilation-database {rel_prefix(jbdb_path)} \\"])
+
+targets_eva = ([f" {make_target_name(target)}.eva \\" for target in targets])
+replace_line(template, "^TARGETS = main.eva", "TARGETS = \\")
+insert_lines_after(template, r"^TARGETS = \\", targets_eva)
+
+delete_line(template, r"^main.parse: \\")
+delete_line(template, r"^ main.c \\")
+for target, sources in reversed(sources_map.items()):
+ pp_target = make_target_name(target)
+ new_lines = [f"{pp_target}.parse: \\"] + pretty_sources(sources) + [""]
+ if any(d[2] for d in main_definitions[target]):
+ logging.debug("target %s has main with args, adding -main eva_main to its FCFLAGS", prettify(target))
+ new_lines += [f"{pp_target}.parse: FCFLAGS += -main eva_main", ""]
+ insert_lines_after(template, "^### Each target <t>.eva", new_lines)
+
+gnumakefile.write_text("\n".join(template))
+
+logging.info("wrote: %s", gnumakefile)
+
+# write path.mk, but only if it does not exist.
+path_mk = dot_framac_dir / "path.mk"
+if not force and path_mk.exists():
+ logging.info("%s already exists, will not overwrite it", path_mk)
+else:
+ path_mk.write_text(f"""FRAMAC_BIN={framac_bin}
+ifeq ($(wildcard $(FRAMAC_BIN)),)
+# Frama-C not installed locally; using the version in the PATH
+else
+FRAMAC=$(FRAMAC_BIN)/frama-c
+FRAMAC_GUI=$(FRAMAC_BIN)/frama-c-gui
+endif
+""")
+ logging.info("wrote: %s", path_mk)
diff --git a/share/analysis-scripts/build_callgraph.py b/share/analysis-scripts/build_callgraph.py
index b53e0d33bb133f15413b096c368f0cc8701d3df2..a1047a70e0eaa9d92044396ed947d5178c2a0822 100755
--- a/share/analysis-scripts/build_callgraph.py
+++ b/share/analysis-scripts/build_callgraph.py
@@ -25,14 +25,14 @@
# 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 sys
+
import function_finder
+import source_filter
-MIN_PYTHON = (3, 5)
-if sys.version_info < MIN_PYTHON:
- sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
+under_test = os.getenv("PTESTS_TESTING")
arg = ""
if len(sys.argv) < 2:
@@ -78,13 +78,13 @@ class Callgraph:
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)
+ file_content = source_filter.open_and_filter(f, not under_test)
+ file_lines = file_content.splitlines(keepends=True)
+ newlines = function_finder.compute_newline_offsets(file_lines)
+ defs = function_finder.find_definitions_and_declarations(True, False, f, file_content, file_lines, newlines)
+ calls = function_finder.find_calls(file_content, newlines)
for call in calls:
caller = function_finder.find_caller(defs, call)
if caller:
@@ -93,7 +93,6 @@ def compute(files):
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"):
diff --git a/share/analysis-scripts/detect_recursion.py b/share/analysis-scripts/detect_recursion.py
index 332d80f3b8ca50eb555c5100b68d96dc7c880e4f..c5da73ad2f3712259a6b8cde93193997ee9a45f9 100755
--- a/share/analysis-scripts/detect_recursion.py
+++ b/share/analysis-scripts/detect_recursion.py
@@ -28,10 +28,6 @@
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 ...]")
diff --git a/share/analysis-scripts/estimate_difficulty.py b/share/analysis-scripts/estimate_difficulty.py
index dab975aabac5e7bf03d0de6a7f20bb4adac0a367..13ad4fec48a3468d47280922239ade96811b04b9 100755
--- a/share/analysis-scripts/estimate_difficulty.py
+++ b/share/analysis-scripts/estimate_difficulty.py
@@ -26,25 +26,23 @@
# 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
+from pathlib import Path
import re
import subprocess
import sys
import tempfile
+import build_callgraph
+import function_finder
+import source_filter
+
#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='+',
@@ -57,6 +55,8 @@ if not header_dirs:
header_dirs = []
files = args["files"]
+under_test = os.getenv("PTESTS_TESTING")
+
# gather information from several sources
def extract_keys(l):
@@ -79,16 +79,16 @@ def get_framac_libc_function_statuses(framac, framac_share):
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 grep_includes_in_file(filename):
+ file_content = source_filter.open_and_filter(filename, not under_test)
+ i = 0
+ for line in file_content.splitlines():
+ 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 = {}
@@ -165,9 +165,10 @@ for callee in sorted(callees):
warnings += 1
if verbose or debug or status == "warning":
print(f"- {status}: {callee} ({standard}) {reason}")
- #print(f"callee: {callee}")
+ is_problematic = callee in posix_identifiers and "notes" in posix_identifiers[callee] and "fc-support" in posix_identifiers[callee]["notes"] and posix_identifiers[callee]["notes"]["fc-support"] == "problematic"
if callee in posix_identifiers:
used_headers.add(posix_identifiers[callee]["header"])
+ status_emitted = False # to avoid re-emitting a message for functions in both C11 and POSIX
if callee in c11_functions:
standard = "C11"
# check that the callee is not a macro or type (e.g. va_arg);
@@ -175,30 +176,40 @@ for callee in sorted(callees):
# 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:
+ if (not is_problematic) and callee in libc_specified_functions:
callee_status("good", standard, "is specified in Frama-C's libc")
- elif callee in libc_defined_functions:
+ status_emitted = True
+ elif (not is_problematic) and callee in libc_defined_functions:
callee_status("ok", standard, "is defined in Frama-C's libc")
+ status_emitted = True
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:
+ if callee not in posix_identifiers:
callee_status("warning", standard, "has neither code nor spec in Frama-C's libc")
- elif callee in posix_identifiers:
+ status_emitted = True
+ if not status_emitted and 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:
+ if (not is_problematic) and callee in libc_specified_functions:
callee_status("good", standard, "specified in Frama-C's libc")
- elif callee in libc_defined_functions:
+ status_emitted = True
+ elif (not is_problematic) and callee in libc_defined_functions:
callee_status("ok", standard, "defined in Frama-C's libc")
+ status_emitted = True
else:
- callee_status("warning", standard, "has neither code nor spec in Frama-C's libc")
+ # Some functions without specification are actually variadic
+ # (and possibly handled by the Variadic plug-in)
+ if "notes" in posix_identifiers[callee]:
+ if "variadic-plugin" in posix_identifiers[callee]["notes"]:
+ callee_status("ok", standard, "is handled by the Variadic plug-in")
+ status_emitted = True
+ elif is_problematic:
+ callee_status("warning", standard, "is known to be problematic for code analysis")
+ status_emitted = True
+ if not status_emitted:
+ 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:
@@ -217,12 +228,15 @@ def is_local_header(header_dirs, header):
print(f"Estimating difficulty for {len(chevron_includes)} '#include <header>' directives...")
non_posix_headers = []
+header_warnings = 0
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":
+ header_warnings += 1
print(f"- WARNING: included header <{header}> is explicitly unsupported by Frama-C")
elif fc_support == "none":
+ header_warnings += 1
print(f"- warning: included header <{header}> not currently included in Frama-C's libc")
else:
if verbose or debug:
@@ -234,8 +248,9 @@ for header in sorted(chevron_includes, key=str.casefold):
print(f"- ok: included header <{header}> seems to be available locally")
else:
non_posix_headers.append(header)
+ header_warnings += 1
print(f"- warning: included non-POSIX header <{header}>")
-print(f"Header-related warnings: {len(non_posix_headers)}")
+print(f"Header-related warnings: {header_warnings}")
# dynamic allocation
@@ -248,7 +263,9 @@ if dyncallees:
# unsupported C11-specific features
-c11_unsupported = ["_Alignas", "_Alignof", "_Generic", "_Static_assert"]
+c11_unsupported = ["_Alignas", "_Alignof", "_Complex", "_Generic", "_Imaginary",
+ "alignas", "alignof" # stdalign.h may use these symbols instead of the C11 keywords
+ ];
for keyword in c11_unsupported:
out = subprocess.Popen(["grep", "-n", '\\b' + keyword + '\\b'] + files + ["/dev/null"],
diff --git a/share/analysis-scripts/find_fun.py b/share/analysis-scripts/find_fun.py
index b14e429fba77ebf14b0e952f5826b0ffa71a6a10..c05fbb68af1854602b05ca2587450f0c1cb501cd 100755
--- a/share/analysis-scripts/find_fun.py
+++ b/share/analysis-scripts/find_fun.py
@@ -32,10 +32,6 @@ import re
import sys
from pathlib import Path
-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)
-
parser = argparse.ArgumentParser(description="""
Looks for likely declarations/definitions of a function
in files with extensions '.c', '.h' and '.i'.
@@ -78,12 +74,15 @@ possible_declarators = []
possible_definers = []
re_fun = function_finder.prepare_re_specific_name(fname)
for f in files:
- found = function_finder.find_specific_name(re_fun, f)
- if found:
- if found == 1:
- possible_declarators.append(f)
- else:
- possible_definers.append(f)
+ try:
+ found = function_finder.find_specific_name(re_fun, f)
+ if found:
+ if found == 1:
+ possible_declarators.append(f)
+ else:
+ possible_definers.append(f)
+ except OSError as e:
+ print(f"error opening '{f}' ({e.errno}, {e.strerror}), skipping file")
def relative_path_to(start):
return lambda p: os.path.relpath(p, start=start)
diff --git a/share/analysis-scripts/function_finder.py b/share/analysis-scripts/function_finder.py
index e68f15ee479361b58be8bbea9284b2538b0130e5..7aef53cef0644df796ea85810fb9545c8de7c849 100755
--- a/share/analysis-scripts/function_finder.py
+++ b/share/analysis-scripts/function_finder.py
@@ -60,9 +60,9 @@ def prepare_re_specific_name(fname):
# Returns 0 if not found, 1 if declaration, 2 if definition
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)
+ with open(f, encoding="ascii", errors='ignore') as data:
+ file_content = data.read()
+ has_decl_or_def = prepared_re.search(file_content)
if has_decl_or_def is None:
return 0
else:
@@ -70,33 +70,35 @@ def find_specific_name(prepared_re, f):
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 definitions or declarations
+# if funcname is not None, only matches for the specified
+# function name
+def compute_re_def_or_decl(funcname):
+ id = funcname if funcname else c_identifier
+ return re.compile("^" + optional_type_prefix +
+ "(" + id + ")" + 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):
+def compute_newline_offsets(file_lines):
offsets = []
current = 0
- with open(filename, encoding="ascii", errors='ignore') as data:
- for line in data:
- current += len(line)
- offsets.append(current)
+ for line in file_lines:
+ 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
+ return bisect.bisect_right(offsets, offset) + 1
# Returns the line number (starting at 1) of each line starting with '}'
# as its first character.
@@ -104,12 +106,19 @@ def line_of_offset(offsets, offset):
# 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):
+def compute_closing_braces(file_lines):
braces = []
- with open(filename, encoding="ascii", errors='ignore') as data:
- for i, line in enumerate(data, start=1):
- if line.startswith("}"):
- braces.append(i)
+ for i, line in enumerate(file_lines, start=1):
+ # note: lines contain '\n', so they are never empty
+ if line[0] == '}':
+ braces.append(i)
+ # Special heuristics: if the last line contains whitespace + '}',
+ # assume it closes a function.
+ last_line_number = len(file_lines)+1
+ if file_lines != [] and not (last_line_number in braces):
+ last_line = file_lines[-1].lstrip()
+ if len(last_line) >= 1 and last_line[0] == '}':
+ braces.append(last_line_number)
return braces
# Returns the first element of [line_numbers] greater than [n], or [None]
@@ -118,10 +127,11 @@ def compute_closing_braces(filename):
#
# [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
+ try:
+ return line_numbers[bisect.bisect_left(line_numbers, n)]
+ except IndexError:
+ # could not find line (e.g. for closing braces); return None
+ return None
# Returns a list of tuples (fname, is_def, line_start, line_end, terminator_offset)
# for each function definition or declaration.
@@ -133,37 +143,38 @@ def get_first_line_after(line_numbers, n):
# [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()
+def find_definitions_and_declarations(want_defs, want_decls, filename, file_content, file_lines, newlines, funcname=None):
+ braces = compute_closing_braces(file_lines)
res = []
- for match in re.finditer(re_fundef_or_decl, content):
+ re_fundef_or_decl = compute_re_def_or_decl(funcname)
+ for match in re.finditer(re_fundef_or_decl, file_content):
funcname = match.group(1)
- is_def = match.group(2) == "{"
- is_decl = match.group(2) == ";"
+ terminator = match.group(2)
+ terminator_offset = match.start(2)
+ is_def = terminator == "{"
+ is_decl = terminator == ";"
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))
+ end = line_of_offset(newlines, terminator_offset)
else:
if not want_defs:
continue
- definition = content[match.start(1):newlines[start-1]]
+ definition = file_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))
+ end = line_of_offset(newlines, terminator_offset)
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("}"):
+ line_of_opening_brace = line_of_offset(newlines, terminator_offset)
+ if start == line_of_opening_brace and definition.rstrip()[-1] == '}':
# assume the '}' is closing the '{' from the same line
end = line_of_opening_brace
else:
@@ -171,7 +182,6 @@ def find_definitions_and_declarations(want_defs, want_decls, filename, newlines)
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))
@@ -184,12 +194,10 @@ calls_blacklist = ["if", "while", "for", "return", "sizeof", "switch", "_Alignas
#
# 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()
+def find_calls(file_content, newlines):
# create a list of Match objects that fit "pattern" regex
res = []
- for match in re.finditer(re_funcall, content):
+ for match in re.finditer(re_funcall, file_content):
funcname = match.group(1)
offset = match.start(1)
line = line_of_offset(newlines, offset)
diff --git a/share/analysis-scripts/heuristic_list_functions.py b/share/analysis-scripts/heuristic_list_functions.py
index ceee3fd5a3cf2892f1ed5c8fc8de5b8e76ce3c82..93c2d5c82f5c6cd5b45d5c3fcae6bf2f42579cb4 100755
--- a/share/analysis-scripts/heuristic_list_functions.py
+++ b/share/analysis-scripts/heuristic_list_functions.py
@@ -30,10 +30,6 @@ 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 = ""
@@ -55,8 +51,11 @@ 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)
+ with open(f, encoding="ascii", errors='ignore') as data:
+ file_content = data.read()
+ file_lines = file_content.splitlines(keepends=True)
+ newlines = function_finder.compute_newline_offsets(file_lines)
+ defs_and_decls = function_finder.find_definitions_and_declarations(want_defs, want_decls, f, file_content, file_lines, 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)")
diff --git a/share/analysis-scripts/list_files.py b/share/analysis-scripts/list_files.py
index ac822030be89c50fcde456d387e91d6708cc50f7..e39ae6cb6d2940e8fd7a8d54f9c4ca29a477a697 100755
--- a/share/analysis-scripts/list_files.py
+++ b/share/analysis-scripts/list_files.py
@@ -33,10 +33,6 @@ import json
import re
from pathlib import Path
-MIN_PYTHON = (3, 6) # for glob(recursive) and automatic Path conversions
-if sys.version_info < MIN_PYTHON:
- sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
-
if len(sys.argv) < 2:
# no argument, assume default name
arg = Path("compile_commands.json")
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index 6e47b60c60993be74bbc2d40a32e9cd45150f880..dad3225eeced1547e9ea2e295987b5b445a2d650 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -36,10 +36,6 @@ from subprocess import Popen, PIPE
from pathlib import Path
import function_finder
-MIN_PYTHON = (3, 6) # for glob(recursive) and automatic Path conversions
-if sys.version_info < MIN_PYTHON:
- sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
-
if len(sys.argv) > 2:
print(f"usage: {sys.argv[0]} [dir]")
print(" creates a Frama-C makefile in [dir] (default: .frama-c)")
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index 7f9f5b9b517b3be2e1eacdc325dad720ee5eed69..56fb52e0f8c1ce4b1f6937dfc15d6ff9f04f6601 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -34,10 +34,6 @@ import sys
from functools import partial
import tempfile
-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)
-
# Check if GNU make is available and has the minimal required version
# (4.0). Otherwise, this script will fail.
# We first test with 'gmake', then 'make', then fail.
diff --git a/share/analysis-scripts/normalize_jcdb.py b/share/analysis-scripts/normalize_jcdb.py
index 041baef52d449f8fb0e73d0c39a542ecf481f4c2..70cff41349cc48c7f2d218aea4a42bdee2a5b152 100755
--- a/share/analysis-scripts/normalize_jcdb.py
+++ b/share/analysis-scripts/normalize_jcdb.py
@@ -32,10 +32,6 @@ import json
import re
from pathlib import Path
-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)
-
if len(sys.argv) < 2:
# no argument, assume default name
arg = Path("compile_commands.json")
diff --git a/share/analysis-scripts/print_callgraph.py b/share/analysis-scripts/print_callgraph.py
index 9c5451669dc0955757608d50db117bb2249b7923..54822dd238817f2840a48fb5a3dd82cb69134890 100755
--- a/share/analysis-scripts/print_callgraph.py
+++ b/share/analysis-scripts/print_callgraph.py
@@ -28,10 +28,6 @@
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:
diff --git a/share/analysis-scripts/source_filter.py b/share/analysis-scripts/source_filter.py
new file mode 100644
index 0000000000000000000000000000000000000000..4156e072aee0fbf7b331d7fe8bbf18b2ae7b1a64
--- /dev/null
+++ b/share/analysis-scripts/source_filter.py
@@ -0,0 +1,90 @@
+#-*- 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 file provides some functions to open and filter source files
+# before they are used by other scripts. These filters help improve
+# the efficiency of regex-based heuristics.
+
+# These filters require external tools, either in the PATH, or in
+# environment variables (the latter has higher priority than the former).
+# - scc (a fork including option -k), to remove C comments (variable SCC);
+# - astyle, to re-indent lines (variable ASTYLE)
+# If a tool is absent, the filter is equivalent to a no-op.
+
+# These functions receive a file object (such as produced by open(),
+# subprocess.run, or a previous filter) and return a
+# file object containing the output. They abort execution in case
+# of errors when running the filters. Note that an absent tool
+# does _not_ lead to an error.
+
+import os
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+
+# warnings about missing commands are disabled during testing
+emit_warns = os.getenv("PTESTS_TESTING") == None
+
+# Returns a Path to the command binary, or None if it is not found
+# Emits a warning the first time it looks for a command
+warned = {}
+def get_command(command, env_var_name):
+ p = os.getenv(env_var_name)
+ if not p:
+ p = shutil.which(command)
+ if not p:
+ if emit_warns and command not in warned:
+ print(f"info: optional external command '{command}' not found in PATH; consider installing it or setting environment variable {env_var_name}")
+ warned[command] = True
+ return None
+ return Path(p)
+
+def run_and_check(command_and_args, input_data):
+ try:
+ return subprocess.check_output(command_and_args, input=input_data, stderr=None, encoding="ascii", errors="ignore")
+ except subprocess.CalledProcessError as e:
+ sys.exit(f"error running command: {command_and_args}\n{e}")
+
+def filter_with_scc(input_data):
+ scc = get_command("scc", "SCC")
+ if scc:
+ return run_and_check([scc, "-k"], input_data)
+ else:
+ return input_data
+
+def filter_with_astyle(input_data):
+ astyle = get_command("astyle", "ASTYLE")
+ if astyle:
+ return run_and_check([astyle, "--keep-one-line-blocks", "--keep-one-line-statements"], input_data)
+ else:
+ return input_data
+
+def open_and_filter(filename, apply_filters):
+ # we ignore encoding errors and use ASCII to avoid issues when
+ # opening files with different encodings (UTF-8, ISO-8859, etc)
+ with open(filename, "r", encoding="ascii", errors='ignore') as f:
+ data = f.read()
+ if apply_filters:
+ data = filter_with_astyle(filter_with_scc(data))
+ return data
diff --git a/share/compliance/posix_identifiers.json b/share/compliance/posix_identifiers.json
index b4badf4cb0004a8ee1a6cfd547a27f9981c0aac8..7fa5e758afd71b643f101a4c6a585f2e9b3e2539 100644
--- a/share/compliance/posix_identifiers.json
+++ b/share/compliance/posix_identifiers.json
@@ -3,7 +3,7 @@
"source":"POSIX.1-2008 - Base Specifications, Issue 7 (IEEE Std 1003.1-2008, 2016 Edition)",
"notes": {
"description": "The 'notes' field is a list of characteristics related to CWEs or that may affect the 'difficulty' of analyzing such headers or functions with Frama-C. Each note is succintly described below.",
- "fc-support":"How well Frama-C supports this construct, w.r.t. the C11 standard: 'unsupported', 'none', 'partial', or 'good'. The difference between 'unsupported' and 'none' is that the former means something requiring substantial changes to be supported by Frama-C, while the latter only means 'not tried yet'.",
+ "fc-support":"How well Frama-C supports this construct: 'unsupported', 'none', 'problematic', 'partial', or 'good'. The difference between 'unsupported' and 'none' is that the former means something requiring substantial changes to be supported by Frama-C, while the latter only means 'not tried yet'. 'problematic' indicates an identifier which is known to cause issues to code analyzers, e.g. setjmp.",
"variadic-plugin":"This is a variadic function known by the Variadic plug-in, which can (in some cases) generate a specification for it."
},
"id_types":[
@@ -58,7 +58,7 @@
"sched.h": {"fc-support":"partial", "extensions":[]},
"search.h": {"fc-support":"none", "extensions":["XSI"]},
"semaphore.h": {"fc-support":"partial", "extensions":[]},
- "setjmp.h": {"fc-support":"partial", "extensions":[]},
+ "setjmp.h": {"fc-support":"partial", "extensions":[], "notes":{"fc-support":"problematic"}},
"signal.h": {"fc-support":"partial", "extensions":[]},
"spawn.h": {"fc-support":"none", "extensions":["SPN"]},
"stdarg.h": {"fc-support":"good", "extensions":[]},
@@ -187,7 +187,7 @@
"_IOFBF": {"id_type":"macro", "header":"stdio.h", "extensions":[]},
"_IOLBF": {"id_type":"macro", "header":"stdio.h", "extensions":[]},
"_IONBF": {"id_type":"macro", "header":"stdio.h", "extensions":[]},
- "_longjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["OB","XSI"]},
+ "_longjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["OB","XSI"], "notes":{"fc-support":"problematic"}},
"_PC_2_SYMLINKS": {"id_type":"constant", "header":"unistd.h", "extensions":[]},
"_PC_ALLOC_SIZE_MIN": {"id_type":"constant", "header":"unistd.h", "extensions":[]},
"_PC_ASYNC_IO": {"id_type":"constant", "header":"unistd.h", "extensions":[]},
@@ -468,7 +468,7 @@
"_SC_XOPEN_UUCP": {"id_type":"constant", "header":"unistd.h", "extensions":[]},
"_SC_XOPEN_VERSION": {"id_type":"constant", "header":"unistd.h", "extensions":[]},
"_SC_XOPEN_XCU_VERSION": {"id_type":"constant", "header":"unistd.h", "extensions":["REM"]},
- "_setjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["OB","XSI"]},
+ "_setjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["OB","XSI"], "notes":{"fc-support":"problematic"}},
"_tolower": {"id_type":"function", "header":"ctype.h", "extensions":["OB","XSI"]},
"_toupper": {"id_type":"function", "header":"ctype.h", "extensions":["OB","XSI"]},
"_V6_ILP32_OFF32": {"id_type":"constant", "header":"unistd.h", "extensions":["REM"]},
@@ -1684,7 +1684,7 @@
"IXON": {"id_type":"constant", "header":"termios.h", "extensions":[]},
"j0": {"id_type":"function", "header":"math.h", "extensions":["XSI"]},
"j1": {"id_type":"function", "header":"math.h", "extensions":["XSI"]},
- "jmp_buf": {"id_type":"type", "header":"setjmp.h", "extensions":[]},
+ "jmp_buf": {"id_type":"type", "header":"setjmp.h", "extensions":[], "notes":{"fc-support":"problematic"}},
"jn": {"id_type":"function", "header":"math.h", "extensions":["XSI"]},
"jrand48": {"id_type":"function", "header":"stdlib.h", "extensions":["XSI"]},
"key_t": {"id_type":"type", "header":"sys/types.h", "extensions":[]},
@@ -1823,7 +1823,7 @@
"LONG_BIT": {"id_type":"macro", "header":"limits.h", "extensions":[]},
"LONG_MAX": {"id_type":"macro", "header":"limits.h", "extensions":[]},
"LONG_MIN": {"id_type":"macro", "header":"limits.h", "extensions":[]},
- "longjmp": {"id_type":"function", "header":"setjmp.h", "extensions":[]},
+ "longjmp": {"id_type":"function", "header":"setjmp.h", "extensions":[], "notes":{"fc-support":"problematic"}},
"lrand48": {"id_type":"function", "header":"stdlib.h", "extensions":["XSI"]},
"lrint": {"id_type":"function", "header":"math.h", "extensions":[]},
"lrintf": {"id_type":"function", "header":"math.h", "extensions":[]},
@@ -2910,7 +2910,7 @@
"setgrent": {"id_type":"function", "header":"grp.h", "extensions":["XSI"]},
"sethostent": {"id_type":"function", "header":"netdb.h", "extensions":[]},
"setitimer": {"id_type":"function", "header":"sys/time.h", "extensions":[]},
- "setjmp": {"id_type":"function", "header":"setjmp.h", "extensions":[]},
+ "setjmp": {"id_type":"function", "header":"setjmp.h", "extensions":[], "notes":{"fc-support":"problematic"}},
"setkey": {"id_type":"function", "header":"stdlib.h", "extensions":["XSI"]},
"setlocale": {"id_type":"function", "header":"locale.h", "extensions":[]},
"setlogmask": {"id_type":"function", "header":"syslog.h", "extensions":[]},
@@ -3010,9 +3010,9 @@
"SIGINT": {"id_type":"macro", "header":"signal.h", "extensions":[]},
"siginterrupt": {"id_type":"function", "header":"signal.h", "extensions":[]},
"sigismember": {"id_type":"function", "header":"signal.h", "extensions":[]},
- "sigjmp_buf": {"id_type":"type", "header":"setjmp.h", "extensions":["CX"]},
+ "sigjmp_buf": {"id_type":"type", "header":"setjmp.h", "extensions":["CX"], "notes":{"fc-support":"problematic"}},
"SIGKILL": {"id_type":"macro", "header":"signal.h", "extensions":[]},
- "siglongjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["CX"]},
+ "siglongjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["CX"], "notes":{"fc-support":"problematic"}},
"sigmask": {"id_type":"function", "header":"signal.h", "extensions":["REM"]},
"signal": {"id_type":"function", "header":"signal.h", "extensions":[]},
"signbit": {"id_type":"macro", "header":"math.h", "extensions":[]},
@@ -3032,7 +3032,7 @@
"SIGSEGV": {"id_type":"macro", "header":"signal.h", "extensions":[]},
"sigset": {"id_type":"function", "header":"signal.h", "extensions":[]},
"sigset_t": {"id_type":"type", "header":"signal.h", "extensions":[]},
- "sigsetjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["CX"]},
+ "sigsetjmp": {"id_type":"function", "header":"setjmp.h", "extensions":["CX"], "notes":{"fc-support":"problematic"}},
"sigstack": {"id_type":"type", "header":"signal.h", "extensions":["REM"]},
"SIGSTKSZ": {"id_type":"macro", "header":"signal.h", "extensions":[]},
"SIGSTOP": {"id_type":"macro", "header":"signal.h", "extensions":[]},
diff --git a/tests/fc_script/build-callgraph.i b/tests/fc_script/build-callgraph.i
index 7ec5a976aeb0b98d696992b666850cb7c6e497fa..be8f7b96630a6bac9c200980026fd29f01ddb347 100644
--- a/tests/fc_script/build-callgraph.i
+++ b/tests/fc_script/build-callgraph.i
@@ -1,6 +1,6 @@
/* 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_RESULT@/build-callgraph.res 2> @PTEST_RESULT@/build-callgraph.err
+ EXECNOW: LOG build-callgraph.res LOG build-callgraph.err PTESTS_TESTING=1 %{bin:frama-c-script} heuristic-print-callgraph @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_RESULT@/build-callgraph.res 2> @PTEST_RESULT@/build-callgraph.err
*/
#include <stdio.h>
diff --git a/tests/fc_script/estimate_difficulty.i b/tests/fc_script/estimate_difficulty.i
new file mode 100644
index 0000000000000000000000000000000000000000..23b63dd6c5250076eb5eb8e74f0197b0bd9a12cc
--- /dev/null
+++ b/tests/fc_script/estimate_difficulty.i
@@ -0,0 +1,28 @@
+/* run.config
+ NOFRAMAC: testing frama-c-script, not frama-c itself
+ EXECNOW: LOG @PTEST_NAME@.res LOG @PTEST_NAME@.err PTESTS_TESTING=1 %{bin:frama-c-script} estimate-difficulty @PTEST_FILE@ > @PTEST_NAME@.res 2> @PTEST_NAME@.err
+*/
+
+// these includes are not actually used by the compiler
+// (this is a preprocessed file), but analyzed by the script
+#include <sys/socket.h>
+# include <complex.h>
+ # include <langinfo.h>
+#include <sys/socket.h>
+
+void g() {
+ int g = 42;
+}
+
+void f() {
+ if (v) f();
+ else g();
+}
+
+int main() {
+ va_arg(); // no warning: it is a macro, not a function
+ setjmp(); // warning: problematic
+ strlen(); // no warning
+ ccosl(); // warning: neither code nor spec
+ dprintf(); // no warning: neither code nor spec, but handled by Variadic
+}
diff --git a/tests/fc_script/list_functions.i b/tests/fc_script/list_functions.i
index 448f97a30909dda8da6e3d773ed34336bf46e4a6..225f70d0a90bc31504e675d9bbaa7bc70503d7f8 100644
--- a/tests/fc_script/list_functions.i
+++ b/tests/fc_script/list_functions.i
@@ -15,5 +15,5 @@
DEPS: @PTEST_DEPS@ @PTEST_DIR@/build-callgraph.i
DEPS: @PTEST_DEPS@ @PTEST_DIR@/recursions.i
- EXECNOW: LOG heuristic_list_functions.res LOG heuristic_list_functions.err %{bin:frama-c-script} heuristic-list-functions true true @PTEST_DEPS@ > @PTEST_RESULT@/heuristic_list_functions.res 2> @PTEST_RESULT@/heuristic_list_functions.err
+ EXECNOW: LOG heuristic_list_functions.res LOG heuristic_list_functions.err PTESTS_TESTING=1 %{bin:frama-c-script} heuristic-list-functions true true @PTEST_DEPS@ > @PTEST_RESULT@/heuristic_list_functions.res 2> @PTEST_RESULT@/heuristic_list_functions.err
*/
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index d6526f2b234c2d45c42862eaf1d7c231c85f268f..cb1a6f9adc2a5443691c4809e7721d42a368ee3e 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -1,16 +1,15 @@
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
- DEPS: for-find-fun2.c for-find-fun.c main.c main2.c main3.c
- EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= %{bin:frama-c-script} -C @PTEST_DIR@ make-template $(basename @PTEST_RESULT@) < %{dep:@PTEST_DIR@/make_template.input} > @PTEST_RESULT@/make_template.res 2> @PTEST_RESULT@/make_template.err
+ COMMENT: the 'build' command cannot be tested because it requires 'glub'.
DEPS: main2.c main3.c main.c
- EXECNOW: LOG list_files.res LOG list_files.err %{bin:frama-c-script} list-files %{dep:@PTEST_DIR@/list_files.json} > @PTEST_RESULT@/list_files.res 2> @PTEST_RESULT@/list_files.err
+ EXECNOW: LOG list_files.res LOG list_files.err PTESTS_TESTING=1 %{bin:frama-c-script} list-files %{dep:@PTEST_DIR@/list_files.json} > @PTEST_RESULT@/list_files.res 2> @PTEST_RESULT@/list_files.err
DEPS: for-find-fun2.c for-find-fun.c for-list-functions.c main2.c main3.c main.c make-wrapper2.c make-wrapper3.c make-wrapper.c
- EXECNOW: LOG find_fun1.res LOG find_fun1.err %{bin:frama-c-script} find-fun main2 @PTEST_DIR@ > @PTEST_RESULT@/find_fun1.res 2> @PTEST_RESULT@/find_fun1.err
- EXECNOW: LOG find_fun2.res LOG find_fun2.err %{bin:frama-c-script} find-fun main3 @PTEST_DIR@ > @PTEST_RESULT@/find_fun2.res 2> @PTEST_RESULT@/find_fun2.err
- EXECNOW: LOG find_fun3.res LOG find_fun3.err %{bin:frama-c-script} find-fun false_positive @PTEST_DIR@ > @PTEST_RESULT@/find_fun3.res 2> @PTEST_RESULT@/find_fun3.err
+ EXECNOW: LOG find_fun1.res LOG find_fun1.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun main2 @PTEST_DIR@ > @PTEST_RESULT@/find_fun1.res 2> @PTEST_RESULT@/find_fun1.err
+ EXECNOW: LOG find_fun2.res LOG find_fun2.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun main3 @PTEST_DIR@ > @PTEST_RESULT@/find_fun2.res 2> @PTEST_RESULT@/find_fun2.err
+ EXECNOW: LOG find_fun3.res LOG find_fun3.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun false_positive @PTEST_DIR@ > @PTEST_RESULT@/find_fun3.res 2> @PTEST_RESULT@/find_fun3.err
DEPS:
- EXECNOW: LOG list_functions.res LOG list_functions.err %{bin:frama-c-script} list-functions %{dep:@PTEST_DIR@/for-find-fun2.c} %{dep:@PTEST_DIR@/for-list-functions.c} > @PTEST_RESULT@/list_functions.res 2> @PTEST_RESULT@/list_functions.err
- EXECNOW: LOG list_functions2.res LOG list_functions2.err LOG list_functions2.json %{bin:frama-c-script} list-functions %{dep:@PTEST_DIR@/for-find-fun2.c} %{dep:@PTEST_DIR@/for-list-functions.c -list-functions-declarations} -list-functions-output @PTEST_RESULT@/list_functions2.json -list-functions-debug 1 > @PTEST_RESULT@/list_functions2.res 2> @PTEST_RESULT@/list_functions2.err
+ EXECNOW: LOG list_functions.res LOG list_functions.err PTESTS_TESTING=1 %{bin:frama-c-script} list-functions %{dep:@PTEST_DIR@/for-find-fun2.c} %{dep:@PTEST_DIR@/for-list-functions.c} > @PTEST_RESULT@/list_functions.res 2> @PTEST_RESULT@/list_functions.err
+ EXECNOW: LOG list_functions2.res LOG list_functions2.err LOG list_functions2.json PTESTS_TESTING=1 %{bin:frama-c-script} list-functions %{dep:@PTEST_DIR@/for-find-fun2.c} %{dep:@PTEST_DIR@/for-list-functions.c -list-functions-declarations} -list-functions-output @PTEST_RESULT@/list_functions2.json -list-functions-debug 1 > @PTEST_RESULT@/list_functions2.res 2> @PTEST_RESULT@/list_functions2.err
*/
diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c
index 89700bc4aa9ecaac4668c8010ebc73edec3d2c26..0f7d0709e6eda239b3a706424d82b2f3b5d9cf00 100644
--- a/tests/fc_script/make-wrapper.c
+++ b/tests/fc_script/make-wrapper.c
@@ -2,7 +2,7 @@
MACRO: RM_TMP_DIR rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva
NOFRAMAC: testing frama-c-script
COMMENT: in case of errors, remove the 'grep' part to get the full output
- EXECNOW: LOG make-wrapper.res LOG make-wrapper.err (cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && @RM_TMP_DIR@ && FRAMAC=%{bin:frama-c} %{bin:frama-c-script} make-wrapper --make-dir . -f make-for-make-wrapper.mk | grep -A999999 "make-wrapper recommendations" && @RM_TMP_DIR@) > @PTEST_RESULT@/make-wrapper.res 2> @PTEST_RESULT@/make-wrapper.err
+ EXECNOW: LOG make-wrapper.res LOG make-wrapper.err (cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && @RM_TMP_DIR@ && FRAMAC=%{bin:frama-c} PTESTS_TESTING=1 %{bin:frama-c-script} make-wrapper --make-dir . -f make-for-make-wrapper.mk | grep -A999999 "make-wrapper recommendations" && @RM_TMP_DIR@) > @PTEST_RESULT@/make-wrapper.res 2> @PTEST_RESULT@/make-wrapper.err
*/
int defined(int a);
diff --git a/tests/fc_script/make_template.input b/tests/fc_script/make_template.input
deleted file mode 100644
index 6963df94935110ccdf0218b25973e3348c9e1947..0000000000000000000000000000000000000000
--- a/tests/fc_script/make_template.input
+++ /dev/null
@@ -1,10 +0,0 @@
-y
-fc_script_main
-for-find*.c main*.c
-y
-y
-y
-invalid_machdep
-n
-x86_64
-y
diff --git a/tests/fc_script/oracle/make_template.err b/tests/fc_script/oracle/estimate_difficulty.err
similarity index 100%
rename from tests/fc_script/oracle/make_template.err
rename to tests/fc_script/oracle/estimate_difficulty.err
diff --git a/tests/fc_script/oracle/estimate_difficulty.res b/tests/fc_script/oracle/estimate_difficulty.res
new file mode 100644
index 0000000000000000000000000000000000000000..6b197b724146d7ba3507c29a2979df06f1027627
--- /dev/null
+++ b/tests/fc_script/oracle/estimate_difficulty.res
@@ -0,0 +1,11 @@
+Building callgraph...
+Computing data about libc/POSIX functions...
+[recursion] found recursive cycle near estimate_difficulty.i:18: f -> f
+Estimating difficulty for 7 function calls...
+- warning: ccosl (POSIX) has neither code nor spec in Frama-C's libc
+- warning: setjmp (POSIX) is known to be problematic for code analysis
+Function-related warnings: 2
+Estimating difficulty for 3 '#include <header>' directives...
+- WARNING: included header <complex.h> is explicitly unsupported by Frama-C
+- warning: included header <langinfo.h> not currently included in Frama-C's libc
+Header-related warnings: 2
diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res
index f16fc61d2be3d40fae3e6b45961875fc0e7f0642..58bf804e3c123e33f21c6761b63dcefa26e2e129 100644
--- a/tests/fc_script/oracle/find_fun1.res
+++ b/tests/fc_script/oracle/find_fun1.res
@@ -1,4 +1,4 @@
-Looking for 'main2' inside 14 file(s)...
+Looking for 'main2' inside 15 file(s)...
Possible declarations for function 'main2' in the following file(s):
for-find-fun.c
Possible definitions for function 'main2' in the following file(s):
diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res
index fda8345bfc224212d8b8d653d325ed83b7acac7c..d868795ee4e11b8858e75185cfd91d68ea8a24e7 100644
--- a/tests/fc_script/oracle/find_fun2.res
+++ b/tests/fc_script/oracle/find_fun2.res
@@ -1,4 +1,4 @@
-Looking for 'main3' inside 14 file(s)...
+Looking for 'main3' inside 15 file(s)...
Possible declarations for function 'main3' in the following file(s):
for-find-fun2.c
Possible definitions for function 'main3' in the following file(s):
diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res
index 4a42d9117089960eb086c47a8e4b07b44795e3c3..00f4bbc10eab9c20620426e670d9d0cf6b715762 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 14 file(s)...
+Looking for 'false_positive' inside 15 file(s)...
No declaration/definition found for function 'false_positive'
diff --git a/tests/fc_script/oracle/heuristic_list_functions.res b/tests/fc_script/oracle/heuristic_list_functions.res
index c07b868d86a6faa808fac543c9825b4288dc37cd..b9cfea105053534f7a392710bc375f1b5bf61e1b 100644
--- a/tests/fc_script/oracle/heuristic_list_functions.res
+++ b/tests/fc_script/oracle/heuristic_list_functions.res
@@ -7,7 +7,7 @@ for-find-fun2.c:19:21: h (definition)
for-find-fun2.c:28:31: static_fun (definition)
for-list-functions.c:8:15: static_fun (definition)
for-list-functions.c:17:22: k (definition)
-main.c:18:20: main (definition)
+main.c:17:19: main (definition)
main2.c:6:8: fake_main (definition)
main2.c:10:12: domain (definition)
main2.c:14:16: main2 (definition)
diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res
deleted file mode 100644
index 4a3ef8e2f6c94cc2d096721b2e93d5f759fc82b3..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/make_template.res
+++ /dev/null
@@ -1,16 +0,0 @@
-Preparing template: GNUmakefile
-Running ptests: setting up mock files...
-warning: GNUmakefile already exists. Overwrite? [y/N] Main target name: Source files (default: **/*.c): The following sources were matched (relative to .):
- ./for-find-fun.c
- ./for-find-fun2.c
- ./main.c # defines 'main'
- ./main2.c
- ./main3.c # defines 'main'
-
-warning: 'main' seems to be defined multiple times.
-Is this ok? [Y/n] compile_commands.json exists, add option -json-compilation-database? [Y/n] Add stub for function main (only needed if it uses command-line arguments)? [y/N] Please define the architectural model (machdep) of the target machine.
-Known machdeps: x86_16 x86_32 x86_64 gcc_x86_16 gcc_x86_32 gcc_x86_64 ppc_32 msvc_x86_64
-Please enter the machdep [x86_64]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_64]: warning: fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: fc_stubs.c
-Template created: GNUmakefile
-Path to Frama-C binaries written to: path.mk
-Running ptests: cleaning up after tests...
diff --git a/tests/fc_script/recursions.i b/tests/fc_script/recursions.i
index 7d7cbfe0daab55000e646e4f72ada4a7a4d6525a..1d1f993cf17245094b713370b8ab32bcc941f2e4 100644
--- a/tests/fc_script/recursions.i
+++ b/tests/fc_script/recursions.i
@@ -1,6 +1,6 @@
/* 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_RESULT@/recursions.res 2> @PTEST_RESULT@/recursions.err
+ EXECNOW: LOG recursions.res LOG recursions.err PTESTS_TESTING=1 %{bin:frama-c-script} heuristic-detect-recursion @PTEST_FILE@ > @PTEST_RESULT@/recursions.res 2> @PTEST_RESULT@/recursions.err
*/
volatile int v;