diff --git a/Makefile b/Makefile
index d6bba5965bcbc39ca650fd00b4838dfc36501569..432c0e8363f6b0598675ff68943e6266bc8ea1eb 100644
--- a/Makefile
+++ b/Makefile
@@ -254,22 +254,24 @@ DISTRIB_FILES:=\
Changelog config.h.in \
VERSION VERSION_CODENAME $(wildcard licenses/*) \
$(LIBC_FILES) \
+ share/analysis-scripts/analysis.mk \
share/analysis-scripts/benchmark_database.py \
share/analysis-scripts/cmd-dep.sh \
share/analysis-scripts/concat-csv.sh \
share/analysis-scripts/clone.sh \
share/analysis-scripts/creduce.sh \
- $(wildcard share/analysis-scripts/examples/*) \
+ share/analysis-scripts/epilogue.mk \
share/analysis-scripts/fc_stubs.c \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
- share/analysis-scripts/frama-c.mk \
share/analysis-scripts/frama_c_results.py \
+ share/analysis-scripts/function_finder.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/make_template.py \
share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/parse-coverage.sh \
+ share/analysis-scripts/prologue.mk \
share/analysis-scripts/README.md \
share/analysis-scripts/results_display.py \
share/analysis-scripts/summary.py \
@@ -1934,29 +1936,30 @@ install:: install-lib-$(OCAMLBEST)
share/configure.ac share/autocomplete_frama-c share/_frama-c \
$(FRAMAC_DATADIR)
$(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts
- $(CP) share/analysis-scripts/benchmark_database.py \
+ $(CP) \
+ share/analysis-scripts/analysis.mk \
+ share/analysis-scripts/benchmark_database.py \
share/analysis-scripts/cmd-dep.sh \
share/analysis-scripts/concat-csv.sh \
share/analysis-scripts/clone.sh \
share/analysis-scripts/creduce.sh \
+ share/analysis-scripts/epilogue.mk \
share/analysis-scripts/fc_stubs.c \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
- share/analysis-scripts/frama-c.mk \
share/analysis-scripts/frama_c_results.py \
+ share/analysis-scripts/function_finder.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/make_template.py \
share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/parse-coverage.sh \
+ share/analysis-scripts/prologue.mk \
share/analysis-scripts/README.md \
share/analysis-scripts/results_display.py \
share/analysis-scripts/summary.py \
share/analysis-scripts/template.mk \
$(FRAMAC_DATADIR)/analysis-scripts
- $(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts/examples
- $(CP) share/analysis-scripts/examples/* \
- $(FRAMAC_DATADIR)/analysis-scripts/examples
$(MKDIR) $(FRAMAC_DATADIR)/compliance
$(CP) share/compliance/c11_functions.json \
share/compliance/glibc_functions.json \
diff --git a/bin/frama-c-script b/bin/frama-c-script
index a3dfda783a26d79051a3392bfefc1a52cf7ee433..0683f0371d7a4b63a0caddd0335db2f9d71349c9 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -35,27 +35,27 @@ usage() {
echo " Display this help message and exit."
echo ""
echo " - make-template [dir]"
- echo " Interactively prepares a template for running analysis scripts,"
- echo " writing it to [dir/GNUmakefile]. [dir] is [.] if omitted."
+ echo " Interactively prepares a template for analyses,"
+ echo " writing it to dir/GNUmakefile [default: .frama-c]."
echo ""
- echo " - make-path"
+ echo " - make-path [dir]"
echo " [for Frama-C developers and advanced users without Frama-C in the path]"
- echo " Creates a frama-c-path.mk file in the current working directory."
+ echo " Creates a path.mk file in dir [default: .frama-c]."
echo ""
echo " - list-files [path/to/compile_commands.json]"
echo " Lists all sources in the given compile_commands.json"
- echo " (defaults to './compile_commands.json' if omitted)."
+ echo " [default: ./compile_commands.json]."
echo " Also lists files defining a 'main' function"
echo " (heuristics-based; neither correct nor complete)."
echo ""
- echo " - flamegraph <flamegraph.txt> [dir]"
- echo " Generates flamegraph.svg and flamegraph.html in [dir]"
- echo " (or in the FRAMAC_SESSION directory by default)."
+ echo " - flamegraph flamegraph.txt [dir]"
+ echo " Generates flamegraph.svg and flamegraph.html in dir"
+ echo " [default: FRAMAC_SESSION]."
echo " Also opens it in a browser, unless variable NOGUI is set."
echo ""
- echo " - find-fun <function-name> [dirs]"
- echo " Lists files in [dirs] declaring or defining <function-name>"
- echo " (defaults to PWD + /usr/include)."
+ echo " - find-fun function-name [dir...]"
+ echo " Lists files in dir... declaring or defining function-name"
+ echo " [default: PWD /usr/include]."
echo " Heuristics-based: neither correct nor complete."
echo ""
echo " - summary [options]"
@@ -63,20 +63,20 @@ usage() {
echo " in the current PWD."
echo " Use $0 summary --help for more informations."
echo ""
- echo " - configure <machdep>"
+ echo " - configure machdep"
echo " Runs an existing configure script to only consider files"
echo " in Frama-C's libc; this will hopefully disable non-essential"
echo " and non-POSIX external libraries."
- echo " <machdep> is necessary to define a required preprocessor symbol"
- echo " (run 'frama-c -machdep' help to get the list of machdeps)."
+ echo " (run 'frama-c -machdep help' to get the list of machdeps)."
echo ""
- echo " - make-wrapper <target> <args>"
- echo " Runs 'make <target> <args>', parsing the output to suggest"
+ echo " - make-wrapper target arg..."
+ echo " Runs 'make target arg...', parsing the output to suggest"
echo " useful commands in case of failure."
echo ""
echo " - normalize-jcdb [path/to/compile_commands.json]"
echo " Applies some transformations to an existing compile_commands.json"
- echo " (such as relativizing paths) to improve portability"
+ echo " (such as relativizing paths) to improve portability."
+ echo " [default: ./compile_commands.json]"
exit $1
}
@@ -85,7 +85,7 @@ if [ $# -lt 1 ]; then
fi
DIR="$( cd "$( dirname "$0" )" && pwd )"
-FRAMAC_SHARE=$("${DIR}/frama-c-config" -print-share-path)
+FRAMAC_SHARE=$("${DIR}/frama-c-config" -share)
if [ -z ${FRAMAC_SESSION+x} ]; then
FRAMAC_SESSION="./.frama-c";
fi
@@ -121,17 +121,31 @@ open_file() {
}
make_path() {
- cat <<EOF > frama-c-path.mk
+ dir=".frama-c"
+ if [ "$#" -gt 0 ]; then
+ dir="$1"
+ fi
+ if [ ! -d "$dir" ]; then
+ read -p "Directory '$dir' does not exist. Create it? [y/N] " yn
+ case $yn in
+ [Yy])
+ mkdir -p "$dir"
+ ;;
+ *)
+ echo "Exiting without creating."
+ exit 0;;
+ esac
+ fi
+ cat <<EOF > "${dir}/path.mk"
FRAMAC_DIR=${DIR}
ifeq (\$(wildcard \$(FRAMAC_DIR)),)
# Frama-C not installed locally; using the version in the PATH
else
FRAMAC=\$(FRAMAC_DIR)/frama-c
FRAMAC_GUI=\$(FRAMAC_DIR)/frama-c-gui
-FRAMAC_CONFIG=\$(FRAMAC_DIR)/frama-c-config
endif
EOF
- echo "Wrote to: frama-c-path.mk"
+ echo "Wrote to: ${dir}/path.mk"
}
flamegraph() {
@@ -232,11 +246,12 @@ case "$command" in
;;
"make-template")
shift;
- ${FRAMAC_SHARE}/analysis-scripts/make_template.py "$0" "$@";
+ export FRAMAC="${DIR}/frama-c"
+ ${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@";
;;
"make-path")
shift;
- make_path;
+ make_path "$@";
;;
"list-files")
shift;
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 67258fcf5c5904b29fbf2bc050108ba16dca68ab..a201e0f32e7a5d6c5491bb2f1e97396c84fe0add 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -111,26 +111,24 @@ ptests/.gitignore: .ignore
ptests/.merlin: .ignore
ptests/ptests.ml: CEA_LGPL
share/_frama-c: CEA_LGPL
+share/analysis-scripts/analysis.mk: CEA_LGPL
share/analysis-scripts/benchmark_database.py: .ignore
share/analysis-scripts/clone.sh: .ignore
share/analysis-scripts/creduce.sh: CEA_LGPL
+share/analysis-scripts/epilogue.mk: CEA_LGPL
share/analysis-scripts/fc_stubs.c: .ignore
-share/analysis-scripts/frama-c.mk: CEA_LGPL
share/analysis-scripts/frama_c_results.py: .ignore
share/analysis-scripts/cmd-dep.sh: .ignore
share/analysis-scripts/concat-csv.sh: .ignore
-share/analysis-scripts/examples/example.c: .ignore
-share/analysis-scripts/examples/example.mk: .ignore
-share/analysis-scripts/examples/example-multi.mk: .ignore
-share/analysis-scripts/examples/example-slevel.mk: .ignore
-share/analysis-scripts/examples/Makefile: .ignore
share/analysis-scripts/find_fun.py: .ignore
share/analysis-scripts/flamegraph.pl: CDDL
+share/analysis-scripts/function_finder.py: .ignore
share/analysis-scripts/git_utils.py: .ignore
share/analysis-scripts/list_files.py: .ignore
share/analysis-scripts/make_template.py: .ignore
share/analysis-scripts/make_wrapper.py: .ignore
share/analysis-scripts/parse-coverage.sh: .ignore
+share/analysis-scripts/prologue.mk: CEA_LGPL
share/analysis-scripts/README.md: .ignore
share/analysis-scripts/results_display.py: .ignore
share/analysis-scripts/summary.py: .ignore
diff --git a/share/analysis-scripts/.gitignore b/share/analysis-scripts/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..bee8a64b79a99590d5303307144172cfe824fbf7
--- /dev/null
+++ b/share/analysis-scripts/.gitignore
@@ -0,0 +1 @@
+__pycache__
diff --git a/share/analysis-scripts/README.md b/share/analysis-scripts/README.md
index 3e95700bb8e313539399c114698008e7adca0f5d..a92f12365c513addf3d1164b633d221e947f15aa 100644
--- a/share/analysis-scripts/README.md
+++ b/share/analysis-scripts/README.md
@@ -1,206 +1,4 @@
-This directory contains a set of a Makefile and several bash scripts which
-can be used to simplify non-trivial analyses with Frama-C and some of its
-plugins, in particular Eva.
-This Makefile can be included in your own Makefile for the following advantages.
+# Analysis scripts
-1. It ensures that no unnecessary work is done. If you change the Makefile,
- targets that have their command line affected will be rebuilt, but any
- target for which the command line doesn't change won't be rebuilt.
-2. It provides commonly used default parameters for the analysis. Note that
- you can still append new parameters or completely redefine them.
-3. It splits between parsing and analysis, storing outputs in separate
- repositories: <target>.parse for parsing-related outputs, and
- <target>.eva for Eva-related outputs.
-4. It produces several additional outputs after parsing and after an Eva
- analysis:
- * `<target>.parse/parse.log`, or `<target>.eva/eva.log`:
- contain the entire output of the parsing/analysis command,
- * `warnings.log`: only the warnings emitted by Frama-C/Eva,
- * `alarms.csv`: list of emitted alarms in csv form,
- * `metrics.log`: various metrics about the analysis,
- * `stats.txt`: stats about the analysis, such as user time,
- memory consumption, the date of the analysis, coverage of the analysis,
- number of warnings and alarms, and the command line arguments.
-5. It keeps copies of all previous analyses you have done in timestamped
- directories.
-
-
-Getting started
-===============
-
-There is a ready-to-use Makefile skeleton at the end of this section. If you
-want explanations about this Makefile, read this entire section.
-
-Other usage examples are available in Frama-C's Github open-source-case-studies
-repository: https://github.com/Frama-C/open-source-case-studies
-
-(If you have access to Frama-C's development repositories, you can also use
-the examples in `analysis-scripts/examples`.)
-
-Including analysis-scripts
--------------------
-
-This folder contains several shell scripts and, most importantly,
-the `frama-c.mk` file. This file is intended to be included at the top of your
-`GNUmakefile`:
-
-````
-include $(shell frama-c -print-share-path)/analysis-scripts/frama-c.mk
-````
-
-The file is named `GNUmakefile` instead of `Makefile` for pragmatic reasons:
-in GNU Make, the file `GNUmakefile`, if it exists, takes precedence over a
-`Makefile`, which avoid having to rename existing Makefiles and having to
-manually specify the Makefile to use when running make (e.g. via `-f`).
-The analysis-scripts Makefile relies on GNU-specific features anyway.
-
-By default, the scripts use the frama-c binaries located in your `$PATH`
-environment variable. You may want to specify different binaries, but, if you
-want to version your analysis, this path will depend on the computer it is run
-on. So, we recommend you use an unversioned file `frama-c-path.mk`. Add this
-file to your `.gitignore` and define the `FRAMAC` and `FRAMAC_GUI`
-variables there. For instance:
-
-````
-FRAMAC_DIR=frama-c/bin
-FRAMAC=$(FRAMAC_DIR)/frama-c
-FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui
-````
-
-And include this file before `frama-c.mk` in your Makefile. As this file
-is computer dependent and unversioned, it will not always be present. Prefix
-the include command with a minus sign `-` to tell `make` to ignore missing
-files:
-
-````
--include frama-c-path.mk
-````
-
-Then, to handle both cases when Frama-C is in the path, and when it is not,
-use the following conditional definition of `FRAMAC` followed by the
-inclusion of `frama-c.mk`:
-
-```
-FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-```
-
-
-Defining analysis global parameters
------------------------------------
-
-Once `frama-c.mk` is included, you may change default values of variables.
-Most usual variables you may want to change are `CPPFLAGS`, `FCFLAGS`
-and `EVAFLAGS`. For example:
-
-````
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-````
-
-Some arguments are passed to Frama-C from the environment. This is the
-case of the `FRAMA_C_MEMORY_FOOTPRINT` variable. You can set it in your
-Makefile with the following line:
-
-````
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-````
-
-The two steps of the analysis
------------------------------
-
-Parsing might be long on some analyses. The analysis scripts save the result
-of the parsing phase so that it is not redone when modifying only analysis
-parameters but not parsing parameters.
-
-The parsing result is saved in a `<target>.parse` directory while the result
-of the analysis is saved in a `<target>.eva` directory.
-The second automatically depends on the first.
-Thus, each time you require that make build the `.eva` target,
-it will build the `.parse` one first.
-
-````
-all: example.eva
-````
-
-
-Defining analysis sources
--------------------------
-
-To define the set of sources to analyze, you must define them as dependencies
-of your `.parse` target.
-
-````
-example.parse: file1.c file2.c file3.c ...
-````
-
-As they are dependencies, parsing will be remade if the sources change.
-
-
-Defining project-specific parameters
-------------------------------------
-
-You can describe several analyses with the same Makefile. We call these
-analyses "projects". Projects are not likely to share the exact same
-parameters. Thus, it is useful to define these parameters project wise.
-`make` allows this by putting the variable definition after the target. For
-instance:
-
-````
-example.parse: CPPFLAGS += -D__FRAMAC__
-example.eva: FCFLAGS += -main my_main
-example.eva: EVAFLAGS += -slevel 500
-````
-
-
-Full example
-------------
-
-### `GNUmakefile`
-
-````
-# optional include, in case frama-c-path.mk does not exist (frama-c in the PATH)
--include frama-c-path.mk
-# frama-c-config is used to find the analysis scripts and frama-c.mk
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Global parameters
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default targets
-all: example.eva
-
-# Input files
-example.parse: example.c
-
-# Project-specific parameters
-example.parse: CPPFLAGS += -D__FRAMAC__
-example.eva: FCFLAGS += -main my_main
-example.eva: EVAFLAGS += -slevel 500
-````
-
-### `frama-c-path.mk`
-
-````
-FRAMAC_DIR=frama-c/bin
-FRAMAC=$(FRAMAC_DIR)/frama-c
-FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui
-````
-
-### `.gitignore`
-
-````
-*.parse*
-*.eva*
-*.crash
-command
-parse.log
-eva.log
-stats.txt
-frama-c-path.mk
-````
+Documentation related to the contents of this directory is available in the
+Frama-C User Manual, chapter "Analysis scripts".
diff --git a/share/analysis-scripts/frama-c.mk b/share/analysis-scripts/analysis.mk
similarity index 89%
rename from share/analysis-scripts/frama-c.mk
rename to share/analysis-scripts/analysis.mk
index b427e63aef0dcf4fe43462cc1ce061c469d05b1a..8a4d48e462d499bb3ac3a400946be46e61efe86f 100644
--- a/share/analysis-scripts/frama-c.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -20,23 +20,19 @@
# #
##########################################################################
-# This file is intended to be included by a classic Makefile when doing
-# non-trivial analyses with Frama-C and its Eva plugin. For instance, you
-# can start your Makefile with the following line:
-#
-# include path/to/frama-c.mk
+# Makefile for Frama-C/Eva case studies.
+# This file is included by epilogue.mk, when using template.mk.
+# See the Frama-C User Manual for more details.
#
# This Makefile uses the following variables.
#
-# FRAMAC the frama-c binary
-# FRAMAC_GUI the frama-c gui binary
+# FRAMAC frama-c binary
+# FRAMAC_GUI frama-c gui binary
# CPPFLAGS preprocessing flags
+# MACHDEP machdep
# FCFLAGS general flags to use with frama-c
# FCGUIFLAGS flags to use with frama-c-gui
# EVAFLAGS flags to use with the Eva plugin
-# SLEVEL the part of the frama-c command line concerning slevel
-# (you can use EVAFLAGS for this, if you don't intend
-# to use slevel-tweaker.sh)
# EVABUILTINS Eva builtins to be set (via -eva-builtin)
# EVAUSESPECS Eva functions to be overridden by specs (-eva-use-spec)
#
@@ -52,15 +48,14 @@
# With command line arguments:
# make FRAMAC=~/bin/frama-c
#
-# In your Makefile, when you want to change a parameter for all analyses :
+# In your Makefile, when you want to change a parameter for all analyses:
# FCFLAGS += -verbose 2
#
# In your Makefile, for a single target :
# target.eva: FCFLAGS += -main my_main
#
-# In order to define an analysis target named target, you must in addition
-# give the list of source files containing the code to be analyzed by adding
-# them as dependencies of target.parse, a in
+# For each analysis target, you must give the list of sources to be analyzed
+# by adding them as prerequisites of target.parse, as in:
#
# target.parse: file1.c file2.c file3.c...
#
@@ -71,6 +66,8 @@ ifneq (4.0,$(firstword $(sort $(MAKE_VERSION) 4.0)))
endif
# Test if on a Mac (and therefore sed has fewer options)
+# Also test if /usr/bin/time is available, otherwise use the shell builtin
+# (which has less options)
UNAME := $(shell uname -s)
ifeq ($(UNAME),Darwin)
SED_UNBUFFERED:=sed
@@ -116,7 +113,6 @@ fc_list = $(subst $(space),$(comma),$(strip $1))
FRAMAC ?= frama-c
FRAMAC_SCRIPT = $(FRAMAC)-script
FRAMAC_GUI ?= frama-c-gui
-SLEVEL ?=
EVAFLAGS ?= \
-eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state \
-eva-print-callstacks -eva-warn-key alarm=inactive \
@@ -146,7 +142,6 @@ clean-backups:
# --- Generic rules ---
-TIMESTAMP := $(shell date +"%Y-%m-%d_%H-%M-%S")
HR_TIMESTAMP := $(shell date +"%H:%M:%S %d/%m/%Y")# Human readable
DIR := $(dir $(lastword $(MAKEFILE_LIST)))
SHELL := /bin/bash
@@ -161,7 +156,7 @@ SHELL := /bin/bash
@#
%.parse: SOURCES = $(filter-out %/command,$^)
-%.parse: PARSE = $(FRAMAC) $(FCFLAGS) -cpp-extra-args="$(CPPFLAGS)" $(SOURCES)
+%.parse: PARSE = $(FRAMAC) $(FCFLAGS) $(if $(value MACHDEP),-machdep $(MACHDEP),) -cpp-extra-args="$(CPPFLAGS)" $(SOURCES)
%.parse: $$(if $$^,,.IMPOSSIBLE) $$(shell $(DIR)cmd-dep.sh $$@/command $$(PARSE))
@$(call display_command,$(PARSE))
mkdir -p $@
@@ -226,7 +221,6 @@ SHELL := /bin/bash
fi
mv $@/{running,command}
touch $@ # Update timestamp and prevents remake if nothing changes
- cp -r $@ $*_$(TIMESTAMP).eva
%.gui: %
$(FRAMAC_GUI) $(FCGUIFLAGS) -load $^/framac.sav &
diff --git a/share/analysis-scripts/epilogue.mk b/share/analysis-scripts/epilogue.mk
new file mode 100644
index 0000000000000000000000000000000000000000..ca49ed6bc7b9fdf07d6871a42123c6b277941b1f
--- /dev/null
+++ b/share/analysis-scripts/epilogue.mk
@@ -0,0 +1,40 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# 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). #
+# #
+##########################################################################
+
+# Makefile template epilogue for analyses with Frama-C/Eva.
+# For details and usage information, see the Frama-C User Manual.
+
+# Some targets provided for convenience
+# Note: they all depend on TARGETS having been properly set by the user
+eva: $(TARGETS)
+parse: $(TARGETS:%.eva=%.parse)
+# Opening one GUI for each target is cumbersome; we open only the first target
+gui: $(firstword $(TARGETS)).gui
+
+# Default target
+all: eva
+ifeq ($(TARGETS),)
+ @echo "error: TARGETS is empty"
+endif
+
+display-targets:
+ @echo "$(addprefix .frama-c/,$(TARGETS))"
diff --git a/share/analysis-scripts/examples/Makefile b/share/analysis-scripts/examples/Makefile
deleted file mode 100644
index 5aca1b8993332028c06307a15a9a5ff74e4eef2e..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/examples/Makefile
+++ /dev/null
@@ -1,18 +0,0 @@
-TARGETS=example example-multi example-slevel
-
-.PHONY: all update-submodules clean $(TARGETS)
-
-all: $(TARGETS)
-
-update-submodules:
- git submodule update --init --recursive --remote
-
-clean:
- @for f in $(TARGETS); \
- do \
- $(MAKE) --no-print-directory --file $$f.mk clean; \
- done
-
-$(TARGETS): %: %.mk
- @$(MAKE) --no-print-directory --file $<
-
diff --git a/share/analysis-scripts/examples/example-multi.mk b/share/analysis-scripts/examples/example-multi.mk
deleted file mode 100644
index fa25003a7127116c5195395fea4e4c1abe1e8880..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/examples/example-multi.mk
+++ /dev/null
@@ -1,23 +0,0 @@
--include frama-c-path.mk
-FRAMAC ?= frama-c
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Global parameters
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-EVABUILTINS += memset:Frama_C_memset memcpy:Frama_C_memcpy
-
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default targets
-all: example1.val example2.val
-
-# Input files
-example1.parse example2.parse: example.c
-
-# Project specific parameters
-example1.parse: CPPFLAGS += -D__FRAMAC__
-example1.val: FCFLAGS += -main my_main
-example2.val: EVAFLAGS += -slevel 500
-example2.val: FCFLAGS += -main main
diff --git a/share/analysis-scripts/examples/example-slevel.mk b/share/analysis-scripts/examples/example-slevel.mk
deleted file mode 100644
index d623a913abbe3b396cce5f4e2c7d02e115c96536..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/examples/example-slevel.mk
+++ /dev/null
@@ -1,37 +0,0 @@
-# This example is the same as example-multi.mk but pay attention to the
-# following changes :
-# 1. slevel is set inside SLEVEL variable instead of EVAFLAGS to allow
-# overriding when testing specific slevels
-# 2. A percent (%) is used in example1.% and example2.% so that
-# options are used also for instance for example1.5000.val which
-# is the same target as example1.val but with 5000 slevel.
-# 3. The all rule invoke the script
-
--include frama-c-path.mk
-FRAMAC ?= frama-c
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Global parameters
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-EVABUILTINS += memset:Frama_C_memset memcpy:Frama_C_memcpy
-
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default targets
-all:
- $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/slevel-tweaker.sh -f example-slevel.mk example1 example2
-
-# Clean
-clean::
- $(RM) slevel-tweaker.log
-
-# Input files
-example1.parse example2.parse: example.c
-
-# Project specific parameters
-example1.parse: CPPFLAGS += -D__FRAMAC__
-example1.%: FCFLAGS += -main my_main
-example2.%: SLEVEL += -slevel 500
-example2.%: FCFLAGS += -main main
diff --git a/share/analysis-scripts/examples/example.c b/share/analysis-scripts/examples/example.c
deleted file mode 100644
index ed7983016f1d3b02737c6f9a909fbd7a8ce29867..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/examples/example.c
+++ /dev/null
@@ -1,25 +0,0 @@
-#include <string.h>
-
-char s[10], t[10];
-
-int f()
-{
- memset(s, 0, 10);
- memcpy(t, s, 10);
- return 42;
-}
-
-void main(void)
-{
- f();
-}
-
-
-#ifdef __FRAMAC__
-
-int my_main(void)
-{
- return f();
-}
-
-#endif
diff --git a/share/analysis-scripts/examples/example.mk b/share/analysis-scripts/examples/example.mk
deleted file mode 100644
index 4a6130de5b3ea37c40629d1ea16052ffde4ee613..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/examples/example.mk
+++ /dev/null
@@ -1,26 +0,0 @@
-# frama-c-path.mk contains variables which are specific to each
-# user and should not be versioned, such as the path to the
-# frama-c binaries (e.g. FRAMAC and FRAMAC_GUI).
-# It is an optional include, unnecessary if frama-c is in the PATH
--include frama-c-path.mk
-# FRAMAC is defined in frama-c-path.mk when it is included, so the
-# line below will be safely ignored if this is the case
-FRAMAC ?= frama-c
-# frama-c.mk should be included at the top of your Makefile, right below
-# the inclusion of frama-c-path.mk
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Define global parameters
-CPPFLAGS += -D__I586__ -D__FRAMAC__
-FCFLAGS += -verbose 0 -main my_main
-EVAFLAGS += -plevel 611
-EVABUILTINS += memset:Frama_C_memset memcpy:Frama_C_memcpy
-
-# Export environment variable for Frama-C
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default target
-all: example.val
-
-# List input files
-example.parse: example.c
diff --git a/share/analysis-scripts/find_fun.py b/share/analysis-scripts/find_fun.py
index 62692663c2d69264531afde5d048fb4974d3278b..5cb0b65863adcf8606a34d59d9156200b73a8f39 100755
--- a/share/analysis-scripts/find_fun.py
+++ b/share/analysis-scripts/find_fun.py
@@ -29,6 +29,7 @@ import sys
import os
import re
import glob
+import function_finder
MIN_PYTHON = (3, 5) # for glob(recursive)
if sys.version_info < MIN_PYTHON:
@@ -67,36 +68,16 @@ for d in dirs:
files += glob.glob(d + "/**/*.[ich]", recursive=True)
print("Looking for '%s' inside %d file(s)..." % (fname, len(files)))
-#print("\n".join(files))
-
-# To minimize the amount of false positives, we try to match the following:
-# - the line must begin with a C identifier (declarations and definitions in C
-# rarely start with spaces in the line), or with the function name itself
-# (supposing the return type is in the previous line)
-# - any number of identifiers are allowed (to allow for 'struct', 'volatile',
-# 'extern', etc)
-# - asterisks are allowed both before and after identifiers, except for the
-# first one (to allow for 'char *', 'struct **ptr', etc)
-# - identifiers are allowed after the parentheses, to allow for some macros/
-# modifiers
possible_declarators = []
possible_definers = []
-c_identifier = "[a-zA-Z_][a-zA-Z0-9_]*"
-c_id_maybe_pointer = c_identifier + "\**"
-type_prefix = c_id_maybe_pointer + "(?:\s+\**" + c_id_maybe_pointer + ")*\s+\**"
-parentheses_suffix = "\s*\([^)]*\)"
-re_fun = re.compile("^(?:" + type_prefix + "\s*)?" + fname + parentheses_suffix
- + "\s*(?:" + c_identifier + ")?\s*(;|{)", flags=re.MULTILINE)
+re_fun = function_finder.prepare(fname)
for f in files:
- with open(f, encoding="ascii", errors='ignore') as content_file:
- content = content_file.read()
- has_decl_or_def = re_fun.search(content)
- if has_decl_or_def is not None:
- is_decl = has_decl_or_def.group(1) == ";"
- if is_decl:
+ found = function_finder.find(re_fun, f)
+ if found:
+ if found == 1:
possible_declarators.append(f)
- else:
+ else:
possible_definers.append(f)
if possible_declarators == [] and possible_definers == []:
diff --git a/share/analysis-scripts/function_finder.py b/share/analysis-scripts/function_finder.py
new file mode 100644
index 0000000000000000000000000000000000000000..ee43f29adfb7ac6b75544622045a75cbceb5b003
--- /dev/null
+++ b/share/analysis-scripts/function_finder.py
@@ -0,0 +1,59 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# 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). #
+# #
+##########################################################################
+
+# Exports find_function_in_file, to be used by other scripts
+
+import re
+
+# To minimize the amount of false positives, we try to match the following:
+# - the line must begin with a C identifier (declarations and definitions in C
+# rarely start with spaces in the line), or with the function name itself
+# (supposing the return type is in the previous line)
+# - any number of identifiers are allowed (to allow for 'struct', 'volatile',
+# 'extern', etc)
+# - asterisks are allowed both before and after identifiers, except for the
+# first one (to allow for 'char *', 'struct **ptr', etc)
+# - identifiers are allowed after the parentheses, to allow for some macros/
+# modifiers
+
+# Precomputes the regex for 'fname'
+def prepare(fname):
+ c_identifier = "[a-zA-Z_][a-zA-Z0-9_]*"
+ c_id_maybe_pointer = c_identifier + "\**"
+ type_prefix = c_id_maybe_pointer + "(?:\s+\**" + c_id_maybe_pointer + ")*\s+\**"
+ parentheses_suffix = "\s*\([^)]*\)"
+ re_fun = re.compile("^(?:" + type_prefix + "\s*)?" + fname + parentheses_suffix
+ + "\s*(?:" + c_identifier + ")?\s*(;|{)", flags=re.MULTILINE)
+ return re_fun
+
+# Returns 0 if not found, 1 if declaration, 2 if definition
+def find(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)
+ if has_decl_or_def is None:
+ return 0
+ else:
+ is_decl = has_decl_or_def.group(1) == ";"
+ return 1 if is_decl else 2
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index bf862b7b51cc03b574ae4b84fb7e50628a1616f6..419dc9d443072b29d39e93c44040e05bc1596624 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -28,38 +28,58 @@
import sys
import os
import re
+import shutil
+import shlex
+import glob
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) > 3:
- print("usage: %s path-to-frama-c-script [dir]" % sys.argv[0])
- print(" creates a GNUmakefile for running Frama-C on a set of files,")
- print(" interactively filling a template.")
+if len(sys.argv) > 2:
+ print(f"usage: {sys.argv[0]} [dir]")
+ print(" creates a Frama-C makefile in [dir] (default: .frama-c)")
sys.exit(1)
-if not os.path.isfile(sys.argv[1]):
- print("error: path to frama-c-script is not a file: " + sys.argv[1])
- sys.exit(1)
+framac_in_path = True
+framac = shutil.which("frama-c")
+if not framac:
+ framac_in_path = False
+ if os.environ.get("FRAMAC"):
+ framac = os.environ["FRAMAC"]
+ else:
+ sys.exit("error: frama-c must be in the PATH, "\
+ "or in environment variable FRAMAC")
jcdb = Path("compile_commands.json")
+dir = Path(sys.argv[1] if len(sys.argv) == 2 else ".frama-c")
+fc_stubs_c = dir / "fc_stubs.c"
+gnumakefile = dir / "GNUmakefile"
+
+print(f"Preparing template: {gnumakefile}")
+
+# relative prefix, due to GNUmakefile possibly being in a sub-directory of PWD
+relprefix = os.path.relpath(os.getcwd(), dir)
+
if "PTESTS_TESTING" in os.environ:
print("Running ptests: setting up mock files...")
jcdb.touch()
+ Path(dir).mkdir(parents=True, exist_ok=True)
+ fc_stubs_c.touch()
+ gnumakefile.touch()
-bindir = Path(os.path.dirname(os.path.abspath(sys.argv[1])))
+bindir = Path(os.path.dirname(os.path.abspath(framac)))
frama_c_config = bindir / "frama-c-config"
-process = Popen([frama_c_config, "-print-share-path"], stdout=PIPE)
+process = Popen([frama_c_config, "-share"], stdout=PIPE)
(output, err) = process.communicate()
output = output.decode('utf-8')
exit_code = process.wait()
if exit_code != 0:
- print("error running frama-c-config")
- sys.exit(1)
+ sys.exit("error running frama-c-config")
sharedir = Path(output)
def get_known_machdeps():
@@ -68,41 +88,83 @@ def get_known_machdeps():
output = output.decode('utf-8')
exit_code = process.wait()
if exit_code != 0:
- print("error getting machdeps: " + output)
- sys.exit(1)
+ sys.exit("error getting machdeps: " + output)
match = re.match("\[kernel\] supported machines are (.*) \(default is (.*)\).", output, re.DOTALL)
if not match:
- print("error getting known machdeps: " + output)
- sys.exit(1)
+ sys.exit("error getting known machdeps: " + output)
machdeps = match.group(1).split()
default_machdep = match.group(2)
return (default_machdep, machdeps)
-dir = Path(sys.argv[2] if len(sys.argv) == 3 else ".")
-gnumakefile = dir / "GNUmakefile"
-
def check_path_exists(path):
if os.path.exists(path):
- yn = input("warning: {} already exists. Overwrite? [y/N] ".format(path))
+ yn = input(f"warning: {path} already exists. Overwrite? [y/N] ")
if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
print("Exiting without overwriting.")
sys.exit(0)
+ pathdir = os.path.dirname(path)
+ if not os.path.exists(pathdir):
+ yn = input(f"warning: directory '{pathdir}' does not exit. Create it? [y/N] ")
+ if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
+ print("Exiting without creating.")
+ sys.exit(0)
+ Path(pathdir).mkdir(parents=True, exist_ok=False)
check_path_exists(gnumakefile)
main = input("Main target name: ")
if not re.match("^[a-zA-Z_0-9]+$", main):
- print("error: invalid main target name")
- sys.exit(1)
+ sys.exit("error: invalid main target name (can only contain letters, digits, dash or underscore)")
+
+main_fun_finder_re = function_finder.prepare("main")
+
+# returns 0 if none, 1 if declaration, 2 if definition
+def defines_or_declares_main(f):
+ return function_finder.find(main_fun_finder_re, f)
+
+def expand_and_normalize_sources(expression, relprefix):
+ subexps = shlex.split(expression)
+ sources_lists = [glob.glob(exp, recursive=True) for exp in subexps]
+ sources = sorted(set([item for sublist in sources_lists for item in sublist]))
+ return sources
-sources = input("Source files separated by spaces (default if empty: *.c): ")
-if not sources:
- sources="*.c"
+def rel_prefix(f):
+ return f"{f}" if os.path.isabs(f) else f"{relprefix}/{f}"
+
+def sources_list_for_makefile(sources):
+ return "\n".join([f" {rel_prefix(source)} \\" for source in sources])
+
+def main_suffix(f):
+ main = defines_or_declares_main(f)
+ if main == 2:
+ return "\t# defines 'main'"
+ elif main == 1:
+ return "\t# declares 'main'"
+ else:
+ return ""
+
+while True:
+ sources = input("Source files (default: **/*.c): ")
+ if not sources:
+ sources="**/*.c"
+ source_list = expand_and_normalize_sources(sources, relprefix)
+ if not source_list:
+ print(f"error: no sources were matched for '{sources}'.")
+ else:
+ print(f"The following sources were matched (relative to {dir}):")
+ print("\n".join([" " + rel_prefix(source) + main_suffix(source) for source in source_list]))
+ print()
+ definitions_of_main = len([source for source in source_list if defines_or_declares_main(source)])
+ if definitions_of_main > 1:
+ print("warning: 'main' seems to be defined multiple times.")
+ yn = input("Is this ok? [Y/n] ")
+ if yn == "" or not (yn[0] == "N" or yn[0] == "n"):
+ break
json_compilation_database = None
if jcdb.is_file():
yn = input("compile_commands.json exists, add option -json-compilation-database? [Y/n] ")
if yn == "" or not (yn[0] == "N" or yn[0] == "n"):
- json_compilation_database = "."
+ json_compilation_database = f"{relprefix}/compile_commands.json"
else:
print("Option not added; you can later add it to FCFLAGS.")
@@ -110,20 +172,19 @@ add_main_stub = False
yn = input("Add stub for function main (only needed if it uses command-line arguments)? [y/N] ")
if yn != "" and (yn[0] == "Y" or yn[0] == "y"):
add_main_stub = True
- sources = "fc_stubs.c " + sources
print("Please define the architectural model (machdep) of the target machine.")
(default_machdep, machdeps) = get_known_machdeps()
print("Known machdeps: " + " ".join(machdeps))
machdep_chosen = False
while not machdep_chosen:
- machdep = input("Please enter the machdep [" + default_machdep + "]: ")
+ machdep = input(f"Please enter the machdep [{default_machdep}]: ")
if not machdep:
machdep = default_machdep
machdep_chosen = True
else:
if not (machdep in machdeps):
- yn = input("'{}' is not a standard machdep. Proceed anyway? [y/N]".format(machdep))
+ yn = input(f"'{machdep}' is not a standard machdep. Proceed anyway? [y/N]")
if yn != "" and (yn[0] == "Y" or yn[0] == "y"):
machdep_chosen = True
else:
@@ -135,17 +196,21 @@ def insert_line_after(lines, line_pattern, newline):
if re_line.search(lines[i]):
lines.insert(i+1, newline)
return lines
- print("error: no lines found matching pattern: " + line_pattern)
- sys.exit(1)
+ sys.exit(f"error: no lines found matching pattern: {line_pattern}")
-def replace_line(lines, line_pattern, value):
+def replace_line(lines, line_pattern, value, all_occurrences=False):
+ replaced = False
re_line = re.compile(line_pattern)
for i in range(0, len(lines)):
if re_line.search(lines[i]):
lines[i] = value
- return lines
- print("error: no lines found matching pattern: " + line_pattern)
- sys.exit(1)
+ replaced = True
+ if not all_occurrences:
+ return lines
+ if replaced:
+ return lines
+ else:
+ sys.exit(f"error: no lines found matching pattern: {line_pattern}")
def remove_lines_between(lines, start_pattern, end_pattern):
re_start = re.compile(start_pattern)
@@ -159,34 +224,39 @@ def remove_lines_between(lines, start_pattern, end_pattern):
last_to_remove = i
break
if first_to_remove == -1:
- print("error: could not find start pattern: " + start_pattern)
- sys.exit(1)
+ sys.exit("error: could not find start pattern: " + start_pattern)
elif last_to_remove == -1:
- print("error: could not find end pattern: " + end_pattern)
- sys.exit(1)
+ sys.exit("error: could not find end pattern: " + end_pattern)
return (lines[:first_to_remove-1] if first_to_remove > 0 else []) + (lines[last_to_remove+1:] if last_to_remove < len(lines)-1 else [])
with open(sharedir / "analysis-scripts" / "template.mk") as f:
lines = list(f)
- lines = replace_line(lines, "^MAIN_TARGET :=", "MAIN_TARGET := {}\n".format(main))
- lines = remove_lines_between(lines, "Remove these lines.*main target", "^endif")
- lines = replace_line(lines, "^\$\(MAIN_TARGET\).parse:", "$(MAIN_TARGET).parse: {}\n".format(sources))
- if json_compilation_database:
- lines = insert_line_after(lines, "^FCFLAGS", " -json-compilation-database {} \\\n".format(json_compilation_database))
- lines = insert_line_after(lines, "^FCFLAGS", " -machdep {} \\\n".format(machdep))
+ lines = replace_line(lines, "^MACHDEP = .*", f"MACHDEP = {machdep}\n")
if add_main_stub:
- check_path_exists("fc_stubs.c")
- from shutil import copyfile
- copyfile(sharedir / "analysis-scripts" / "fc_stubs.c", "fc_stubs.c")
+ lines = insert_line_after(lines, "^main.parse: \\\\", f" fc_stubs.c \\\n")
+ check_path_exists(fc_stubs_c)
+ shutil.copyfile(sharedir / "analysis-scripts" / "fc_stubs.c", fc_stubs_c)
lines = insert_line_after(lines, "^FCFLAGS", " -main eva_main \\\n")
- print("Created stub for main function: fc_stubs.c")
+ print(f"Created stub for main function: {dir / 'fc_stubs.c'}")
+ lines = replace_line(lines, "^main.parse: \\\\", f"{main}.parse: \\\n")
+ lines = replace_line(lines, "^TARGETS = main.eva", f"TARGETS = {main}.eva\n")
+ lines = replace_line(lines, "^ main.c \\\\", sources_list_for_makefile(source_list) + "\n")
+ if json_compilation_database:
+ lines = insert_line_after(lines, "^FCFLAGS", f" -json-compilation-database {json_compilation_database} \\\n")
+ if relprefix != "..":
+ lines = replace_line(lines, "^ -add-symbolic-path=.:.. \\\\", f" -add-symbolic-path=.:{relprefix} \\\n", all_occurrences=True)
gnumakefile.write_text("".join(lines))
-print("Template created: " + gnumakefile.name)
+print(f"Template created: {gnumakefile}")
+
+if not framac_in_path:
+ print(f"Frama-C not in path, adding path.mk to {dir}")
+ frama_c_script = bindir / "frama-c-script"
+ os.system(f"{frama_c_script} make-path {dir}")
if "PTESTS_TESTING" in os.environ:
print("Running ptests: cleaning up after tests...")
jcdb.unlink()
- if add_main_stub:
- Path("fc_stubs.c").unlink()
+ fc_stubs_c.unlink()
+ # gnumakefile is not erased because we want it as an oracle
diff --git a/share/analysis-scripts/prologue.mk b/share/analysis-scripts/prologue.mk
new file mode 100644
index 0000000000000000000000000000000000000000..f1cca3d38888a266e2f049084e8aa4a227af99fa
--- /dev/null
+++ b/share/analysis-scripts/prologue.mk
@@ -0,0 +1,43 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# 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). #
+# #
+##########################################################################
+
+# Makefile template prologue for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+# Note: this variable must be defined before including any files
+makefile_dir := $(dir $(lastword $(MAKEFILE_LIST)))
+
+## Useful definitions (to be overridden later if needed)
+
+# Improves analysis time, at the cost of extra memory usage
+export FRAMA_C_MEMORY_FOOTPRINT = 8
+
+# FRAMAC is defined in path.mk when it is included, so the
+# line below will be safely ignored if this is the case.
+# Otherwise, the user may supply it to indicate which Frama-C binary to use.
+FRAMAC ?= frama-c
+
+# analysis.mk contains the main rules and targets
+include $(makefile_dir)/analysis.mk
+
+# Default target
+all: eva
diff --git a/share/analysis-scripts/summary.py b/share/analysis-scripts/summary.py
index a23c34e73ac9d5960d75d0140ee09f355e6f3d8d..6c0e9790e457e66562005c1ee7e75fc8ddb43b41 100755
--- a/share/analysis-scripts/summary.py
+++ b/share/analysis-scripts/summary.py
@@ -38,21 +38,36 @@ import benchmark_database
class OperationException(Exception):
pass
-def build_env(framac):
+def build_make_environment(framac):
if framac is None:
- return { **os.environ }
+ env = { **os.environ }
+ args = []
else:
- bindir = framac + '/build/bin'
- return { **os.environ, 'PATH' : bindir + ':' + os.environ['PATH'] }
-
-def list_targets():
- env = build_env(framac)
+ env = { **os.environ, 'PATH' : f"{framac}/bin:{os.environ['PATH']}" }
+ args = [
+ f"FRAMAC_DIR={framac}/bin",
+ f"FRAMAC={framac}/bin/frama-c"
+ ]
+ return env, args
+
+def list_targets(dir):
+ if not os.path.isdir(dir):
+ raise OperationException(f"target is not a directory: {dir}")
+
+ env, args = build_make_environment(framac)
res = subprocess.run(
- ["make", "--quiet", "display-targets"],
+ ["make", "--directory", dir, "--quiet", "display-targets"] + args,
env=env,
stdout=subprocess.PIPE,
encoding='ascii')
- return res.stdout.split()
+ targets = res.stdout.split()
+ res = []
+ for target in targets:
+ if target.endswith(".eva") or target.endswith(".parse"):
+ res += [f"{dir}/{target}"]
+ else:
+ res += list_targets(target)
+ return res
def clone_frama_c(clonedir, hash):
print("Cloning Frama-C", hash, "...")
@@ -63,21 +78,16 @@ def clone_frama_c(clonedir, hash):
if res.returncode != 0:
raise OperationException("Cannot clone repository. Try to manually"
"remove the broken clone in " + clonedir)
- return res.stdout.strip()
+ return res.stdout.strip() + '/build'
def run_make(framac, benchmark_tag=None):
args = ['make', '--keep-going', 'all']
- env = build_env(framac)
- if not framac is None:
- bindir = framac + '/build/bin'
- args += [
- 'FRAMAC_DIR=' + bindir,
- 'FRAMAC=' + bindir + '/frama-c']
+ env, var_args = build_make_environment(framac)
if benchmark_tag is None:
- args += ['-j', '8']
+ args += ['-j', str(os.cpu_count ())]
else:
args += ['BENCHMARK=' + benchmark_tag]
- return subprocess.Popen(args, env=env,
+ return subprocess.Popen(args + var_args, env=env,
stdout=subprocess.DEVNULL,
stderr=subprocess.PIPE,
preexec_fn=os.setsid)
@@ -95,8 +105,10 @@ def terminate_process(process):
return errors
def smart_rename(target):
+ target = re.sub('^\./', '', target)
target = re.sub('main\.eva$', '', target)
target = re.sub('\.eva$', '', target)
+ target = re.sub('\.frama-c/', '', target)
target = re.sub('qds/frama-c', 'qds', target)
return target
@@ -118,7 +130,7 @@ def poll_results(targets, benchmark_tag):
def run_analyses(display, database, framac, benchmark_tag):
results = []
- targets = list_targets()
+ targets = list_targets(".")
process = run_make(framac, benchmark_tag)
errors = b""
next_poll = time.time()
@@ -188,7 +200,7 @@ try:
gitdir = clonedir + "/frama-c.git"
framac = clone_frama_c(clonedir, args.rev)
else:
- framac = args.repository_path
+ framac = os.path.abspath(args.repository_path)
gitdir = framac
if args.benchmark:
diff --git a/share/analysis-scripts/summary.sh b/share/analysis-scripts/summary.sh
deleted file mode 100755
index 26c4678d98df70eda29f8729f28f2b22cc31b7e5..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/summary.sh
+++ /dev/null
@@ -1,155 +0,0 @@
-#!/bin/bash -u
-
-declare -A stats
-
-function pretty_size()
-{
- ([[ $# -lt 1 ]] || ! [[ $1 =~ ^[0-9]+$ ]]) && return
- KB=$1
- [ $KB -lt 4096 ] && echo ${KB} kiB && return
- MB=$(((KB+512)/1024))
- [ $MB -lt 4096 ] && echo ${MB} MiB && return
- GB=$(((MB+512)/1024))
- echo $GB GiB
-}
-
-function pretty_coverage()
-{
- if [[ $# -gt 1 ]] && [ -n '$1' -a $2 -ne 0 ]
- then
- echo $(bc <<<"scale=1; 100 * $2 / $1")%
- fi
-}
-
-function print_results()
-{
- local t
- local format
-
- format="%20s %10s %10s %10s %10s %10s\n"
-
- if [ -z "$quiet" ]
- then
- echo -e '\e\0143'
- printf "$format" 'target' 'coverage' 'alarms' 'warnings' 'time' 'memory'
- printf "%s\n" " ----------------------------------------------------------------------------"
- for t in $targets
- do
- printf "$format" $t \
- "${stats["$t,coverage"]-}" \
- "${stats["$t,alarms"]-}" \
- "${stats["$t,warnings"]-}" \
- "${stats["$t,user_time"]-}" \
- "${stats["$t,memory"]-}"
- done
- printf "%s\n" " ----------------------------------------------------------------------------"
- printf "$format" 'total' '' "${stats["total_alarms"]-}" "${stats["total_warnings"]-}" "${stats["total_user_time"]-}" ''
- printf "\n"
- fi
-}
-
-function print_csv()
-{
- local t
- local format
-
- format="%s\t%s\t%s\t%s\t%s\t%s\n"
-
- printf "$format" 'target' 'coverage' 'alarms' 'warnings' 'time' 'memory'
- for t in $targets
- do
- printf "$format" $t \
- "${stats["$t,coverage"]-}" \
- "${stats["$t,alarms"]-}" \
- "${stats["$t,warnings"]-}" \
- "${stats["$t,user_time"]-}" \
- "${stats["$t,memory"]-}"
- done
-}
-
-function poll_results()
-{
- stats["total_alarms"]=0
- stats["total_warnings"]=0
- stats["total_user_time"]=0
-
- for t in $targets
- do
- if [ -f "$t/stats.txt" ]
- then
- read stats["$t,syn_reach"] stats["$t,sem_reach"] \
- stats["$t,alarms"] stats["$t,warnings"] \
- stats["$t,user_time"] stats["$t,mem_bytes"] <<< $(
- source $t/stats.txt
- echo ${syn_reach_stmt:-0} ${sem_reach_stmt:-0} \
- ${alarms:-x} ${warnings:-x} \
- ${user_time:-x} ${memory:-'x'}
- )
- stats["$t,coverage"]=$(pretty_coverage ${stats["$t,syn_reach"]} ${stats["$t,sem_reach"]})
- stats["$t,memory"]=$(pretty_size ${stats["$t,mem_bytes"]})
- stats["total_alarms"]=$(bc <<<"${stats["total_alarms"]} + ${stats["$t,alarms"]-0}")
- stats["total_warnings"]=$(bc <<<"${stats["total_warnings"]} + ${stats["$t,warnings"]-0}")
- stats["total_user_time"]=$(bc <<<"${stats["total_user_time"]} + ${stats["$t,user_time"]-0}")
- fi
- done
-}
-
-
-# Parse command Line
-
-run="make"
-targets=""
-quiet=""
-
-while [[ $# > 0 ]]
-do
- case $1 in
- -f|--file|--makefile)
- run="$run $1 $2"
- shift
- ;;
-
- -B|--always-make)
- run="$run $1"
- ;;
-
- -q|--quiet)
- quiet="yes"
- ;;
-
- *)
- targets="$targets $1"
- ;;
- esac
- shift
-done
-
-
-# List make targets
-
-for t in $targets
-do
- run="$run $t"
-done
-
-
-# Run and display
-
-{
- $run > /dev/null &
- pid=$!
-
- poll_results
- print_results
-
- while ps -p $pid >/dev/null
- do
- sleep 1
- poll_results
- print_results
- done
-} 2> summary.log
-
-cat summary.log >&2
-rm -f summary.log
-print_csv > summary.csv
diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk
index 7cf5bcb29e186a6a7b80a0a261094e0915c77bb4..114d2cd6f80d6b624ece1a7f0478979eeac81036 100644
--- a/share/analysis-scripts/template.mk
+++ b/share/analysis-scripts/template.mk
@@ -1,70 +1,43 @@
-# TEMPLATE FOR MAKEFILE TO USE IN FRAMA-C/EVA CASE STUDIES
-
-# DO NOT EDIT THE LINES BETWEEN THE '#'S
-
-###############################################################################
-# Improves analysis time, at the cost of extra memory usage
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-#
-# frama-c-path.mk contains variables which are specific to each
-# user and should not be versioned, such as the path to the
-# frama-c binaries (e.g. FRAMAC and FRAMAC_GUI).
-# It is an optional include, unnecessary if frama-c is in the PATH
--include frama-c-path.mk
-#
-# FRAMAC is defined in frama-c-path.mk when it is included, so the
-# line below will be safely ignored if this is the case
-FRAMAC ?= frama-c
-#
-# frama-c.mk contains the main rules and targets
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-#
+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+### Prologue. Do not modify this block. #######################################
+-include path.mk # path.mk contains variables specific to each user
+ # (e.g. FRAMAC, FRAMAC_GUI) and should not be versioned. It is
+ # an optional include, unnecessary if frama-c is in the PATH.
+FRAMAC ?= frama-c # FRAMAC is defined in path.mk when it is included, but the
+ # user can override it in the command-line.
+include $(shell $(FRAMAC)-config -scripts)/prologue.mk
###############################################################################
-# EDIT VARIABLES AND TARGETS BELOW AS NEEDED
-# The flags below are only suggestions to use with Eva, and can be removed
+# Edit below as needed. Suggested flags are optional.
-# (Optional) preprocessing flags, usually handled by -json-compilation-database
-CPPFLAGS +=
+MACHDEP = x86_32
-# (Optional) Frama-C general flags (parsing and kernel)
+## Preprocessing flags (for -cpp-extra-args)
+CPPFLAGS += \
+
+## General flags
FCFLAGS += \
+ -add-symbolic-path=.:.. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-# (Optional) Eva-specific flags
+## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
-# (MANDATORY) Name of the main target
-MAIN_TARGET :=
-
-# Remove these lines after defining the main target
-ifeq ($(MAIN_TARGET),)
-$(error MAIN_TARGET not defined in $(firstword $(MAKEFILE_LIST)))
-endif
+## GUI-only flags
+FCGUIFLAGS += \
+ -add-symbolic-path=.:.. \
-# Add other targets if needed
-TARGETS = $(MAIN_TARGET).eva
+## Analysis targets (suffixed with .eva)
+TARGETS = main.eva
-# Default target
-all: $(TARGETS)
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+main.parse: \
+ main.c \
-# (MANDATORY) List of source files used by MAIN_TARGET.
-# If there is a JSON compilation database,
-# 'frama-c-script list-files' can help obtain it
-$(MAIN_TARGET).parse:
-
-
-# The following targets are optional and provided for convenience only
-parse: $(TARGETS:%.eva=%.parse)
-loop: $(TARGETS:%.eva=%.parse.loop) $(TARGETS:%=%.loop)
-gui: $(MAIN_TARGET).eva.gui
-
-# Run 'make <TARGET>.eva.loop' to obtain a .loop file, fine-tune it by hand,
-# then rename it to <TARGET>.slevel to prevent it from being overwritten.
-# If such file exists, use it to define per-function slevel values.
-ifneq (,$(wildcard $(MAIN_TARGET).slevel))
-$(MAIN_TARGET).eva: \
- EVAFLAGS += $(shell cat $(MAIN_TARGET).slevel | tr -d '\n\\')
-endif
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+###############################################################################
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index 74219d5a7189f16ec2c67693fda369b891036493..d3e15e1b85ec9976597846dcbf9b4be241b9e69b 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -1,6 +1,6 @@
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
- EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= bin/frama-c-script make-template @PTEST_DIR@/result < @PTEST_DIR@/make_template.input > @PTEST_DIR@/result/make_template.res 2> @PTEST_DIR@/result/make_template.err
+ EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err cd @PTEST_DIR@ && PTESTS_TESTING= ../../bin/frama-c-script make-template result < make_template.input > result/make_template.res 2> result/make_template.err
EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 bin/frama-c-script flamegraph @PTEST_DIR@/flamegraph.txt @PTEST_DIR@/result > @PTEST_DIR@/result/flamegraph.res 2> @PTEST_DIR@/result/flamegraph.err && rm -f @PTEST_DIR@/result/flamegraph.svg
EXECNOW: LOG find_fun1.res LOG find_fun1.err bin/frama-c-script find-fun main2 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun1.res 2> @PTEST_DIR@/result/find_fun1.err
diff --git a/tests/fc_script/make_template.input b/tests/fc_script/make_template.input
index 62488cfcb339f48b9263e611e5e7422074143ddb..6963df94935110ccdf0218b25973e3348c9e1947 100644
--- a/tests/fc_script/make_template.input
+++ b/tests/fc_script/make_template.input
@@ -1,7 +1,10 @@
+y
fc_script_main
-file1.c file*.c dir/more_files.c
+for-find*.c main*.c
+y
y
y
invalid_machdep
n
x86_64
+y
diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile
index 44f773a61a3c01b2d46d6407f2cda92926b65d7d..5b9a464e26fd809740a93a417ee458e204eb115c 100644
--- a/tests/fc_script/oracle/GNUmakefile
+++ b/tests/fc_script/oracle/GNUmakefile
@@ -1,68 +1,50 @@
-# TEMPLATE FOR MAKEFILE TO USE IN FRAMA-C/EVA CASE STUDIES
-
-# DO NOT EDIT THE LINES BETWEEN THE '#'S
-
-###############################################################################
-# Improves analysis time, at the cost of extra memory usage
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-#
-# frama-c-path.mk contains variables which are specific to each
-# user and should not be versioned, such as the path to the
-# frama-c binaries (e.g. FRAMAC and FRAMAC_GUI).
-# It is an optional include, unnecessary if frama-c is in the PATH
--include frama-c-path.mk
-#
-# FRAMAC is defined in frama-c-path.mk when it is included, so the
-# line below will be safely ignored if this is the case
-FRAMAC ?= frama-c
-#
-# frama-c.mk contains the main rules and targets
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-#
+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+### Prologue. Do not modify this block. #######################################
+-include path.mk # path.mk contains variables specific to each user
+ # (e.g. FRAMAC, FRAMAC_GUI) and should not be versioned. It is
+ # an optional include, unnecessary if frama-c is in the PATH.
+FRAMAC ?= frama-c # FRAMAC is defined in path.mk when it is included, but the
+ # user can override it in the command-line.
+include $(shell $(FRAMAC)-config -scripts)/prologue.mk
###############################################################################
-# EDIT VARIABLES AND TARGETS BELOW AS NEEDED
-# The flags below are only suggestions to use with Eva, and can be removed
+# Edit below as needed. Suggested flags are optional.
+
+MACHDEP = x86_64
-# (Optional) preprocessing flags, usually handled by -json-compilation-database
-CPPFLAGS +=
+## Preprocessing flags (for -cpp-extra-args)
+CPPFLAGS += \
-# (Optional) Frama-C general flags (parsing and kernel)
+## General flags
FCFLAGS += \
+ -json-compilation-database ../compile_commands.json \
-main eva_main \
- -machdep x86_64 \
- -json-compilation-database . \
+ -add-symbolic-path=.:.. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-# (Optional) Eva-specific flags
+## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
-# (MANDATORY) Name of the main target
-MAIN_TARGET := fc_script_main
+## GUI-only flags
+FCGUIFLAGS += \
+ -add-symbolic-path=.:.. \
-# Add other targets if needed
-TARGETS = $(MAIN_TARGET).eva
+## Analysis targets (suffixed with .eva)
+TARGETS = fc_script_main.eva
-# Default target
-all: $(TARGETS)
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+fc_script_main.parse: \
+ fc_stubs.c \
+ ../for-find-fun.c \
+ ../for-find-fun2.c \
+ ../main.c \
+ ../main2.c \
+ ../main3.c \
-# (MANDATORY) List of source files used by MAIN_TARGET.
-# If there is a JSON compilation database,
-# 'frama-c-script list-files' can help obtain it
-$(MAIN_TARGET).parse: fc_stubs.c file1.c file*.c dir/more_files.c
-
-
-# The following targets are optional and provided for convenience only
-parse: $(TARGETS:%.eva=%.parse)
-loop: $(TARGETS:%.eva=%.parse.loop) $(TARGETS:%=%.loop)
-gui: $(MAIN_TARGET).eva.gui
-
-# Run 'make <TARGET>.eva.loop' to obtain a .loop file, fine-tune it by hand,
-# then rename it to <TARGET>.slevel to prevent it from being overwritten.
-# If such file exists, use it to define per-function slevel values.
-ifneq (,$(wildcard $(MAIN_TARGET).slevel))
-$(MAIN_TARGET).eva: \
- EVAFLAGS += $(shell cat $(MAIN_TARGET).slevel | tr -d '\n\\')
-endif
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+###############################################################################
diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res
index 9f38d9c7e745cbea6fe458c9fc77cdcd03f48e1e..8d4a89eefce975172999f89a7e9917cb87545087 100644
--- a/tests/fc_script/oracle/make_template.res
+++ b/tests/fc_script/oracle/make_template.res
@@ -1,6 +1,17 @@
+Preparing template: result/GNUmakefile
Running ptests: setting up mock files...
-Main target name: Source files separated by spaces (default if empty: *.c): 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.
+warning: result/GNUmakefile already exists. Overwrite? [y/N] Main target name: Source files (default: **/*.c): The following sources were matched (relative to result):
+ ../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_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: Created stub for main function: fc_stubs.c
-Template created: GNUmakefile
+Please enter the machdep [x86_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: warning: result/fc_stubs.c already exists. Overwrite? [y/N] Wrote to: result/path.mk
+Created stub for main function: result/fc_stubs.c
+Template created: result/GNUmakefile
+Frama-C not in path, adding path.mk to result
Running ptests: cleaning up after tests...