diff --git a/Makefile b/Makefile
index 9b37922a1720555b0839db0ca6f186064b4dda95..be69328b95b0112741225168aa73fb212a998cba 100644
--- a/Makefile
+++ b/Makefile
@@ -275,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 \
@@ -1990,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 \
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 9b1284e3fbfb00c32470a8008affd78b1b791c82..014772a4d0b9acd3bd1918dcaa00670f64dea5b9 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -95,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."
@@ -225,10 +221,6 @@ case "$command" in
shift;
${FRAMAC_SHARE}/analysis-scripts/build.py "$@";
;;
- "make-template")
- shift;
- "${FRAMAC_SHARE}"/analysis-scripts/make_template.py "$@";
- ;;
"list-files")
shift;
"${FRAMAC_SHARE}"/analysis-scripts/list_files.py "$@";
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 7eef44ba09bb4562be65708698e210d792abaa1a..ed7274359e029f74d908804e7f177df5935b22ae 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -134,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
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index 9a89c3f67b277df2d5186ace181b70a8e13f593e..cb1a6f9adc2a5443691c4809e7721d42a368ee3e 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -1,7 +1,6 @@
/* 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=1 %{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 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
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/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.err b/tests/fc_script/oracle/make_template.err
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
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...