...
 
Commits (25)
......@@ -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 \
......@@ -1575,10 +1577,6 @@ STDLIB_FILES:=\
weak \
ephemeron
ifeq ($(HAS_OCAML407),no)
STDLIB_FILES+=pervasives
endif
STDLIB_FILES:=$(patsubst %,$(OCAMLLIB)/%.mli,$(STDLIB_FILES))
.PHONY: doc-kernel
......@@ -1938,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 \
......
......@@ -126,56 +126,12 @@ endif
GENERATED+= src/libraries/utils/json.ml src/libraries/stdlib/transitioning.ml
ifeq ($(HAS_OCAML408),yes)
DYNLINK_INIT=fun () -> ()
FORMAT_STAG=stag
FORMAT_STRING_OF_STAG=match s with \
Format.String_tag str -> str \
| _ -> raise (Invalid_argument "unsupported tag extension")
FORMAT_STAG_OF_STRING=Format.String_tag s
FORMAT_PP_OPT=Format.pp_print_option
HAS_OCAML407_OR_408=yes
else
DYNLINK_INIT=Dynlink.init
FORMAT_STAG=tag
FORMAT_STRING_OF_STAG=s
FORMAT_STAG_OF_STRING=s
ifeq ($(HAS_OCAML407),yes)
HAS_OCAML407_OR_408=yes
else
HAS_OCAML407_OR_408=no
endif
FORMAT_PP_OPT=fun ?(none=(fun _ () -> ())) pp fmt o -> \
match o with \
| None -> none fmt () \
| Some v -> pp fmt v
endif
ifeq ($(HAS_OCAML407_OR_408),yes)
FLOAT_MAX_FLOAT=Float.max_float
else
FLOAT_MAX_FLOAT=Pervasives.max_float
endif
src/libraries/stdlib/transitioning.ml: \
src/libraries/stdlib/transitioning.ml.in \
Makefile.generating share/Makefile.config
$(PRINT_MAKING) $@
rm -f $@
sed \
-e 's/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g' \
-e 's/@STACK_FOLD@/$(STACK_FOLD)/g' \
-e 's/@NTH_OPT@/$(NTH_OPT)/g' \
-e 's/@FIND_OPT@/$(FIND_OPT)/g' \
-e 's/@ASSOC_OPT@/$(ASSOC_OPT)/g' \
-e 's/@ASSQ_OPT@/$(ASSQ_OPT)/g' \
-e 's/@DYNLINK_INIT@/$(DYNLINK_INIT)/g' \
-e 's/@FLOAT_MAX_FLOAT@/$(FLOAT_MAX_FLOAT)/g' \
-e 's/@FORMAT_STAG@/$(FORMAT_STAG)/g' \
-e 's/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g' \
-e 's/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g' \
-e 's/@FORMAT_PP_OPT@/$(FORMAT_PP_OPT)/g' \
$< > $@
cat $< > $@
$(CHMOD_RO) $@
##################
......
......@@ -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;
......
......@@ -108,8 +108,8 @@ AC_MSG_CHECKING(version of OCaml)
OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
AC_MSG_RESULT($OCAMLVERSION)
case $OCAMLVERSION in
0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.*|4.03.*|4.04.*)
AC_MSG_ERROR(Incompatible OCaml version; use 4.05+.);;
0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.*|4.03.*|4.04.*|4.05.*|4.06.*|4.07.*|4.08.0)
AC_MSG_ERROR(Incompatible OCaml version; use 4.08.1+.);;
*)
OCAML_ANNOT_OPTION="-bin-annot";;
esac
......@@ -118,24 +118,24 @@ AC_SUBST(OCAMLMAJORNB)
AC_SUBST(OCAMLMINORNB)
AC_SUBST(OCAMLPATCHNB)
AC_SUBST(HAS_OCAML407)
AC_SUBST(HAS_OCAML408)
AC_SUBST(HAS_OCAML409)
AC_SUBST(HAS_OCAML410)
OCAMLMAJORNB=$(echo $OCAMLVERSION | cut -f 1 -d .)
OCAMLMINORNB=$(echo $OCAMLVERSION | cut -f 2 -d .)
OCAMLPATCHNB=$(echo $OCAMLVERSION | cut -f 3 -d .)
if test $OCAMLMAJORNB -gt 4; then
HAS_OCAML407=yes;
HAS_OCAML408=yes;
HAS_OCAML409=yes;
HAS_OCAML410=yes;
else
HAS_OCAML407=no;
HAS_OCAML408=no;
if test $OCAMLMINORNB -ge 7; then
HAS_OCAML407=yes;
HAS_OCAML409=no;
HAS_OCAML410=no;
if test $OCAMLMINORNB -ge 9; then
HAS_OCAML409=yes;
fi;
if test $OCAMLMINORNB -ge 8; then
HAS_OCAML408=yes;
if test $OCAMLMINORNB -ge 10; then
HAS_OCAML410=yes;
fi;
fi; # MAJORNB -gt 4
......@@ -300,10 +300,14 @@ AC_MSG_CHECKING(for zarith)
ZARITH=$($OCAMLFIND query zarith -format %v)
if test -z "$ZARITH" ; then
AC_MSG_ERROR(Cannot find zarith via ocamlfind.)
else
AC_MSG_RESULT(found $ZARITH)
AC_MSG_ERROR(Cannot find zarith via ocamlfind (requires zarith 1.5 or higher).)
fi
case ZARITH in
1.[[01234]].*)
AC_MSG_ERROR(found $ZARITH: requires 1.5 or higher.);;
*)
AC_MSG_RESULT(found $ZARITH);;
esac
# yojson
########
......@@ -839,7 +843,7 @@ AC_ARG_ENABLE(external,
])
AC_FOREACH([__plugin],m4_esyscmd([ls src/plugins]),
[ m4_if(m4_regexp(KNOWN_SRC_DIRS,`\<__plugin\>'),[-1],
[ m4_if(m4_bregexp(KNOWN_SRC_DIRS,`\<__plugin\>'),[-1],
[
m4_define([plugin_dir],[src/plugins/__plugin])
m4_syscmd(test -r plugin_dir/configure.in)
......
......@@ -1236,8 +1236,8 @@ and user-friendly way.
As a general rule, you should \emph{never} write to standard output
and error channels through \ocaml standard libraries. For instance,
you should never use \texttt{Pervasives.stdout} and
\texttt{Pervasives.stderr} channels, nor \texttt{Format.printf}-like
you should never use \texttt{Stdlib.stdout} and
\texttt{Stdlib.stderr} channels, nor \texttt{Format.printf}-like
routines.
Instead, you should use \texttt{Format.fprintf} to implement
......@@ -1616,7 +1616,7 @@ allows you to create such channels for your own purposes.
Basically, \emph{channels} ensure that no message emission interfere
with each others during echo on standard output. Hence the forbidden
direct access to \lstinline{Pervasives.stdout}. However,
direct access to \lstinline{Stdlib.stdout}. However,
\lstinline{Log} interface allows you to create such channels on your
own, in addition to the one automatically created for your plug-in.
......@@ -1666,7 +1666,7 @@ another channel:
\end{description}
It is also possible to have a momentary direct access to
\lstinline{Pervasives.stdout}, or whatever its redirection is:
\lstinline{Stdlib.stdout}, or whatever its redirection is:
\begin{description}
%%item
\logroutine{print\_on\_output}{ "..."}%
......@@ -1844,7 +1844,7 @@ module AB =
(Structural_desr.Sum [| [| Structural_descr.p_int |] |])
(* equality, compare and hash are the standard OCaml ones *)
let equal (x:t) y = x = y
let compare (x:t) y = Pervasives.compare x y
let compare (x:t) y = Stdlib.compare x y
let hash (x:t) = Hashtbl.hash x
(* the type ab is a standard functional type, thus copying and rehashing
are simply identity. Rehashing is used when marshaling. *)
......@@ -1968,7 +1968,7 @@ module Poly_ab =
| A _, B _ | B _, A _ -> false
let mk_compare f x y = match x, y with
| A x, A y -> f x y
| B x, B y -> Pervasives.compare x y
| B x, B y -> Stdlib.compare x y
| A _, B _ -> 1
| B _, A _ -> -1
let mk_hash f = function A x -> f x | B x -> 257 * x
......
......@@ -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
......
......@@ -14,7 +14,7 @@ import './style.css';
import { LabView, View, Group } from 'frama-c/LabViews';
import Dive from 'frama-c/dive/Dive';
import { GridItem } from 'dome/layout/grids';
import { GridHbox, GridItem } from 'dome/layout/grids';
import * as Controller from './Controller';
import ASTview from './ASTview';
......@@ -59,11 +59,11 @@ const HistorySelectionControls = () => {
export default (() => {
const [sidebar, flipSidebar] = Dome.useSwitch(
'frama-c.sidebar.unfold',
false,
true,
);
const [viewbar, flipViewbar] = Dome.useSwitch(
'frama-c.viewbar.unfold',
false,
true,
);
return (
......@@ -94,9 +94,27 @@ export default (() => {
customize={viewbar}
settings="frama-c.labview"
>
<View id="dashboard" label="Dashboard" defaultView>
<View id="console" label="Console" defaultView>
<GridItem id="frama-c.console" />
</View>
<View id="values" label="Values">
<GridHbox>
<GridItem id="frama-c.astview" />
<GridItem id="frama-c.values" />
</GridHbox>
<GridItem id="frama-c.properties" />
</View>
<View id="dive" label="Dive">
<GridHbox>
<GridItem id="frama-c.astview" />
<GridItem id="dive.graph" />
<GridItem id="frama-c.locations" />
</GridHbox>
<GridHbox>
<GridItem id="frama-c.properties" />
<GridItem id="frama-c.console" />
</GridHbox>
</View>
<Group id="frama-c" label="Frama-C" title="Frama-C Kernel Components">
<Controller.Console />
<Properties />
......
......@@ -85,8 +85,8 @@ OCAMLMAJORNB ?=@OCAMLMAJORNB@
OCAMLMINORNB ?=@OCAMLMINORNB@
OCAMLPATCHNB ?=@OCAMLPATCHNB@
HAS_OCAML407 ?=@HAS_OCAML407@
HAS_OCAML408 ?=@HAS_OCAML408@
HAS_OCAML409 ?=@HAS_OCAML409@
HAS_OCAML410 ?=@HAS_OCAML410@
PLATFORM ?=@PLATFORM@
OCAMLWIN32 ?=@OCAMLWIN32@
......
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".
......@@ -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 &
......
##########################################################################
# #
# 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))"
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 $<
-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
# 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
#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
# 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
......@@ -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 == []:
......
#!/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
This diff is collapsed.
##########################################################################
# #
# 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
......@@ -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:
......
#!/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
# 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
###############################################################################
......@@ -432,7 +432,7 @@ module Bool = struct
type t = Top | True | False | Bottom
let hash (b : t) = Hashtbl.hash b
let equal (b1 : t) (b2 : t) = b1 = b2
let compare (b1 : t) (b2 : t) = Transitioning.Stdlib.compare b1 b2
let compare (b1 : t) (b2 : t) = Stdlib.compare b1 b2
let pretty fmt = function
| Top -> Format.fprintf fmt "Top"
| True -> Format.fprintf fmt "True"
......
......@@ -172,7 +172,7 @@ module Make (F: Float_sig.S) = struct
let compare x y =
match x, y with
| FRange.Itv (b1, e1, n1), FRange.Itv (b2, e2, n2) ->
let c = Transitioning.Stdlib.compare n1 n2 in
let c = Stdlib.compare n1 n2 in