diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3394befbc709bec2d77dbc1603508d8c0e8f786e..87d65d5591a26341fecf9f5c8e2e77512a365b82 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -64,6 +64,13 @@ genassigns:
tags:
- nix
+frama-clang:
+ stage: tests
+ script:
+ - nix/frama-ci.sh build -A frama-clang.tests
+ tags:
+ - nix
+
counter-examples:
stage: tests
script:
diff --git a/Makefile b/Makefile
index 7dd57fbf16620ad4344ab825ae8e30793e42e470..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 \
@@ -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 \
diff --git a/Makefile.generating b/Makefile.generating
index 2e1c0c6c5dfc5b3bdb9ca7fc003397c3255386d3..e55a39ff38ce2e325850aa68aff2c11074ca1a24 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -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) $@
##################
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/configure.in b/configure.in
index 364940906cb9c955115ee9d81cca18b36168df30..3f792af4a5f4938a604d93d181bcb4807ebd9999 100644
--- a/configure.in
+++ b/configure.in
@@ -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)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 54d485f04fa5143478f29a72319ce5a5c1bd7c66..1be1e161e81026b4b4d255c1605fdd11f083defa 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -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
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/ivette/src/frama-c/dive/Dive.tsx b/ivette/src/frama-c/dive/Dive.tsx
index d66a1749b030d17596937718db2ad4ef3a5488aa..c0480f5b4b54d3bf747390caaceb846ed712fb3b 100644
--- a/ivette/src/frama-c/dive/Dive.tsx
+++ b/ivette/src/frama-c/dive/Dive.tsx
@@ -42,12 +42,12 @@ function callstackToString(callstack: API.callstack): string {
function buildCxtMenu(
commands: Cxtcommand[],
- content? : JSX.Element,
- action? : () => void,
+ content?: JSX.Element,
+ action?: () => void,
) {
commands.push({
content: content ? renderToString(content) : '',
- select: action || (() => {}),
+ select: action || (() => { }),
enabled: !!action,
});
}
@@ -226,8 +226,7 @@ class Dive {
receiveGraph(data: any): Cytoscape.CollectionReturnValue {
let newNodes = this.cy.collection();
- for (const node of data.nodes)
- {
+ for (const node of data.nodes) {
if (typeof node.range === 'number')
node.stops = `0% ${node.range}% ${node.range}% 100%`;
@@ -271,8 +270,7 @@ class Dive {
}
}
- for (const dep of data.deps)
- {
+ for (const dep of data.deps) {
const src = this.cy.$id(dep.src);
const dst = this.cy.$id(dep.dst);
const isRoot = dst?.data('is_root');
@@ -308,7 +306,7 @@ class Dive {
set layout(layout: string) {
let extendedOptions = {};
if (layout in layouts)
- extendedOptions = (layouts as {[key: string]: object})[layout];
+ extendedOptions = (layouts as { [key: string]: object })[layout];
this._layout = layout;
this.layoutOptions = {
name: layout,
@@ -323,7 +321,7 @@ class Dive {
recomputeLayout(newNodes?: Cytoscape.Collection): void {
if (this.layoutOptions && this.cy.container() &&
- (newNodes === undefined || !newNodes.empty())) {
+ (newNodes === undefined || !newNodes.empty())) {
this.cy.layout({
animationEasing: 'ease-in-out-quad',
/* Do not move new nodes */
@@ -438,8 +436,11 @@ class Dive {
node.unselectify();
}
- selectLocation(location: States.Location, doExplore: boolean) {
- if (location !== this.selectedLocation) {
+ selectLocation(location: States.Location | undefined, doExplore: boolean) {
+ if (!location) {
+ // Reset whole graph if no location is selected.
+ this.clear();
+ } else if (location !== this.selectedLocation) {
this.selectedLocation = location;
const selectNode = this.cy.$('node:selected');
const writes = selectNode?.data()?.writes;
@@ -475,7 +476,7 @@ const GraphView = () => {
const [selection, updateSelection] = States.useSelection();
const [lock, flipLock] = Dome.useSwitch('dive.lock', false);
const [selectionMode, flipSelectionMode] =
- Dome.useGlobalSetting('dive.selectionMode', 'follow');
+ Dome.useGlobalSetting('dive.selectionMode', 'follow');
function setCy(cy: Cytoscape.Core) {
if (cy !== dive.cy)
@@ -503,8 +504,7 @@ const GraphView = () => {
};
// Updates the graph according to the selected marker.
- if (selection?.current)
- dive.selectLocation(selection?.current, !lock);
+ dive.selectLocation(selection?.current, !lock);
}, [dive, lock, selection, updateSelection]);
// Layout selection
@@ -523,14 +523,14 @@ const GraphView = () => {
// Selection mode
const selectMode = (id?: boolean) => id && flipSelectionMode(id);
- const modes =
- [{ id: 'follow', label: 'Follow selection' },
- { id: 'add', label: 'Add selection to the graph' },
- ];
+ const modes = [
+ { id: 'follow', label: 'Follow selection' },
+ { id: 'add', label: 'Add selection to the graph' },
+ ];
const checkMode =
- (item: { id: string }) => (
- { checked: item.id === selectionMode, ...item }
- );
+ (item: { id: string }) => (
+ { checked: item.id === selectionMode, ...item }
+ );
const modeMenu = () => {
Dome.popupMenu(modes.map(checkMode), selectMode);
};
@@ -583,7 +583,7 @@ export default () => (
id="dive.graph"
label="Data-flow graph"
title={'Data dependency graph according to an Eva analysis.\nNodes color ' +
- 'represents the precision of the values inferred by Eva.'}
+ 'represents the precision of the values inferred by Eva.'}
>
<GraphView />
</Component>
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index cf01222181acde5a5daef680ecb593f020745107..a3a4bad5ae3e8bed8131be99c3073c65295e1c43 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -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 />
diff --git a/nix/default.nix b/nix/default.nix
index b7804254b581310c919738b827b0dd22a9aa0ba7..fdce398cfe5fadaca673a976eb8bb381dec43ffa 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -218,6 +218,7 @@ rec {
];
counter_examples_src = plugins.counter-examples.src;
genassigns_src = plugins.genassigns.src;
+ frama_clang_src = plugins.frama-clang.src;
pathcrawler_src = plugins.pathcrawler.src;
mthread_src = plugins.mthread.src;
caveat_importer_src = plugins.caveat-importer.src;
@@ -233,6 +234,8 @@ rec {
chmod -R u+w -- "$sourceRoot/src/plugins/counter-examples"
cp -r --preserve=mode "$genassigns_src" "$sourceRoot/src/plugins/genassigns"
chmod -R u+w -- "$sourceRoot/src/plugins/genassigns"
+ cp -r --preserve=mode "$frama_clang_src" "$sourceRoot/src/plugins/frama-clang"
+ chmod -R u+w -- "$sourceRoot/src/plugins/frama-clang"
cp -r --preserve=mode "$pathcrawler_src" "$sourceRoot/src/plugins/pathcrawler"
chmod -R u+w -- "$sourceRoot/src/plugins/pathcrawler"
cp -r --preserve=mode "$mthread_src" "$sourceRoot/src/plugins/mthread"
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
index 067bb0c00611b8250fb16c3f0a34a70a23ed2c86..e093574991eec97d4c896c33edf17c28d543b5cf 100644
--- a/nix/frama-ci.nix
+++ b/nix/frama-ci.nix
@@ -5,7 +5,7 @@ let
src = builtins.fetchGit {
"url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
"name" = "Frama-CI";
- "rev" = "0dad15724fe9fa0782e8797f996d9a996a68ae65";
+ "rev" = "abf07b7c0f53b33b32c8b170580e14480fd3aba6";
"ref" = "master";
};
in
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 653d91fad5e4696a2cb7398993aad983048684d5..0739e3cef9cf47ea569ff43de2d365dc91910a61 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -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@
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..e732240db26edd846b33d9d6d610b25454044b7b 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,14 +113,12 @@ 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 \
-no-deps-print -no-calldeps-print \
-eva-warn-key garbled-mix \
-memexec-all -calldeps -permissive -from-verbose 0 \
- $(SLEVEL) \
$(if $(EVABUILTINS), -eva-builtin=$(call fc_list,$(EVABUILTINS)),) \
$(if $(EVAUSESPECS), -eva-use-spec $(call fc_list,$(EVAUSESPECS)),)
FCFLAGS ?=
@@ -146,7 +141,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 +155,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 $@
@@ -186,7 +180,6 @@ SHELL := /bin/bash
mv $@/{running,command}
touch $@ # Update timestamp and prevents remake if nothing changes
-%.slevel.eva: SLEVEL = -slevel $(word 2,$(subst ., ,$*))
%.eva: EVA = $(FRAMAC) $(FCFLAGS) -eva $(EVAFLAGS)
%.eva: PARSE_RESULT = $(word 1,$(subst ., ,$*)).parse
%.eva: $$(PARSE_RESULT) $$(shell $(DIR)cmd-dep.sh $$@/command $$(EVA)) $(if $(BENCHMARK),.FORCE,)
@@ -226,7 +219,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/cmd-dep.sh b/share/analysis-scripts/cmd-dep.sh
index 61fdaff4b3400bf2afeac287d5cf36b3d0177acf..7dc15d918d3a566489d08ced974d6aa645662ec0 100755
--- a/share/analysis-scripts/cmd-dep.sh
+++ b/share/analysis-scripts/cmd-dep.sh
@@ -18,7 +18,7 @@ STRING=$*
if
[ ! -e $FILE ] ||
- ! (diff --brief --ignore-space-change $FILE - <<< "$STRING")
+ ! (diff --brief --ignore-space-change $FILE - >/dev/null <<< "$STRING")
then
mkdir -p $(dirname "$FILE")
echo $STRING > "$FILE"
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..504043a6ebf62a733e1b9290293b866f0a15463a 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 "PTESTS_TESTING" in os.environ and 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/slevel-tweaker.sh b/share/analysis-scripts/slevel-tweaker.sh
deleted file mode 100755
index f67979a1ebe319e6aed9eb2a7037e74dc115e955..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/slevel-tweaker.sh
+++ /dev/null
@@ -1,118 +0,0 @@
-#!/bin/bash -u
-
-declare -A alarms
-declare -A utimes
-
-
-function print_results()
-{
- local s
- local t
-
- if [ -z "$quiet" ]
- then
- echo -e '\e\0143'
- printf "%24s" 'file / slevel'
- for s in $slevels
- do
- printf "%8s" $s
- done
- printf "\n"
- for t in $targets
- do
- printf "\n"
- printf "%18s%6s" $t '#alrm'
- for s in $slevels
- do
- printf "%8s" ${alarms["$t,$s"]-}
- done
- printf "\n"
- printf "%18s%6s" '' 'time'
- for s in $slevels
- do
- printf "%8s" ${utimes["$t,$s"]-}
- done
- printf "\n"
- done
- printf "\n"
- fi
-}
-
-function poll_results()
-{
- for s in $slevels
- do
- for t in $targets
- do
- base=$t.$s.slevel.eva
- if [ -f $base/stats.txt ]
- then
- read alarms["$t,$s"] utimes["$t,$s"] <<< $(
- source $base/stats.txt
- echo ${alarms:-x} ${user_time:- }
- )
- fi
- done
- done
-}
-
-
-# Parse command Line
-
-slevels="0 10 20 50 100 200 500 1000 2000 5000 10000 20000 50000"
-run="make --jobs 9"
-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 s in $slevels
-do
- for t in $targets
- do
- run="$run $t.$s.slevel.eva"
- done
-done
-
-
-# Run and display
-
-{
- $run > /dev/null &
- pid=$!
-
- print_results
-
- while ps -p $pid >/dev/null
- do
- sleep 1
- poll_results
- print_results
- done
-} 2> slevel-tweaker.log
-
-cat slevel-tweaker.log >&2
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/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index ae489b0b24b78e15ecff98fa17b1f8384b375205..89202b4021e323eb84e96c3951b1246e64149594 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -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"
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index fd063ecc15feda204b32f728b7d5d8c40ce53c11..195d7f285c35cccc2eaf3bd81012fe37ef1ba1f4 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -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
if c <> 0 then c else
let r = F.compare b1 b2 in
if r <> 0 then r else F.compare e1 e2
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 2d1fce1097ab3aadbeddbc72ec6c83e549ba32a2..e3c5c99c8db5ef823e98341d23bceef3eec40262 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -306,8 +306,8 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
if hashed_node == tentative_new_node
then begin
if current_counter = max_int
- then Kernel.fatal "Offsetmap(%s): internal maximum exeeded" V.name;
- counter := Transitioning.Stdlib.succ current_counter;
+ then Kernel.fatal "Offsetmap(%s): internal maximum exceeded" V.name;
+ counter := Stdlib.succ current_counter;
end;
hashed_node
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index a0845e815040b754587d15eca7cf150ba0911b25..5635f1b14691576d2a1c76134895676b7c3dc6c3 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -134,7 +134,7 @@ module D =
let n = Exp.compare e1 e2 in
if n = 0 then Extlib.compare_basic fk1 fk2 else n
| Memory_access(lv1, access_kind1), Memory_access(lv2, access_kind2) ->
- let n = Transitioning.Stdlib.compare access_kind1 access_kind2 in
+ let n = Stdlib.compare access_kind1 access_kind2 in
if n = 0 then Lval.compare lv1 lv2 else n
| Index_out_of_bound(e11, e12), Index_out_of_bound(e21, e22) ->
let n = Exp.compare e11 e21 in
@@ -147,11 +147,11 @@ module D =
let n = Extlib.opt_compare Exp.compare e11 e21 in
if n = 0 then Exp.compare e12 e22 else n
| Overflow(s1, e1, n1, b1), Overflow(s2, e2, n2, b2) ->
- let n = Transitioning.Stdlib.compare s1 s2 in
+ let n = Stdlib.compare s1 s2 in
if n = 0 then
let n = Exp.compare e1 e2 in
if n = 0 then
- let n = Transitioning.Stdlib.compare b1 b2 in
+ let n = Stdlib.compare b1 b2 in
if n = 0 then Integer.compare n1 n2 else n
else
n
@@ -160,7 +160,7 @@ module D =
| Float_to_int(e1, n1, b1), Float_to_int(e2, n2, b2) ->
let n = Exp.compare e1 e2 in
if n = 0 then
- let n = Transitioning.Stdlib.compare b1 b2 in
+ let n = Stdlib.compare b1 b2 in
if n = 0 then Integer.compare n1 n2 else n
else
n
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 7f6f2802239ca20044ef97d8dbd18fd2146d74a1..01dde03fd642e3351dd11f0ddb2a4888dde30020 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -285,7 +285,7 @@ let merge_funspec s1 s2 =
(** {2 Getting annotations} *)
(**************************************************************************)
-module Behavior_set_map = Transitioning.Stdlib.Map.Make(Datatype.String.Set)
+module Behavior_set_map = Stdlib.Map.Make(Datatype.String.Set)
let is_same_behavior_set l1 l2 =
Datatype.String.Set.(equal (of_list l1) (of_list l2))
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index bfa51a66126795e29082521bb02dfbfa96d3fee6..7edb1e01b553e34a9c6e32619d61abfcd8ea779d 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -658,7 +658,7 @@ include Datatype.Make_with_collections
let n = Extlib.opt_compare Kf.compare kf1 kf2 in
if n = 0 then
let n = Kinstr.compare ki1 ki2 in
- if n = 0 then Transitioning.Stdlib.compare ba1 ba2 else n
+ if n = 0 then Stdlib.compare ba1 ba2 else n
else
n
| IPAxiom {il_name=s1}, IPAxiom {il_name=s2}
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index d4209faf3a99aca4c09714fa442d0128d45c42eb..441c1594ac728b5cbb08d757ac1ee7eaea8413fa 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -47,7 +47,7 @@ module Emitted_status =
| True -> "VALID"
| False_if_reachable | False_and_reachable -> "**NOT** VALID"
| Dont_know -> "unknown")
- let compare (s1:t) s2 = Transitioning.Stdlib.compare s1 s2
+ let compare (s1:t) s2 = Stdlib.compare s1 s2
let equal (s1:t) s2 = s1 = s2
let hash (s:t) = Caml_hashtbl.hash s
end)
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index 90a28b89a7125de34b7b761d84e88fc50bf62e6e..9ec29a131e400c08717e0b17458a5f4b5373de2f 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -251,11 +251,11 @@ and pp_raw_stmt fmt = function
pp_block bl1 pp_block bl2 pp_cabsloc loc
| THROW(e,loc) ->
fprintf fmt "@[<hov 2>THROW %a, loc(%a)@]"
- (Transitioning.Format.pp_print_option pp_exp) e pp_cabsloc loc
+ (Format.pp_print_option pp_exp) e pp_cabsloc loc
| TRY_CATCH(s,l,loc) ->
let print_one_catch fmt (v,s) =
fprintf fmt "@[<v 2>@[CATCH %a {@]@;%a@]@;}"
- (Transitioning.Format.pp_print_option pp_single_name) v
+ (Format.pp_print_option pp_single_name) v
pp_stmt s
in
fprintf fmt "@[<v 2>@[TRY %a (loc %a) {@]@;%a@]@;}"
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 47add398d3dbb5684c85af5f42351c50b8090032..6822800afecaf8e3d5e546787baa5fa0545a42bb 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -424,7 +424,7 @@ type order =
| A of Datatype.String.Set.t
let cmp_order a b = match a , b with
- | I a , I b -> Transitioning.Stdlib.compare a b
+ | I a , I b -> Stdlib.compare a b
| I _ , _ -> (-1)
| _ , I _ -> 1
| S a , S b -> String.compare a b
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 36c2d644f4678075e8515401b601ed91b3ef308c..e3437fa40dd4b9f93bed8c05a3826b3266070abe 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1639,7 +1639,7 @@ and compare_toffset off1 off2 =
and compare_logic_label l1 l2 = match l1, l2 with
| StmtLabel s1 , StmtLabel s2 -> Stmt.compare !s1 !s2
| FormalLabel s1, FormalLabel s2 -> String.compare s1 s2
- | BuiltinLabel l1, BuiltinLabel l2 -> Transitioning.Stdlib.compare l1 l2
+ | BuiltinLabel l1, BuiltinLabel l2 -> Stdlib.compare l1 l2
| (StmtLabel _ | FormalLabel _), (FormalLabel _ | BuiltinLabel _) -> -1
| (BuiltinLabel _ | FormalLabel _), (StmtLabel _ | FormalLabel _) -> 1
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 6deba7d75d1e529660d1516ff905088ba8af6f8d..319f65e11a927a36afa0fcaff587ae6524aa7a0e 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -303,7 +303,7 @@ module DatatypeMachdep = Datatype.Make_with_collections(struct
let reprs = [Machdeps.x86_32]
let name = "File.Machdep"
type t = Cil_types.mach
- let compare : t -> t -> int = Transitioning.Stdlib.compare
+ let compare : t -> t -> int = Stdlib.compare
let equal : t -> t -> bool = (=)
let hash : t -> int = Hashtbl.hash
let copy = Datatype.identity
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d0298228e25e382a6a140398d4a14ec0fd524f7b..8bd52d2425db3ee2d4b36909b04efa6b388ae7d4 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -478,7 +478,7 @@ module Type_namespace =
let reprs = [Typedef]
let name = "Logic_typing.type_namespace"
type t = type_namespace
- let compare : t -> t -> int = Transitioning.Stdlib.compare
+ let compare : t -> t -> int = Stdlib.compare
let equal : t -> t -> bool = (=)
let hash : t -> int = Hashtbl.hash
end)
@@ -3614,7 +3614,7 @@ struct
struct
type t = string list
let compare s1 s2 =
- Transitioning.Stdlib.(compare (List.sort compare s1) (List.sort compare s2))
+ Stdlib.(compare (List.sort compare s1) (List.sort compare s2))
end)
let type_spec old_behaviors loc is_stmt_contract result env s =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index bf0b1e828dbf5c66679c255ebaf1c2e306b066c2..bd2af8507ff33b2cc6e28ab4b1557d552988b316 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1657,12 +1657,12 @@ let rec compare_term t1 t2 =
| TAlignOfE _, _ -> 1
| _, TAlignOfE _ -> -1
| TUnOp (o1,t1), TUnOp(o2,t2) ->
- let res = Transitioning.Stdlib.compare o1 o2 in
+ let res = Stdlib.compare o1 o2 in
if res = 0 then compare_term t1 t2 else res
| TUnOp _, _ -> 1
| _, TUnOp _ -> -1
| TBinOp(o1,l1,r1), TBinOp(o2,l2,r2) ->
- let res = Transitioning.Stdlib.compare o1 o2 in
+ let res = Stdlib.compare o1 o2 in
if res = 0 then
let res = compare_term l1 l2 in
if res = 0 then compare_term r1 r2 else res
@@ -1852,7 +1852,7 @@ and compare_predicate_node p1 p2 =
| Papp _, _ -> 1
| _, Papp _ -> -1
| Prel(r1,lt1,rt1), Prel(r2,lt2,rt2) ->
- let res = Transitioning.Stdlib.compare r1 r2 in
+ let res = Stdlib.compare r1 r2 in
if res = 0 then
let res = compare_term lt1 lt2 in
if res = 0 then compare_term rt1 rt2 else res
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index 3d6cefa192d4fa5f37a279ff9591af2a2ee5f606..533be6968e7c37f0b8e0eb30919a465623537770 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -338,8 +338,6 @@ struct
(** {3 String} *)
(* ************************************************************************ *)
- module Pervasives_string = String
-
module String
(X: sig include Parameter_sig.Input_with_arg val default: string end) =
struct
@@ -711,7 +709,7 @@ struct
(* return the list of tokens, in reverse order *)
let parse s =
- let len = Pervasives_string.length s in
+ let len = Stdlib.String.length s in
let rec aux acc pos i s =
if i = len then acc
else
@@ -730,7 +728,7 @@ struct
read_char_in_word
(fun acc -> add_char c (add_char '\\' acc)) (Word false)
in
- match Pervasives_string.get s i, pos with
+ match Stdlib.String.get s i, pos with
| '+', Start when use_category ->
aux (add_action Add acc) (Word true) next s
| '-', Start when use_category ->
@@ -1552,7 +1550,7 @@ struct
in
let r = Str.regexp "[^:]:[^:]" in
let split_delim d =
- (Pervasives_string.sub d 0 1, Pervasives_string.sub d 2 1)
+ (Stdlib.String.sub d 0 1, Stdlib.String.sub d 2 1)
in
let remove_none_and_rev l =
List.fold_left
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 160d39bcf4743e2bb176574380d78f7539e9ac63..8d52b20163f8efcb9f77d1deb3fe64a445a5d7e4 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -46,7 +46,6 @@ let dynlib_init () =
if not !dynlib_init then
begin
dynlib_init := true ;
- Transitioning.Dynlink.init () ;
Dynlink.allow_unsafe_modules true ;
end
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 40e1c3b169904a21ea2f915e39222f25c8ce7b56..06ec07489dc851480fc9b9964637474f4ba26b4c 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -679,7 +679,7 @@ struct
(* the level of verbose is at least the level of debug *)
if n > Verbose.get () then Verbose.set n;
if n = 0 then decr positive_debug_ref
- else if old = 0 then Transitioning.Stdlib.incr positive_debug_ref);
+ else if old = 0 then Stdlib.incr positive_debug_ref);
if is_kernel () then begin
Cmdline.kernel_debug_atleast_ref := (fun n -> get () >= n);
match !Cmdline.Kernel_debug_level.value_if_set with
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 3afa8e4aa0410776bfad147cfd9f04dfefd0c37c..15f719230756dc77631aa9760feed0ebaac405e7 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -1676,13 +1676,13 @@ module With_collections(X: S)(Info: Functor_info) = struct
module Set =
Set
- (Transitioning.Stdlib.Set.Make(D))
+ (Stdlib.Set.Make(D))
(D)
(struct let module_name = Info.module_name ^ ".Set" end)
module Map =
Map
- (Transitioning.Stdlib.Map.Make(D))
+ (Stdlib.Map.Make(D))
(D)
(struct let module_name = Info.module_name ^ ".Map" end)
@@ -1781,7 +1781,7 @@ module Bool =
let name = "bool"
let reprs = [ true ]
let copy = identity
- let compare : bool -> bool -> int = Transitioning.Stdlib.compare
+ let compare : bool -> bool -> int = Stdlib.compare
let equal : bool -> bool -> bool = (=)
let pretty fmt b = Format.fprintf fmt "%B" b
let varname _ = "b"
@@ -1795,12 +1795,12 @@ module Int = struct
let name = "int"
let reprs = [ 2 ]
let copy = identity
- let compare : int -> int -> int = Transitioning.Stdlib.compare
+ let compare : int -> int -> int = Stdlib.compare
let equal : int -> int -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%d" n
let varname _ = "n"
end)
- let compare : int -> int -> int = Transitioning.Stdlib.compare
+ let compare : int -> int -> int = Stdlib.compare
end
let int = Int.ty
@@ -1853,7 +1853,7 @@ module Float =
let name = "float"
let reprs = [ 0.1 ]
let copy = identity
- let compare : float -> float -> int = Transitioning.Stdlib.compare
+ let compare : float -> float -> int = Stdlib.compare
let equal : float -> float -> bool = (=)
let pretty fmt f = Format.fprintf fmt "%f" f
let varname _ = "f"
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 070d355011242fc21581b923dcbf2c73b521422b..f4717ef4eb03594985ed4672be70167f169b777b 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -66,10 +66,10 @@ module type S_no_copy = sig
(** List of representants of the descriptor. *)
val equal: t -> t -> bool
- (** Equality: same spec than [Pervasives.(=)]. *)
+ (** Equality: same spec than [Stdlib.(=)]. *)
val compare: t -> t -> int
- (** Comparison: same spec than [Pervasives.compare]. *)
+ (** Comparison: same spec than [Stdlib.compare]. *)
val hash: t -> int
(** Hash function: same spec than [Hashtbl.hash]. *)
diff --git a/src/libraries/stdlib/FCHashtbl.ml b/src/libraries/stdlib/FCHashtbl.ml
index c5e703592cdab256f351fe8b8208888e0a1c3240..c8a339057523a41e0b6d4e9661ee819cf6257e05 100644
--- a/src/libraries/stdlib/FCHashtbl.ml
+++ b/src/libraries/stdlib/FCHashtbl.ml
@@ -50,7 +50,7 @@ module Make(H: Hashtbl.HashedType) : S with type key = H.t = struct
include Hashtbl.Make(H)
- let fold_sorted ?(cmp=Transitioning.Stdlib.compare) f h acc =
+ let fold_sorted ?(cmp=Stdlib.compare) f h acc =
let module Aux = struct type t = key let compare = cmp end in
let module M = Map.Make(Aux) in
let add k v m =
diff --git a/src/libraries/stdlib/FCHashtbl.mli b/src/libraries/stdlib/FCHashtbl.mli
index e8f59e718087316aafe7b27e737ecb990f1b2904..998aab3dd926769674233ce33bf7ba5d049e2cdf 100644
--- a/src/libraries/stdlib/FCHashtbl.mli
+++ b/src/libraries/stdlib/FCHashtbl.mli
@@ -33,7 +33,7 @@ module type S = sig
val iter_sorted:
?cmp:(key -> key -> int) -> (key -> 'a -> unit) -> 'a t -> unit
(** Iter on the hashtbl, but respecting the order on keys induced
- by [cmp]. Use [Pervasives.compare] if [cmp] not given.
+ by [cmp]. Use [Stdlib.compare] if [cmp] not given.
If the table contains several bindings for the same key, they
are passed to [f] in reverse order of introduction, that is,
@@ -42,7 +42,7 @@ module type S = sig
val fold_sorted:
?cmp:(key -> key -> int) -> (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
(** Fold on the hashtbl, but respecting the order on keys induced
- by [cmp]. Use [Pervasives.compare] if [cmp] not given.
+ by [cmp]. Use [Stdlib.compare] if [cmp] not given.
If the table contains several bindings for the same key, they
are passed to [f] in reverse order of introduction, that is,
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 0714b72b4c9816a4c8a2f4453104fb99bc2fbdab..04d1facd71e8c7df8b9a21aef7b9b054ff26f70b 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -512,6 +512,10 @@ let html_escape s =
) s ;
Buffer.contents buf
+let format_string_of_stag = function
+ | Format.String_tag tag -> tag
+ | _ -> raise (Invalid_argument "unsupported tag extension")
+
(* ************************************************************************* *)
(** Comparison functions *)
(* ************************************************************************* *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 50d3745f5506e63bd47700cd3e88dacfe35122c5..7a1204e843cf57bea0b27b12844c5a73774360b1 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -320,6 +320,13 @@ val strip_underscore: string -> string
val html_escape: string -> string
+(** [format_string_of_stag stag] returns the string corresponding to [stag],
+ or raises an exception if the tag extension is unsupported.
+
+ @since Frama-C+dev
+ *)
+val format_string_of_stag: Format.stag -> string
+
(* ************************************************************************* *)
(** {2 Performance} *)
(* ************************************************************************* *)
@@ -351,9 +358,9 @@ val mkdir : ?parents:bool -> string -> Unix.file_perm -> unit
@since 19.0-Potassium *)
val safe_at_exit : (unit -> unit) -> unit
- (** Register function to call with [Pervasives.at_exit], but only
+ (** Register function to call with [Stdlib.at_exit], but only
for non-child process (fork). The order of execution is preserved
- {i wrt} ordinary calls to [Pervasives.at_exit]. *)
+ {i wrt} ordinary calls to [Stdlib.at_exit]. *)
val cleanup_at_exit: string -> unit
(** [cleanup_at_exit file] indicates that [file] must be removed when the
@@ -386,7 +393,7 @@ val safe_remove_dir: string -> unit
(** Comparison functions *)
(* ************************************************************************* *)
-(** Use this function instead of [Pervasives.compare], as this makes
+(** Use this function instead of [Stdlib.compare], as this makes
it easier to find incorrect uses of the latter *)
external compare_basic: 'a -> 'a -> int = "%compare"
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 6d95b7a1466454402704bd22f262d9bb770d5096..182bc40a8e1af00f6d1329952d449d0f2e6808e1 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -19,112 +19,3 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
-
-module Stdlib = struct
- (* Pervasives/Stdlib functions *)
- let compare = compare
- let succ = succ
- let incr = incr
- let min = min
- let max = max
- let min_int = min_int
- let max_int = max_int
- let flush = flush
- module Set = Set
- module Map = Map
-end
-
-[@@@ warning "-3"]
-
-module Dynlink = struct
- let init = @DYNLINK_INIT@
-end
-
-module Float = struct
- let max_float = @FLOAT_MAX_FLOAT@
-end
-
-module Format = struct
- type stag = Format.@FORMAT_STAG@
- let string_of_stag s = @FORMAT_STRING_OF_STAG@
- let stag_of_string s = @FORMAT_STAG_OF_STRING@
- type formatter_stag_functions = {
- mark_open_stag : stag -> string;
- mark_close_stag : stag -> string;
- print_open_stag : stag -> unit;
- print_close_stag : stag -> unit;
- }
- let pp_set_formatter_stag_functions fmt set_formatter_stag_functions =
- Format.pp_set_formatter_@FORMAT_STAG@_functions fmt
- {
- Format.mark_open_@FORMAT_STAG@ =
- set_formatter_stag_functions.mark_open_stag;
- Format.mark_close_@FORMAT_STAG@ =
- set_formatter_stag_functions.mark_close_stag;
- Format.print_open_@FORMAT_STAG@ =
- set_formatter_stag_functions.print_open_stag;
- Format.print_close_@FORMAT_STAG@ =
- set_formatter_stag_functions.print_close_stag;
- }
- let pp_get_formatter_stag_functions fmt () =
- let st = Format.pp_get_formatter_@FORMAT_STAG@_functions fmt () in
- {
- mark_open_stag = st.Format.mark_open_@FORMAT_STAG@;
- mark_close_stag = st.Format.mark_close_@FORMAT_STAG@;
- print_open_stag = st.Format.print_open_@FORMAT_STAG@;
- print_close_stag = st.Format.print_close_@FORMAT_STAG@;
- }
- let pp_open_stag fmt s =
- Format.pp_open_@FORMAT_STAG@ fmt s
- let pp_close_stag fmt () =
- Format.pp_close_@FORMAT_STAG@ fmt ()
-
- let pp_print_option = @FORMAT_PP_OPT@
-end
-
-module Q = struct
-
- let round_to_float x exact =
- let m = Z.to_int64 x in
- (* Unless the fractional part is exactly 0, round m to an odd integer *)
- let m = if exact then m else Int64.logor m 1L in
- (* Then convert m to float, with the current rounding mode. *)
- Int64.to_float m
-
-
- let to_float x =
- match Q.classify x with
- | Q.ZERO -> 0.0
- | Q.INF -> infinity
- | Q.MINF -> neg_infinity
- | Q.UNDEF -> nan
- | Q.NZERO ->
- let p = x.Q.num and q = x.Q.den in
- let np = Z.numbits p and nq = Z.numbits q in
- if np <= 53 && nq <= 53 then
- (* p and q convert to floats exactly; use FP division to get the
- correctly-rounded result. *)
- Int64.to_float (Z.to_int64 p) /. Int64.to_float (Z.to_int64 q)
- else begin
- (* |p| is in [2^(np-1), 2^np)
- q is in [2^(nq-1), 2^nq)
- hence |p/q| is in (2^(np-nq-1), 2^(np-nq+1)).
- We define n such that |p/q*2^n| is in [2^54, 2^56).
- >= 2^54 so that the round to odd technique applies.
- < 2^56 so that the integral part is representable as an int64. *)
- let n = 55 - (np - nq) in
- (* Scaling p/q by 2^n *)
- let (p', q') =
- if n >= 0
- then (Z.shift_left p n, q)
- else (p, Z.shift_left q (-n)) in
- (* Euclidean division of p' by q' *)
- let (quo, rem) = Z.ediv_rem p' q' in
- (* quo is the integral part of p/q*2^n
- rem/q' is the fractional part. *)
- (* Round quo to float *)
- let f = round_to_float quo (Z.sign rem = 0) in
- (* Apply exponent *)
- ldexp f (-n)
- end
-end
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index b07a1d6bd0bb4138a1840dcd60541f3d82d5c720..d882bcef8ac05f6e0783ad0bf76ed0dbfbebd9f5 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -32,55 +32,3 @@
*)
(** {1 OCaml} *)
-
-(** 4.08 *)
-module Stdlib: sig
- val compare: 'a -> 'a -> int
- val succ: int -> int
- val incr: int ref -> unit
- val min: 'a -> 'a -> 'a
- val max: 'a -> 'a -> 'a
- val min_int: int
- val max_int: int
- val flush: out_channel -> unit
- module Set: module type of Set
- module Map: module type of Map
-end
-
-(** 4.08 *)
-module Dynlink: sig
- val init: unit -> unit
-end
-
-(** 4.07 *)
-module Float: sig
- val max_float: float
-end
-
-(** 4.08 *)
-module Format: sig
- type stag
- val string_of_stag: stag -> string
- val stag_of_string: string -> stag
- type formatter_stag_functions = {
- mark_open_stag : stag -> string;
- mark_close_stag : stag -> string;
- print_open_stag : stag -> unit;
- print_close_stag : stag -> unit;
- }
- val pp_set_formatter_stag_functions:
- Format.formatter -> formatter_stag_functions -> unit
- val pp_get_formatter_stag_functions:
- Format.formatter -> unit -> formatter_stag_functions
- val pp_open_stag : Format.formatter -> stag -> unit
- val pp_close_stag : Format.formatter -> unit -> unit
- val pp_print_option: ?none:(Format.formatter -> unit -> unit) ->
- (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a option -> unit
-end
-
-(** {1 Zarith} *)
-
-(** Function [Q.to_float] was introduced in Zarith 1.5 *)
-module Q: sig
- val to_float : Q.t -> float
-end
diff --git a/src/libraries/utils/bitvector.ml b/src/libraries/utils/bitvector.ml
index e927e6488f05243dcba174f6830a5d9abca64c6b..7aa34b0fa72987a7fbcf37a7695aded378d31f17 100644
--- a/src/libraries/utils/bitvector.ml
+++ b/src/libraries/utils/bitvector.ml
@@ -223,7 +223,7 @@ let bitwise_op4 size op4 a b c d =
let equal = (=);; (* String equality. *)
-let compare = Transitioning.Stdlib.compare
+let compare = Stdlib.compare
let hash = Hashtbl.hash
let concat bv1 size1 bv2 size2 =
diff --git a/src/libraries/utils/dotgraph.ml b/src/libraries/utils/dotgraph.ml
index f162ef75c89ce637b4c50ced8f208c3fba98a07a..3072dbf8b956913d6596465858dba437d97924f6 100644
--- a/src/libraries/utils/dotgraph.ml
+++ b/src/libraries/utils/dotgraph.ml
@@ -128,7 +128,7 @@ let close dot =
begin
Format.fprintf dot.fmt "}@." ;
dot.fmt <- Format.err_formatter ;
- Transitioning.Stdlib.flush out ; close_out out ;
+ Stdlib.flush out ; close_out out ;
dot.out <- None ;
end
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index 40e348054821262bed3b760b550ff50221ed2655..f374ebf853bda2feb075aa70ca7fc4a1b70922d7 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -44,8 +44,8 @@ type json =
| `String of string ]
type t = json
-val equal : t -> t -> bool (** Pervasives *)
-val compare : t -> t -> int (** Pervasives *)
+val equal : t -> t -> bool (** Stdlib *)
+val compare : t -> t -> int (** Stdlib *)
val pp : Format.formatter -> t -> unit
val pp_dump : Format.formatter -> t -> unit (** without formatting *)
diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll
index 491569669a1b011898697c82f0f9b60e4049742a..f17c82ac25de8d3bc772b2ea4eb1141432190980 100644
--- a/src/libraries/utils/json.mll
+++ b/src/libraries/utils/json.mll
@@ -37,7 +37,7 @@ type json =
type t = json
let equal = (=)
-let compare = Transitioning.Stdlib.compare
+let compare = Stdlib.compare
type token = EOF | TRUE | FALSE | NULL | KEY of char
| STR of string | INT of string | DEC of string
diff --git a/src/libraries/utils/pretty_utils.ml b/src/libraries/utils/pretty_utils.ml
index 645b73304e1850265f169ed52e65908914918ae8..2d192599aaa33325aae95373c5c550bd34c703fd 100644
--- a/src/libraries/utils/pretty_utils.ml
+++ b/src/libraries/utils/pretty_utils.ml
@@ -184,7 +184,7 @@ type marger = int ref
let marger () = ref 0
let add_margin marger ?(margin=0) ?(min=0) ?(max=80) text =
let size = String.length text + margin in
- let n = Transitioning.Stdlib.min max (Transitioning.Stdlib.max min size) in
+ let n = Stdlib.min max (Stdlib.max min size) in
if n > !marger then marger := n
type align = [ `Center | `Left | `Right ]
diff --git a/src/libraries/utils/rgmap.ml b/src/libraries/utils/rgmap.ml
index e6d0b182f88970205e3ccdb12d0f411b4395c83e..4888dec36402ea59e368f93c678b15bdc2d865bd 100644
--- a/src/libraries/utils/rgmap.ml
+++ b/src/libraries/utils/rgmap.ml
@@ -42,7 +42,7 @@ type 'a entry = int * int * 'a
module Wmap = Map.Make
(struct
type t = int
- let compare (a:t) (b:t) = Transitioning.Stdlib.compare a b
+ let compare (a:t) (b:t) = Stdlib.compare a b
end)
module Rmap = Map.Make
diff --git a/src/libraries/utils/rich_text.ml b/src/libraries/utils/rich_text.ml
index 2a2a6e8d88b89ba8414bcd335a563c8aeacd5b16..006995446ac7f96006debcb8247caac138c9fdf9 100644
--- a/src/libraries/utils/rich_text.ml
+++ b/src/libraries/utils/rich_text.ml
@@ -27,7 +27,7 @@
type tag = {
p : int ; (* first position *)
q : int ; (* last position (excluded) *)
- tag : Transitioning.Format.stag ;
+ tag : Format.stag ;
children : tag list ;
}
@@ -50,8 +50,8 @@ let tags_at (_,tags) k = lookup [] k tags
type env = {
text : string ;
output : (string -> int -> int -> unit) option ;
- open_tag : (Transitioning.Format.stag -> int -> int -> unit) option ;
- close_tag : (Transitioning.Format.stag -> int -> int -> unit) option ;
+ open_tag : (Format.stag -> int -> int -> unit) option ;
+ close_tag : (Format.stag -> int -> int -> unit) option ;
}
let signal f tag p q =
@@ -86,8 +86,8 @@ let rec output_vbox fmt text k n =
end
let output_fmt fmt text k n = Format.pp_print_string fmt (String.sub text k n)
-let open_tag fmt tag _k _n = Transitioning.Format.pp_open_stag fmt tag
-let close_tag fmt _tag _k _n = Transitioning.Format.pp_close_stag fmt ()
+let open_tag fmt tag _k _n = Format.pp_open_stag fmt tag
+let close_tag fmt _tag _k _n = Format.pp_close_stag fmt ()
let pretty ?vbox fmt message =
let open_tag = open_tag fmt in
@@ -208,8 +208,8 @@ let create ?indent ?margin () =
Format.pp_set_max_indent fmt (max 0 (min k (m-10)))
end ;
let open Format in
- Transitioning.Format.pp_set_formatter_stag_functions fmt {
- Transitioning.Format.print_open_stag = push_tag buffer ;
+ Format.pp_set_formatter_stag_functions fmt {
+ Format.print_open_stag = push_tag buffer ;
print_close_stag = pop_tag buffer ;
mark_open_stag = no_mark ;
mark_close_stag = no_mark ;
diff --git a/src/libraries/utils/rich_text.mli b/src/libraries/utils/rich_text.mli
index f28e688c30324270d72b1f94007a776c04e4920c..1326ed8ca1a9ba0a4772257c23a53f51fda61b3e 100644
--- a/src/libraries/utils/rich_text.mli
+++ b/src/libraries/utils/rich_text.mli
@@ -31,14 +31,14 @@ val char_at : message -> int -> char
val string : message -> string
val substring : message -> int -> int -> string
-val tags_at : message -> int -> (Transitioning.Format.stag * int * int) list
+val tags_at : message -> int -> (Format.stag * int * int) list
(** Returns the list of tags at the given position.
Inner tags come first, outer tags last. *)
val visit :
?output:(string -> int -> int -> unit) ->
- ?open_tag:(Transitioning.Format.stag -> int -> int -> unit) ->
- ?close_tag:(Transitioning.Format.stag -> int -> int -> unit) ->
+ ?open_tag:(Format.stag -> int -> int -> unit) ->
+ ?close_tag:(Format.stag -> int -> int -> unit) ->
message -> unit
(** Visit the message, with depth-first recursion on tags.
All methods are called with text or tag, position and length. *)
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 0bd290f0608a3cf8d647480f03386158d5eaf152..b428aa3c26a5505067728761cf476339de4d3d6e 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -38,9 +38,16 @@ let get_context =
match !context with
| Some c -> c
| None ->
- let c = Context.create () in
- context := Some c;
- c
+ if Db.Value.is_computed () then
+ let c = Context.create () in
+ context := Some c;
+ c
+ else
+ begin
+ Self.error ~once:true
+ "A prior Eva analysis is required to build the graphs.";
+ Server.Data.failure "Eva analysis not computed"
+ end
let global_window = ref {
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 91043aca76ad4b42c112c4f1abe3f10a7c4d0f46..ab451611348a7ad2d828eb43eeac5f8de28ae100 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -53,8 +53,8 @@ module D =
Ival.compare i1 i2
| Float (k1, f1), Float (k2, f2) ->
(* faster to compare a kind than a float *)
- let n = Transitioning.Stdlib.compare k1 k2 in
- if n = 0 then Transitioning.Stdlib.compare f1 f2 else n
+ let n = Stdlib.compare k1 k2 in
+ if n = 0 then Stdlib.compare f1 f2 else n
| Ival _, (Float _ | Rational | Real | Nan)
| Float _, (Rational | Real | Nan)
| Rational, (Real | Nan)
@@ -92,7 +92,7 @@ module D =
let is_included i1 i2 = match i1, i2 with
| Ival i1, Ival i2 -> Ival.is_included i1 i2
| Float(k1, f1), Float(k2, f2) ->
- Transitioning.Stdlib.compare k1 k2 <= 0
+ Stdlib.compare k1 k2 <= 0
&& (match f1, f2 with
| None, None | Some _, None -> true
| None, Some _ -> false
@@ -126,7 +126,7 @@ let lift_binop ~safe_float f i1 i2 = match i1, i2 with
| Ival i1, Ival i2 ->
Ival (f i1 i2)
| Float(k1, _), Float(k2, _) when safe_float ->
- let k = if Transitioning.Stdlib.compare k1 k2 >= 0 then k1 else k2 in
+ let k = if Stdlib.compare k1 k2 >= 0 then k1 else k2 in
Float(k, None (* lost value, if any before *))
| Ival iv, Float(k, _)
| Float(k, _), Ival iv ->
@@ -147,8 +147,8 @@ let lift_binop ~safe_float f i1 i2 = match i1, i2 with
Floating_point.most_negative_single_precision_float,
Floating_point.max_single_precision_float
| FDouble ->
- -. Transitioning.Float.max_float,
- Transitioning.Float.max_float
+ -. Float.max_float,
+ Float.max_float
| FLongDouble ->
raise Exit
in
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index ae46e46f67bec0a1f3d2e307daf1d7528d9f48df..a2612ee906f2595622dd37a63cc835b93b44fd9f 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -67,7 +67,7 @@ module D =
if i1 = i2 then 0
else if Cil.intTypeIncluded i1 i2 then -1 else 1
| C_float f1, C_float f2 ->
- Transitioning.Stdlib.compare f1 f2
+ Stdlib.compare f1 f2
| (C_integer _ | C_float _ | Gmpz | Rational | Real), Nan
| (C_integer _ | C_float _ | Gmpz | Rational ), Real
| (C_integer _ | C_float _ | Gmpz), Rational
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 9c7e60f4979d262a98e8ea79da9a41a0aa9d699d..eb010f92eb65a2cf9cacdd39a3e5ea53a47dd8d4 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -158,14 +158,9 @@ let mk_mark_readonly vi =
let loc = vi.vdecl in
mk_rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
-let mk_runtime_check_with_msg ?(reverse=false) ~loc msg kind kf e =
+let mk_runtime_check_with_msg ~loc msg kind kf e =
let file = (fst loc).Filepath.pos_path in
let line = (fst loc).Filepath.pos_lnum in
- let e =
- if reverse
- then e
- else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
- in
mk_rtl_call ~loc
"assert"
[ e;
@@ -175,13 +170,13 @@ let mk_runtime_check_with_msg ?(reverse=false) ~loc msg kind kf e =
Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
Cil.integer loc line ]
-let mk_runtime_check ?(reverse=false) kind kf e p =
+let mk_runtime_check kind kf e p =
let loc = p.pred_loc in
let msg =
Kernel.Unicode.without_unicode
(Format.asprintf "%a@?" Printer.pp_predicate) p
in
- mk_runtime_check_with_msg ~reverse ~loc msg kind kf e
+ mk_runtime_check_with_msg ~loc msg kind kf e
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index c309ad478045a7e41d6582ae886931bce1b0fdcd..676bfe14af6286cc19179f2d0c8c0aa1a6badc4e 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -80,16 +80,14 @@ type annotation_kind =
| RTE
val mk_runtime_check:
- ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate ->
- stmt
+ annotation_kind -> kernel_function -> exp -> predicate -> stmt
(** [mk_runtime_check kind kf e p] generates a runtime check for predicate [p]
by building a call to [__e_acsl_assert]. [e] (or [!e] if [reverse] is set to
[true]) is the C translation of [p], [kf] is the current kernel_function and
[kind] is the annotation kind of [p]. *)
val mk_runtime_check_with_msg:
- ?reverse:bool -> loc:location -> string -> annotation_kind ->
- kernel_function -> exp -> stmt
+ loc:location -> string -> annotation_kind -> kernel_function -> exp -> stmt
(** [mk_runtime_check_with_msg kind kf e msg] generates a runtime check for [e]
(or [!e] if [reverse] is [true]) by building a call to [__e_acsl_assert].
[msg] is the message printed if the runtime check fails. [loc] is the
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index fe84f48fc299b5204eeb39a5439468e6b6110a5c..d76bac69fc4f89b825141d83ccc88461fb9f0289 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -253,7 +253,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
| Some p ->
let e, env = !named_predicate_ref kf (Env.push env) p in
let stmt, env =
- Constructor.mk_runtime_check ~reverse:true Constructor.RTE kf e p, env
+ Constructor.mk_runtime_check Constructor.RTE kf e p, env
in
let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
let guard_for_small_type = Cil.mkStmt ~valid_sid:true (Block b) in
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index 79332b5913879d1d17cb36cc878279dde66f5669..41a1245eed32cade67ec277a16e931e21de66282 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -159,7 +159,7 @@ let gmp_to_sizet ~loc kf env size p =
None
sizet
(fun vi _ ->
- [ Constructor.mk_runtime_check ~reverse:true Constructor.RTE kf guard p;
+ [ Constructor.mk_runtime_check Constructor.RTE kf guard p;
Constructor.mk_lib_call ~loc
~result:(Cil.var vi)
"__gmpz_get_ui"
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 76d59a3eb9f1ac40038bf5a415dba121d6f77555..4e310e1b4adfbc577e2aaa98178f4be15ed50693 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -364,8 +364,9 @@ and context_insensitive_term_to_exp kf env t =
let guard, env =
let name = Misc.name_of_binop bop ^ "_guard" in
comparison_to_exp
- ~loc kf env Typing.gmpz ~e1:e2 ~name Eq t2 zero t
+ ~loc kf env Typing.gmpz ~e1:e2 ~name Ne t2 zero t
in
+ let p = Logic_const.prel ~loc (Rneq, t2, zero) in
let mk_stmts _v e =
assert (Gmp_types.Z.is_t ty);
let cond =
@@ -373,9 +374,9 @@ and context_insensitive_term_to_exp kf env t =
(Env.annotation_kind env)
kf
guard
- (Logic_const.prel ~loc (Req, t2, zero))
+ p
in
- Env.add_assert kf cond (Logic_const.prel (Rneq, t2, zero));
+ Env.add_assert kf cond p;
let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
[ cond; instr ]
in
@@ -454,7 +455,6 @@ and context_insensitive_term_to_exp kf env t =
let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
let pred = { pred with pred_name = pname :: pred.pred_name } in
let cond = Constructor.mk_runtime_check
- ~reverse:true
Constructor.RTE
kf
coerce_guard
@@ -516,7 +516,6 @@ and context_insensitive_term_to_exp kf env t =
let e1_guard_cond =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
let cond = Constructor.mk_runtime_check
- ~reverse:true
Constructor.RTE
kf
e1_guard
@@ -1058,7 +1057,6 @@ and translate_named_predicate kf env p =
env
kf
(Constructor.mk_runtime_check
- ~reverse:true
(Env.annotation_kind env)
kf
e
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
index 6677db53488571ae0cb179d7c6504944131f9cd8..249a2e3366637540cf22f0fbbc67c8468d49a72d 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
@@ -39,8 +39,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 0xffffffffffffffffffffff ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),"Assertion","main",
- "0xffffffffffffffffffffff == 0","tests/arith/arith.i",18);
+ __e_acsl_assert(__gen_e_acsl_div_guard != 0,"Assertion","main",
+ "0xffffffffffffffffffffff != 0","tests/arith/arith.i",18);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
@@ -108,8 +108,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init(__gen_e_acsl_div_2);
/*@ assert E_ACSL: y - 123456789123456789 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),"Assertion","main",
- "y - 123456789123456789 == 0","tests/arith/arith.i",34);
+ __e_acsl_assert(__gen_e_acsl_div_guard_2 != 0,"Assertion","main",
+ "y - 123456789123456789 != 0","tests/arith/arith.i",34);
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 7ee8de540851b4cfc13f744c22e4e0271e5e0561..0720b6503aa754f974b9df3eb49a3e708e503dd3 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -54,8 +54,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),"Assertion","main",
- "2 == 0","tests/arith/longlong.i",17);
+ __e_acsl_assert(__gen_e_acsl_mod_guard != 0,"Assertion","main","2 != 0",
+ "tests/arith/longlong.i",17);
__gmpz_tdiv_r(__gen_e_acsl_mod,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index 9899c99482fd3a9ee9baba785b2fe903ce547253..9db467e05fce5f01652cb191a4ef603018c77832 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -160,8 +160,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 3 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),"Assertion","main",
- "3 == 0","tests/gmp-only/arith.i",17);
+ __e_acsl_assert(__gen_e_acsl_div_guard != 0,"Assertion","main","3 != 0",
+ "tests/gmp-only/arith.i",17);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
@@ -194,8 +194,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
__gmpz_init(__gen_e_acsl_div_2);
/*@ assert E_ACSL: 0xffffffffffffffffffffff ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),"Assertion","main",
- "0xffffffffffffffffffffff == 0","tests/gmp-only/arith.i",
+ __e_acsl_assert(__gen_e_acsl_div_guard_2 != 0,"Assertion","main",
+ "0xffffffffffffffffffffff != 0","tests/gmp-only/arith.i",
18);
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__13),
@@ -228,8 +228,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),"Assertion","main",
- "2 == 0","tests/gmp-only/arith.i",19);
+ __e_acsl_assert(__gen_e_acsl_mod_guard != 0,"Assertion","main","2 != 0",
+ "tests/gmp-only/arith.i",19);
__gmpz_tdiv_r(__gen_e_acsl_mod,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
@@ -273,8 +273,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
__gmpz_init(__gen_e_acsl_mod_2);
/*@ assert E_ACSL: -2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard_2 == 0),"Assertion","main",
- "-2 == 0","tests/gmp-only/arith.i",20);
+ __e_acsl_assert(__gen_e_acsl_mod_guard_2 != 0,"Assertion","main",
+ "-2 != 0","tests/gmp-only/arith.i",20);
__gmpz_tdiv_r(__gen_e_acsl_mod_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_8),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_9));
@@ -315,8 +315,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
__gmpz_init(__gen_e_acsl_mod_3);
/*@ assert E_ACSL: -2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard_3 == 0),"Assertion","main",
- "-2 == 0","tests/gmp-only/arith.i",21);
+ __e_acsl_assert(__gen_e_acsl_mod_guard_3 != 0,"Assertion","main",
+ "-2 != 0","tests/gmp-only/arith.i",21);
__gmpz_tdiv_r(__gen_e_acsl_mod_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_11));
@@ -574,8 +574,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__55));
__gmpz_init(__gen_e_acsl_div_3);
/*@ assert E_ACSL: y ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_3 == 0),"Assertion","main",
- "y == 0","tests/gmp-only/arith.i",31);
+ __e_acsl_assert(__gen_e_acsl_div_guard_3 != 0,"Assertion","main",
+ "y != 0","tests/gmp-only/arith.i",31);
__gmpz_tdiv_q(__gen_e_acsl_div_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__54),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
@@ -620,8 +620,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__59));
__gmpz_init(__gen_e_acsl_div_4);
/*@ assert E_ACSL: y - 123456789123456789 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_4 == 0),"Assertion","main",
- "y - 123456789123456789 == 0","tests/gmp-only/arith.i",
+ __e_acsl_assert(__gen_e_acsl_div_guard_4 != 0,"Assertion","main",
+ "y - 123456789123456789 != 0","tests/gmp-only/arith.i",
34);
__gmpz_tdiv_q(__gen_e_acsl_div_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 2d2aad9b3d4c1af83cb72d104299de79909de1c8..18b41177870c626626a67afe3571c8922cafc36b 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -151,7 +151,7 @@ module Configuration: sig
val config_values : key:string -> default:'a ->
values:('a * string) list -> 'a #selector -> unit
(** The [values] field is used as a dictionary of available values.
- They are compared with [Pervasives.(=)]. *)
+ They are compared with [Stdlib.(=)]. *)
end
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 6cd8a1f06f72d9e737ecc105de7f43e6f1cf138a..fae7a1f6c75b9dad6da3f7d676e01af913aca608 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -164,8 +164,8 @@ struct
if (pe1 = pe2) then 0
else
(* most englobing comes first *)
- Transitioning.Stdlib.compare pe2 pe1
- else Transitioning.Stdlib.compare pb1 pb2
+ Stdlib.compare pe2 pe1
+ else Stdlib.compare pb1 pb2
) arr
;
arr
@@ -275,14 +275,14 @@ let localizable_from_locs state ~file ~line =
let buffer_formatter state source =
let starts = Stack.create () in
let emit_open_tag s =
- let s = Transitioning.Format.string_of_stag s in
+ let s = Extlib.format_string_of_stag s in
(* Ignore tags that are not ours *)
if Extlib.string_prefix "guitag:" s then
Stack.push (source#end_iter#offset, Tag.get s) starts ;
""
in
let emit_close_tag s =
- let s = Transitioning.Format.string_of_stag s in
+ let s = Extlib.format_string_of_stag s in
(try
if Extlib.string_prefix "guitag:" s then
let (p,sid) = Stack.pop starts in
@@ -295,7 +295,7 @@ let buffer_formatter state source =
Format.pp_set_tags gtk_fmt true;
Format.pp_set_print_tags gtk_fmt false;
Format.pp_set_mark_tags gtk_fmt true;
- let open Transitioning.Format in
+ let open Format in
pp_set_formatter_stag_functions
gtk_fmt {(pp_get_formatter_stag_functions gtk_fmt ())
with
diff --git a/src/plugins/gui/warning_manager.ml b/src/plugins/gui/warning_manager.ml
index 7083cff3e897b5287d409eb001a400ed31f74ab1..e76ee827ccfe9ce32cc7e9c077d086f4fab67af1 100644
--- a/src/plugins/gui/warning_manager.ml
+++ b/src/plugins/gui/warning_manager.ml
@@ -34,7 +34,7 @@ type t =
module Data = Indexer.Make(
struct
type t = int*row
- let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
+ let compare (x,_) (y,_) = Stdlib.compare x y
end)
let make ~packing ~callback =
diff --git a/src/plugins/gui/wtext.ml b/src/plugins/gui/wtext.ml
index fff094c660d5ad8c1ff7a4edbcc78551e4ca8919..7bfe557c97514b4af670d6cb0b61f7de097c69dc 100644
--- a/src/plugins/gui/wtext.ml
+++ b/src/plugins/gui/wtext.ml
@@ -244,7 +244,7 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
end
method private open_tag name =
- let name = Transitioning.Format.string_of_stag name in
+ let name = Extlib.format_string_of_stag name in
self#flush () ; style <- self#tag name :: style ; ""
method private close_tag _name =
@@ -255,7 +255,7 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
| (TAG _ | PLAIN) :: sty -> style <- sty ; ""
method fmt = match fmtref with Some fmt -> fmt | None ->
- let open Transitioning.Format in
+ let open Format in
let output_string s a b = if b > 0 then Buffer.add_substring text s a b in
let fmt = Format.make_formatter output_string self#flush in
let tagger = pp_get_formatter_stag_functions fmt () in
@@ -308,10 +308,9 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
begin
let sid = hid <- succ hid ; Printf.sprintf ">%X" hid in
Hashtbl.add marks sid (fun p q -> Hashtbl.remove marks sid ; f p q) ;
- Transitioning.Format.pp_open_stag fmt
- (Transitioning.Format.stag_of_string sid) ;
+ Format.pp_open_stag fmt (Format.String_tag sid) ;
let () = pp fmt in
- Transitioning.Format.pp_close_stag fmt () ;
+ Format.pp_close_stag fmt () ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index e089ea8ce2d788f66dbfbcc360a2dbad9c4b3629..6e8cc4b68f7771060214537bbe16865d7ea0904f 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -284,7 +284,7 @@ let dump_acsl_stats fmt =
let dump_acsl_stats_html fmt =
- Transitioning.Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
+ Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
Format.fprintf fmt
"@[<v 0> <!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\
\"http://www.w3.org/TR/html4/strict.dtd\">@ \
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index 9a6e2e50dc1d5b6d3376006fabd61d7bfff8465f..c4c0934db605687aeb685d16abaebc37a0b4e5d6 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -26,10 +26,10 @@ open Cil_types (* vname, vaddrof *)
(* Formatting html with Format.formatters *)
let html_stag_functions =
let mark_open_stag t =
- let t = Transitioning.Format.string_of_stag t in
+ let t = Extlib.format_string_of_stag t in
Format.sprintf "<%s>" t
and mark_close_stag t =
- let t = Transitioning.Format.string_of_stag t in
+ let t = Extlib.format_string_of_stag t in
try
let index = String.index t ' ' in
Format.sprintf "</%s>" (String.sub t 0 index)
@@ -38,7 +38,7 @@ let html_stag_functions =
and print_open_stag _ = ()
and print_close_stag _ = ()
in
- { Transitioning.Format.mark_open_stag; mark_close_stag;
+ { Format.mark_open_stag; mark_close_stag;
print_open_stag; print_close_stag; }
;;
@@ -265,7 +265,7 @@ let get_file_type filename =
module VarinfoByName = struct
type t = Cil_types.varinfo
- let compare v1 v2 = Transitioning.Stdlib.compare v1.vname v2.vname
+ let compare v1 v2 = Stdlib.compare v1.vname v2.vname
end
(** Map and sets of varinfos sorted by name (and not by ids) *)
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index e9194fe7aea4922f4e4c761969516a9780223c32..bd8b85522c181da835fdfc7c4e1fc0d628978db6 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Tag functions handling html tags for Format *)
-val html_stag_functions : Transitioning.Format.formatter_stag_functions;;
+val html_stag_functions : Format.formatter_stag_functions;;
(** mk_hdr [level] [ppf] [hdr_strg] produces a title from [hdr_strg] with an
underline of the same length.
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index c6a607be5d638141e0d2269cd2a6ce2a5d1a66d8..e719e52e683d298406b5e70bed2f14c561ea5d3a 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -135,7 +135,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
Format.fprintf fmt "%a" self#pp_file_metrics filename) metrics_map
method print_stats fmt =
- Transitioning.Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
+ Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
Format.pp_set_tags fmt true;
let pr_hdr fmt hdr_name =
Format.fprintf fmt "@{<th>%s@}" hdr_name in
@@ -547,7 +547,7 @@ let pretty_used_files used_files =
let dump_html fmt cil_visitor =
(* Activate tagging for html *)
- Transitioning.Format.pp_set_formatter_stag_functions fmt html_stag_functions;
+ Format.pp_set_formatter_stag_functions fmt html_stag_functions;
Format.pp_set_tags fmt true;
let pr_row s fmt n =
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index ad342ba999a102b65a55f7eb7cd8f5706c437723..4567b97fe13a42312c094644f9f538fe97d21590 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -78,7 +78,7 @@ include Datatype.Make_with_collections
let reprs = [ Global_var ]
let hash (k:k) = Hashtbl.hash k
let equal (k1:k) k2 = k1 = k2
- let compare (k1:k) k2 = Transitioning.Stdlib.compare k1 k2
+ let compare (k1:k) k2 = Stdlib.compare k1 k2
let varname _ = "k"
let internal_pretty_code = Datatype.undefined
let copy = Datatype.identity
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index c2834f47ab666958476dc3921c257fa3669b26e7..e761247ebc70745eeaa92b6a2cd2237e9d70eb28 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -45,7 +45,7 @@ exception Err_Bot of string
(** set of nodes of the graph *)
module BoolNodeSet =
- Transitioning.Stdlib.Set.Make(Datatype.Pair(Datatype.Bool)(PdgTypes.Node))
+ Stdlib.Set.Make(Datatype.Pair(Datatype.Bool)(PdgTypes.Node))
let pretty_node ?(key=false) fmt n =
PdgTypes.Node.pretty fmt n;
diff --git a/src/plugins/qed/export.ml b/src/plugins/qed/export.ml
index b77cd13a68f251ff1d244b35f1562a6a833d2c7e..f0ab696d75cb71ce45d2fe696ab6a7dd8af8d10d 100644
--- a/src/plugins/qed/export.ml
+++ b/src/plugins/qed/export.ml
@@ -828,7 +828,7 @@ struct
(fun (s1,e1) (s2,e2) ->
match s1,s2 with
| true,true | false,false ->
- Transitioning.Stdlib.compare (T.weigth e1) (T.weigth e2)
+ Stdlib.compare (T.weigth e1) (T.weigth e2)
| true,false -> (-1)
| false,true -> 1
) sxs in
diff --git a/src/plugins/qed/intmap.ml b/src/plugins/qed/intmap.ml
index 63cd9aefc1c8f7490df1c40774facc0069e63efa..8aa8b46723aa628f4be0f2511b590dd4d0c850ca 100644
--- a/src/plugins/qed/intmap.ml
+++ b/src/plugins/qed/intmap.ml
@@ -211,12 +211,12 @@ let rec compare cmp s t =
| Empty , _ -> (-1)
| _ , Empty -> 1
| Lf(i,x) , Lf(j,y) ->
- let ck = Transitioning.Stdlib.compare i j in
+ let ck = Stdlib.compare i j in
if ck = 0 then cmp x y else ck
| Lf _ , _ -> (-1)
| _ , Lf _ -> 1
| Br(p,s0,s1) , Br(q,t0,t1) ->
- let cp = Transitioning.Stdlib.compare p q in
+ let cp = Stdlib.compare p q in
if cp <> 0 then cp else
let c0 = compare cmp s0 t0 in
if c0 <> 0 then c0 else
diff --git a/src/plugins/qed/kind.ml b/src/plugins/qed/kind.ml
index eef9ea65a4d01cbbcd6040f2ce711fede63473b1..c2c5e20d2b2d716dc86383c45cb3d3c9dd5d6f67 100644
--- a/src/plugins/qed/kind.ml
+++ b/src/plugins/qed/kind.ml
@@ -177,7 +177,7 @@ let rec compare_tau cfield cadt t1 t2 =
| Prop , Prop -> 0
| Prop , _ -> (-1)
| _ , Prop -> 1
- | Tvar k , Tvar k' -> Transitioning.Stdlib.compare k k'
+ | Tvar k , Tvar k' -> Stdlib.compare k k'
| Tvar _ , _ -> (-1)
| _ , Tvar _ -> 1
| Array(ta,tb) , Array(ta',tb') ->
diff --git a/src/plugins/qed/pool.ml b/src/plugins/qed/pool.ml
index 61234f5c5812c90d6dd3ecf8629086ed2e03e506..7671548f9cf3af414fbc47324688c9e2df9451d2 100644
--- a/src/plugins/qed/pool.ml
+++ b/src/plugins/qed/pool.ml
@@ -77,9 +77,9 @@ struct
let compare x y =
let cmp = String.compare x.vbase y.vbase in
if cmp <> 0 then cmp else
- let cmp = Transitioning.Stdlib.compare x.vrank y.vrank in
+ let cmp = Stdlib.compare x.vrank y.vrank in
if cmp <> 0 then cmp else
- Transitioning.Stdlib.compare x.vid y.vid
+ Stdlib.compare x.vid y.vid
(* POOL *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 3b42acac46a11ff8e899c1b71599b840f11e6fe2..c533be908fb938cb2cc419a53579da64bb6b1d13 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -464,7 +464,7 @@ struct
| Constructor -> 1
| Operator _ -> 0
- let cmp_size a b = Transitioning.Stdlib.compare a.size b.size
+ let cmp_size a b = Stdlib.compare a.size b.size
let rank_bind = function Forall -> 0 | Exists -> 1 | Lambda -> 2
let cmp_bind p q = rank_bind p - rank_bind q
let cmp_field phi (f,x) (g,y) =
@@ -1413,7 +1413,7 @@ struct
| _ -> (k,t) :: acc
(* sorts monoms by terms *)
- let compare_monoms (_,t1) (_,t2) = Transitioning.Stdlib.compare t1.id t2.id
+ let compare_monoms (_,t1) (_,t2) = Stdlib.compare t1.id t2.id
(* factorized monoms *)
let fold_monom ts k t =
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index ba15f820bfa17c098dc679eefd7155835e427a06..08e198b764dd8a9392443d780850e9d7b04ef02d 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -241,7 +241,7 @@ let json_of_event e =
module EVENTS = Set.Make
(struct
type t = event
- let compare = Transitioning.Stdlib.compare
+ let compare = Stdlib.compare
end)
let events_queue = Queue.create ()
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index 680de39c07f068e09c6a73a3e061feee0d4d919a..7d50b76be8d88a410e194c2d9a81f5c7152cdf45 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -66,7 +66,7 @@ let lines () =
emitted on statements copied through loop unrolling. This is the desired
semantics for now. However, since we compare entire locations, textually
identical lines that refer to different expressions are kept separate *)
- Extlib.sort_unique Transitioning.Stdlib.compare l
+ Extlib.sort_unique Stdlib.compare l
let output file =
let ch = open_out file in
diff --git a/src/plugins/server/jbuffer.ml b/src/plugins/server/jbuffer.ml
index 64a536cf7662ea50fe0aa0c18f206ce3cf0a6014..f7ca9ebbfe05418e06440810bca2103881afd3b3 100644
--- a/src/plugins/server/jbuffer.ml
+++ b/src/plugins/server/jbuffer.ml
@@ -41,7 +41,7 @@ let flush buffer () =
Buffer.clear t
let push_tag buffer stag =
- let tag = Transitioning.Format.string_of_stag stag in
+ let tag = Extlib.format_string_of_stag stag in
flush buffer () ;
buffer.stack <- ( tag , buffer.rjson ) :: buffer.stack ;
buffer.rjson <- []
@@ -84,7 +84,7 @@ let create ?indent ?margin () =
Format.pp_set_max_indent fmt (max 0 (min k (m-10)))
end ;
begin
- let open Transitioning.Format in
+ let open Format in
pp_set_formatter_stag_functions fmt {
print_open_stag = no_mark ;
print_close_stag = no_mark ;
diff --git a/src/plugins/server/jbuffer.mli b/src/plugins/server/jbuffer.mli
index 9db8cfab7eaed970a0cba77b1af9e913d1f4c161..2a825a04f0f8f0fbc42efba13991bb55d88c6ac6 100644
--- a/src/plugins/server/jbuffer.mli
+++ b/src/plugins/server/jbuffer.mli
@@ -48,8 +48,8 @@ val bprintf : buffer -> ('a,Format.formatter,unit) format -> 'a
val append : buffer -> string -> int -> int -> unit
val flush : buffer -> unit -> unit
-val push_tag : buffer -> Transitioning.Format.stag -> unit
-val pop_tag : buffer -> Transitioning.Format.stag -> unit
+val push_tag : buffer -> Format.stag -> unit
+val pop_tag : buffer -> Format.stag -> unit
(** Flushes the buffer and returns its JSON enoding. This pops all pending
tags. *)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index cf64d538e89a29899ab61df41bfb2cff5827e309..832c1adce2b70ba182a4549234391d18512c4f28 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -385,10 +385,10 @@ module Info = struct
open Printer_tag
let print_function fmt name =
- let stag = Transitioning.Format.stag_of_string name in
- Transitioning.Format.pp_open_stag fmt stag;
+ let stag = Format.String_tag name in
+ Format.pp_open_stag fmt stag;
Format.pp_print_string fmt name;
- Transitioning.Format.pp_close_stag fmt ()
+ Format.pp_close_stag fmt ()
let print_kf fmt kf = print_function fmt (Kernel_function.get_name kf)
@@ -399,7 +399,7 @@ module Info = struct
let pp_kf fmt kf = Format.fprintf fmt " of function %a" print_kf kf in
Format.fprintf fmt "It is a %s variable%a.@."
(if vi.vglob then "global" else if vi.vformal then "formal" else "local")
- (Transitioning.Format.pp_print_option pp_kf) kf;
+ (Format.pp_print_option pp_kf) kf;
if vi.vtemp then
Format.fprintf fmt "This is a temporary variable%s.@."
(match vi.vdescr with None -> "" | Some descr -> " for " ^ descr);
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index 39ac4af5b98a0ecf6a4b71ba01dedd1b1da56599..309cae632565703288b5cc95ca1a5793215cfba5 100644
--- a/src/plugins/server/package.ml
+++ b/src/plugins/server/package.ml
@@ -46,7 +46,7 @@ let pp_ident fmt { plugin ; package ; name } =
(* --- Name Resolution --- *)
(* -------------------------------------------------------------------------- *)
-module Std = Transitioning.Stdlib
+module Std = Stdlib
module Id = struct type t = ident let compare = Std.compare end
module IdMap = Map.Make(Id)
module IdSet = Set.Make(Id)
diff --git a/src/plugins/server/server_batch.ml b/src/plugins/server/server_batch.ml
index 2df2d4d2567d1649b23219aa05712a9886951398..4fc37a40aa6850f9a8dfcbf01313317f67356436 100644
--- a/src/plugins/server/server_batch.ml
+++ b/src/plugins/server/server_batch.ml
@@ -102,7 +102,13 @@ let execute () =
List.iter
begin fun file ->
Senv.feedback "Script %S" file ;
- let response = execute_batch (Js.from_file file) in
+ let response =
+ try
+ execute_batch (Js.from_file file)
+ with Yojson.Json_error msg ->
+ Senv.error "[batch] error in JSON file:@\n%s@." msg;
+ `Null
+ in
let output = Filename.remove_extension file ^ ".out.json" in
let output = match BatchOutputDir.get () with
| "" -> output
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 522cc6584cfffdbadf3508ce01515780ef9ab1d5..9b7365eb82294c163c339f797c5139ba077d938e 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -237,7 +237,7 @@ let table_of_contents () =
module Cmap = Map.Make
(struct
type t = string list
- let compare = Transitioning.Stdlib.compare
+ let compare = Stdlib.compare
end)
let index_entry (title,href) =
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 21475b79a7a7d523304ec22c16b5d8ed8b76e2d5..b0bd8fb82ac6e22c451e767cf9b015e9dbb8e2b6 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -48,7 +48,7 @@ module Status = struct
let reprs = [ True; False; False; Unknown ]
let mem_project = Datatype.never_any_project
let pretty = pretty_status
- let compare (s1:t) (s2:t) = Transitioning.Stdlib.compare s1 s2
+ let compare (s1:t) (s2:t) = Stdlib.compare s1 s2
let equal (s1:t) (s2:t) = s1 = s2
let hash (s:t) = Hashtbl.hash s
end)
diff --git a/src/plugins/value/domains/domain_mode.ml b/src/plugins/value/domains/domain_mode.ml
index 298f27fc57d885a4b0c438fe24e4388ad983f435..2d0788ba113800847d38ef598287acdadce0e407 100644
--- a/src/plugins/value/domains/domain_mode.ml
+++ b/src/plugins/value/domains/domain_mode.ml
@@ -39,7 +39,7 @@ module Mode = struct
type t = mode
let name = "Domain_mode.Mode"
let reprs = [ default ]
- let compare = Transitioning.Stdlib.compare
+ let compare = Stdlib.compare
let equal = Datatype.from_compare
let hash = Hashtbl.hash
end)
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 4c8dec87e1ecf236a920ef4eb38a1134f3a6ceb7..2f2bcab9c4bce90fd2be0cea767426d5261b29f7 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -502,7 +502,7 @@ module G = struct
let compare ii1 ii2 = match ii1, ii2 with
| PreciseIteration i1, PreciseIteration i2 ->
- Transitioning.Stdlib.compare i1 i2
+ Stdlib.compare i1 i2
| MultipleIterations i1, MultipleIterations i2 ->
MultipleIterations.compare i1 i2
| PreciseIteration _, MultipleIterations _ -> -1
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index c7cb5f5219d7ce702517e27cfac0d85b2b665b05..32548a62121bc92a17f752c05235b6fdfe1e6960 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -135,7 +135,7 @@ end = struct
| Assume (_, e1, b1), Assume (_, e2, b2) ->
let c = ExpStructEq.compare e1 e2 in
if c <> 0 then c else
- Transitioning.Stdlib.compare b1 b2
+ Stdlib.compare b1 b2
| EnterScope (_, vs1), EnterScope (_, vs2) ->
Extlib.list_compare Varinfo.compare vs1 vs2
| LeaveScope (_, vs1), LeaveScope (_, vs2) ->
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index 8b9f681f75c233319637e4bc5f6dbd8b2b1b9cc1..bbb192034aa53b3582b4ecdc77789c03864cd1e8 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -261,7 +261,7 @@ module Make (Input: Input) = struct
module Data = Indexer.Make(
struct
type t = int * value row
- let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
+ let compare (x,_) (y,_) = Stdlib.compare x y
end)
(* This function creates a single GTree that displays per-callstack
diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml
index 8671ed982494460661e53c88939c4ae85d6b9e5e..1e6c0ffb11d8e7f62fa1bb8831407e67b413feed 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -108,7 +108,7 @@ type t =
module Data = Indexer.Make(
struct
type t = int*row
- let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
+ let compare (x,_) (y,_) = Stdlib.compare x y
end)
let append t message = t.append message
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index 9722347d7d85b1bbd54e823b3f1a5ec5876c4c27..197bad845fccfff841887077319631212f0f0c40 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -52,7 +52,7 @@ module Make () = struct
then Some ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
else None
- let compare x y = Transitioning.Stdlib.compare x.tag y.tag
+ let compare x y = Stdlib.compare x.tag y.tag
let hash x = x.tag
let tag x = x.tag
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index bb7ebcf7d266a91dcd7029d0e68bdd9cb61263e7..6dea7f2ed2919b1dce27acfa2f1bc8aaa2d10de9 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -88,7 +88,7 @@ module Call_info = struct
(* Sorts call_infos by decreasing execution time. *)
let cmp current_time ci1 ci2 =
- - (Transitioning.Stdlib.compare (total_duration current_time ci1) (total_duration current_time ci2))
+ - (Stdlib.compare (total_duration current_time ci1) (total_duration current_time ci2))
;;
(* From an iteration, filter and sort by call_info, and returns the
diff --git a/src/plugins/value/values/numerors/numerors_interval.ml b/src/plugins/value/values/numerors/numerors_interval.ml
index 4a65ac8f170652a0550f919a21e9ca8bce854744..7f1e0f63bf46db8409b8cec9ab3b9d09e114a71b 100644
--- a/src/plugins/value/values/numerors/numerors_interval.ml
+++ b/src/plugins/value/values/numerors/numerors_interval.ml
@@ -52,7 +52,7 @@ let prec = function NaN p -> p | I (x, _, _) -> F.prec x
let get_max_exponent = function
| NaN _ -> Value_parameters.fatal "Numerors: can't return the exponent of a NaN"
- | I (x, y, _) -> Transitioning.Stdlib.max (F.exponent x) (F.exponent y)
+ | I (x, y, _) -> Stdlib.max (F.exponent x) (F.exponent y)
let get_exponents = function
| NaN _ -> Value_parameters.fatal "Numerors: can't return the exponent of a NaN"
@@ -171,7 +171,7 @@ let compare a b = (a, b) >>+ fun _ ->
match a, b with
| NaN _, NaN _ -> 0 | NaN _, _ -> 1 | _, NaN _ -> -1
| I (x, y, n), I (x', y', n') ->
- let c = Transitioning.Stdlib.compare n n' in
+ let c = Stdlib.compare n n' in
if c = 0 then
let c = F.compare x x' in
if c = 0 then F.compare y y'
diff --git a/src/plugins/value/values/numerors/numerors_utils.ml b/src/plugins/value/values/numerors/numerors_utils.ml
index 85e6f155b27b6036d1b0671105eca7f02b74f7d2..41d0d26e91ec68440dff2d5433b6afa7217a0efe 100644
--- a/src/plugins/value/values/numerors/numerors_utils.ml
+++ b/src/plugins/value/values/numerors/numerors_utils.ml
@@ -51,15 +51,15 @@ module Precisions = struct
(* Defined by the IEEE-754 standard *)
let exponent = function
| Simple -> 8 | Double -> 11
- | Long_Double -> 15 | Real -> Transitioning.Stdlib.max_int
+ | Long_Double -> 15 | Real -> Stdlib.max_int
(* Computed as - ((2 - 2^(e-1)) - (m - 1)) where e is the number of bits of
the exponent and m is the number of bits of the significand *)
let denormalized = function
| Simple -> -149 | Double -> -1074
- | Long_Double -> -16494 | Real -> Transitioning.Stdlib.min_int
+ | Long_Double -> -16494 | Real -> Stdlib.min_int
- let compare a b = Transitioning.Stdlib.compare (get a) (get b)
+ let compare a b = Stdlib.compare (get a) (get b)
let eq a b = compare a b = 0
let max a b = if compare a b <= 0 then b else a
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 93051f60d086a6613c33d8327a049d52343fb9f8..1a119b7433829124d0aab9784e0611a2baf90ee4 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -54,7 +54,7 @@ let empty = { pos = false; zero = false; neg = false }
include Datatype.Make(struct
type t = signs
include Datatype.Serializable_undefined
- let compare = Transitioning.Stdlib.compare
+ let compare = Stdlib.compare
let equal = Datatype.from_compare
let hash = Hashtbl.hash
let reprs = [top]
diff --git a/src/plugins/wp/CfgCompiler.ml b/src/plugins/wp/CfgCompiler.ml
index e0f6bda712ed89f21b706b64a417f588963560a2..62b804223326d9a21858e983f7004efe3817d050 100644
--- a/src/plugins/wp/CfgCompiler.ml
+++ b/src/plugins/wp/CfgCompiler.ml
@@ -437,7 +437,7 @@ struct
let pp fmt = function | Node i -> Node.pp fmt i | Assume (i,_) -> Format.fprintf fmt "ass%i" i
| Check (i,_) -> Format.fprintf fmt "chk%i" i
let equal x y = (tag x) = (tag y)
- let compare x y = Transitioning.Stdlib.compare (tag x) (tag y)
+ let compare x y = Stdlib.compare (tag x) (tag y)
let hash x = tag x
end in
let module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (V)(E) in
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 64e1cfd7065d4bd0a9de71a2afe0eb99abc6de41..04ccb8f815113a5a3d9fb346bcac84af4a2f55b3 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -145,7 +145,7 @@ let fmake ulp value = match ulp with
| Float32 -> F.e_fun ~result:t32 fq32 [F.e_float (rfloat value)]
| Float64 -> F.e_fun ~result:t64 fq64 [F.e_float value]
-let qmake ulp q = fmake ulp (Transitioning.Q.to_float q)
+let qmake ulp q = fmake ulp (Q.to_float q)
let re_mantissa = "\\([-+]?[0-9]*\\)"
let re_comma = "\\(.\\(\\(0*[1-9]\\)*\\)0*\\)?"
let re_exponent = "\\([eE]\\([-+]?[0-9]*\\)\\)?"
@@ -219,8 +219,8 @@ let force_float r =
let float_lit ulp (q : Q.t) =
let v = match ulp with
- | Float32 -> rfloat @@ Transitioning.Q.to_float q
- | Float64 -> Transitioning.Q.to_float q in
+ | Float32 -> rfloat @@ Q.to_float q
+ | Float64 -> Q.to_float q in
let reparse ulp r =
match ulp with
| Float32 -> rfloat @@ float_of_string r
@@ -314,7 +314,7 @@ module Compute = WpContext.StaticGenerator
(struct
type t = model * c_float * op
- let compare = Transitioning.Stdlib.compare
+ let compare = Stdlib.compare
let pretty fmt (m, ft, op) =
Format.fprintf fmt "%s_%a_%s" (model_name m) pp_suffix ft (op_name op)
diff --git a/src/plugins/wp/Cmath.ml b/src/plugins/wp/Cmath.ml
index 5f00300cf14dfba7ae6422c690767924f6cb049a..96b326d43d9dffbadd0e8b9d0631ebae354f2c03 100644
--- a/src/plugins/wp/Cmath.ml
+++ b/src/plugins/wp/Cmath.ml
@@ -71,7 +71,7 @@ let builtin_truncate f e =
begin
try
(* Waiting for Z-Arith to have truncation to big-int *)
- let truncated = int_of_float (Transitioning.Q.to_float r) in
+ let truncated = int_of_float (Q.to_float r) in
let reversed = Q.of_int truncated in
let base = F.e_int truncated in
if Q.equal r reversed then base else
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 9acc9575ac31a2b3502930433420575c0d39643e..d6e531f56be84457ef273df9c4db17a9d8391ccd 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -270,7 +270,7 @@ struct
| _ -> 2
in
let r = rank s1.condition - rank s2.condition in
- if r = 0 then Transitioning.Stdlib.compare k2 k1 else r
+ if r = 0 then Stdlib.compare k2 k1 else r
end)
type t = Vars.t * SEQ.t
diff --git a/src/plugins/wp/Cstring.ml b/src/plugins/wp/Cstring.ml
index 7705498957b67213b63c2dc7142c5bd396f6b3f7..d5d2ceb8a4cfb3a0ac8dde152e2d289baec2a90c 100644
--- a/src/plugins/wp/Cstring.ml
+++ b/src/plugins/wp/Cstring.ml
@@ -35,7 +35,7 @@ type cst =
module STR =
struct
type t = cst
- let compare = Transitioning.Stdlib.compare (* only comparable types *)
+ let compare = Stdlib.compare (* only comparable types *)
let pretty fmt = function
| C_str s -> Format.fprintf fmt "%S" s
| W_str _ -> Format.fprintf fmt "\"L<...>\""
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 7d388748ccf4a9b092b3dc9b26d061e00ab97770..f6a1a01a5d9e183c1405b213830f25f60c9d4c80 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -34,7 +34,7 @@ type setup = {
cfloat : Cfloat.model ;
}
-(*[LC] All types in [model] must be Pervasives-comparable *)
+(*[LC] All types in [model] must be Stdlib-comparable *)
type driver = LogicBuiltins.driver
@@ -304,7 +304,7 @@ module COMPILERS = Map.Make
(struct
type t = setup * driver
let compare (s,d) (s',d') =
- let cmp = Transitioning.Stdlib.compare s s' in
+ let cmp = Stdlib.compare s s' in
if cmp <> 0 then cmp else LogicBuiltins.compare d d'
end)
diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml
index 2045b0c8586b82ab08b67d3dd4fcc6d550042a41..d1e8b5795328c83d795393ebc8b699a997b0749b 100644
--- a/src/plugins/wp/Layout.ml
+++ b/src/plugins/wp/Layout.ml
@@ -52,7 +52,7 @@ struct
| _ , Field _ -> 1
| Index(ta,n) , Index(tb,m) ->
let cmp = Typ.compare ta tb in
- if cmp <> 0 then cmp else Transitioning.Stdlib.compare n m
+ if cmp <> 0 then cmp else Stdlib.compare n m
let equal a b = (compare a b = 0)
@@ -175,7 +175,7 @@ struct
Usage.pretty fmt usage
let compare ((da,ta):t) ((db,tb):t) =
- let cmp = Transitioning.Stdlib.compare da db in
+ let cmp = Stdlib.compare da db in
if cmp <> 0 then cmp else Typ.compare ta tb
let equal a b = (compare a b = 0)
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index e713b74ade46db3ccab2d7746acc4c613061270b..e08114243391f957a51271c62bc30c5e258145dd 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -182,14 +182,14 @@ let iter_table f =
Hashtbl.iter
(fun a sigs -> List.iter (fun (ks,lnk) -> items := (a,ks,lnk)::!items) sigs)
(cdriver_ro ()).hlogic ;
- List.iter f (List.sort Transitioning.Stdlib.compare !items)
+ List.iter f (List.sort Stdlib.compare !items)
let iter_libs f =
let items = ref [] in
Hashtbl.iter
(fun a libs -> items := (a,libs) :: !items)
(cdriver_ro ()).hdeps ;
- List.iter f (List.sort Transitioning.Stdlib.compare !items)
+ List.iter f (List.sort Stdlib.compare !items)
let dump () =
Log.print_on_output
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 427bd92700c4405e3c9b2c2abc65e405af971fa8..3723ce4232264c2faccafea2a67ae8216a808eab 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -234,7 +234,7 @@ struct
Format.fprintf fmt "}@]" ;
end
- let compare = Transitioning.Stdlib.compare
+ let compare = Stdlib.compare
(* Extract constant offset *)
let offset k =
@@ -300,7 +300,7 @@ module ARRAY =
struct
type t = int * int list
- let compare = Transitioning.Stdlib.compare
+ let compare = Stdlib.compare
let pretty fmt (s,ds) = Format.fprintf fmt "%d%a" s Layout.Matrix.pretty ds
(* Coefficient from Matrix dimensions: c_i = \Pi_{i<j} d_j *)
@@ -637,7 +637,7 @@ struct
let hash m = id m
let compare m m' =
- if m==m then 0 else Transitioning.Stdlib.compare (id m) (id m')
+ if m==m then 0 else Stdlib.compare (id m) (id m')
let equal m m' = m==m' || (id m = id m')
let tau_of_value = function
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 90311c627cfb9ae4ae5c87405d93f58aea8179c5..6743fc7a086ad6307be7534c6fe25eeff69917dd 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -390,7 +390,7 @@ let shift l obj k = e_fun (Shift.get obj) [l;k]
module LITERAL =
struct
type t = int * Cstring.cst
- let compare (a:t) (b:t) = Transitioning.Stdlib.compare (fst a) (fst b)
+ let compare (a:t) (b:t) = Stdlib.compare (fst a) (fst b)
let pretty fmt (eid,cst) = Format.fprintf fmt "%a@%d" Cstring.pretty cst eid
end
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index e2e434090d6de3baeb9aa0430a998943ec8bb00f..9458666cfc60d2dcc01e346c2aba174f0f1afde5 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -47,7 +47,7 @@ struct
let sa = stage a in
let sb = stage b in
if sa = sb
- then Transitioning.Stdlib.compare (time a) (time b)
+ then Stdlib.compare (time a) (time b)
else sa - sb
let sort script = List.stable_sort compare script
diff --git a/src/plugins/wp/Region.ml b/src/plugins/wp/Region.ml
index de1feb7484424035fcbc68725ce611bcf1a17984..0de209c12f6bf8041c70125a7fef262e4c327e6d 100644
--- a/src/plugins/wp/Region.ml
+++ b/src/plugins/wp/Region.ml
@@ -128,7 +128,7 @@ struct
type t = region
let id a = a.id
let equal a b = (a.id = b.id)
- let compare a b = Transitioning.Stdlib.compare a.id b.id
+ let compare a b = Stdlib.compare a.id b.id
let pp_rid fmt id = Format.fprintf fmt "R%03d" id
let pretty fmt r = pp_rid fmt r.id
end
diff --git a/src/plugins/wp/Splitter.ml b/src/plugins/wp/Splitter.ml
index b5930b40748cf9752bc470ee58ebb5c1eb70baf0..32dfd8adf7a1bd0952154b8321635a33af8211f1 100644
--- a/src/plugins/wp/Splitter.ml
+++ b/src/plugins/wp/Splitter.ml
@@ -63,7 +63,7 @@ let compare p q =
| _ , ELSE _ -> 1
| CASE(s1,k1) , CASE(s2,k2) ->
let c = Stmt.compare s1 s2 in
- if c = 0 then Transitioning.Stdlib.compare k1 k2 else c
+ if c = 0 then Stdlib.compare k1 k2 else c
| CASE _ , _ -> (-1)
| _ , CASE _ -> 1
| DEFAULT s , DEFAULT t -> Stmt.compare s t
@@ -75,7 +75,7 @@ let compare p q =
| CALL _ , _ -> (-1)
| _ , CALL _ -> 1
| ASSERT(ip1,k1,_) , ASSERT(ip2,k2,_) ->
- let c = Transitioning.Stdlib.compare ip1.ip_id ip2.ip_id in
+ let c = Stdlib.compare ip1.ip_id ip2.ip_id in
if c = 0 then k1 - k2 else c
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 22b7335e91ecd96befa323fb73703dcab40a81ba..234884282f5195ff5ffad5ee1f4368b93b9537cb 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -499,7 +499,7 @@ struct
| NoneInfo, NoneInfo -> 0
| NoneInfo, _ -> -1
| _ , NoneInfo -> 1
- | LoopHead i, LoopHead j -> Transitioning.Stdlib.compare j i
+ | LoopHead i, LoopHead j -> Stdlib.compare j i
module Automata = Interpreted_automata.UnrollUnnatural.Version
type nodes = {
diff --git a/src/plugins/wp/Strategy.ml b/src/plugins/wp/Strategy.ml
index 1ce102defda986389209d719d68e8a0b6077e1c9..cf232eaa0dcd6b43601e9ec08574d6c03d827cfe 100644
--- a/src/plugins/wp/Strategy.ml
+++ b/src/plugins/wp/Strategy.ml
@@ -104,7 +104,7 @@ type strategy = {
arguments : argument list ;
} and t = strategy
-let highest a b = Transitioning.Stdlib.compare b.priority a.priority
+let highest a b = Stdlib.compare b.priority a.priority
class pool =
object
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index c92b0ca59fb985c1a5b76353ce52de64594e1ba7..1a855c3bbbe474b41d5fb2df7d0fc903235b27e0 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -354,11 +354,11 @@ let compare p q =
in
let r = rank q.verdict - rank p.verdict in
if r <> 0 then r else
- let s = Transitioning.Stdlib.compare p.prover_steps q.prover_steps in
+ let s = Stdlib.compare p.prover_steps q.prover_steps in
if s <> 0 then s else
- let t = Transitioning.Stdlib.compare p.prover_time q.prover_time in
+ let t = Stdlib.compare p.prover_time q.prover_time in
if t <> 0 then t else
- Transitioning.Stdlib.compare p.solver_time q.solver_time
+ Stdlib.compare p.solver_time q.solver_time
let combine v1 v2 =
match v1 , v2 with
diff --git a/src/plugins/wp/Warning.ml b/src/plugins/wp/Warning.ml
index f5c88a6dddb922970b978f3f6c85f60026691115..00664bb1670f5f34b80f9d0685150e8854932e81 100644
--- a/src/plugins/wp/Warning.ml
+++ b/src/plugins/wp/Warning.ml
@@ -48,7 +48,7 @@ struct
match w1.severe , w2.severe with
| true , false -> (-1)
| false , true -> 1
- | _ -> Transitioning.Stdlib.compare w1 w2
+ | _ -> Stdlib.compare w1 w2
end
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 232c05888e6f00a5ba13a24e09495becd39a764c..ab50c9858b2de0a3fec9d8adc147994a3e0db981 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -46,9 +46,9 @@ let configure =
begin try
Arg.parse_argv ~current:(ref 0) args
(Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list])
- (fun _ -> raise (Arg.Help "Unknown why3 option"))
+ (fun opt -> raise (Arg.Bad ("unknown option: " ^ opt)))
"Why3 options"
- with Arg.Bad s -> Wp_parameters.abort "%s" s
+ with Arg.Bad s | Arg.Help s -> Wp_parameters.abort "%s" s
end;
ignore (Why3.Debug.Args.option_list ());
Why3.Debug.Args.set_flags_selected ();
diff --git a/src/plugins/wp/clabels.mli b/src/plugins/wp/clabels.mli
index cb577648c59219916a8e69b3b22e7e95f8145423..26bdbfb4fcbdce2eb8ea16e372f9147ba91b926e 100644
--- a/src/plugins/wp/clabels.mli
+++ b/src/plugins/wp/clabels.mli
@@ -26,7 +26,7 @@
(**
Structural representation of logic labels.
- Compatible with pervasives comparison and structural equality.
+ Compatible with stdlib comparison and structural equality.
*)
type c_label
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 0dcff7411efc6a4cd32044713b52b6f597d4d1f7..303790f3b75d254f3e616e6b92cfa919eafbe3fb 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -323,7 +323,7 @@ module AinfoComparable = struct
let c = !cmp obj_a obj_b in
if c <> 0 then c
else match a.arr_flat , b.arr_flat with
- | Some a , Some b -> Transitioning.Stdlib.compare a.arr_size b.arr_size
+ | Some a , Some b -> Stdlib.compare a.arr_size b.arr_size
| None , Some _ -> (-1)
| Some _ , None -> 1
| None , None -> 0
@@ -599,7 +599,7 @@ and compare_array_ptr_conflated a b =
let c = compare_ptr_conflated obj_a obj_b in
if c <> 0 then c
else match a.arr_flat , b.arr_flat with
- | Some a , Some b -> Transitioning.Stdlib.compare a.arr_size b.arr_size
+ | Some a , Some b -> Stdlib.compare a.arr_size b.arr_size
| None , Some _ -> (-1)
| Some _ , None -> 1
| None , None -> 0
diff --git a/src/plugins/wp/proof.ml b/src/plugins/wp/proof.ml
index 9a6c21a585f181c0fe9e197fb8deed89b835d302..795ac2b52701be870f3507aab0d7a13e880c7f18 100644
--- a/src/plugins/wp/proof.ml
+++ b/src/plugins/wp/proof.ml
@@ -225,7 +225,7 @@ let update_hints_for_goal goal hints =
try
let old_hints,script,qed = Hashtbl.find scriptbase goal in
let new_hints = List.sort String.compare hints in
- if Transitioning.Stdlib.compare new_hints old_hints <> 0 then
+ if Stdlib.compare new_hints old_hints <> 0 then
begin
Hashtbl.replace scriptbase goal (new_hints,script,qed) ;
needsave := true ;
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 9821c657890900dac6b7ba825e5dc6c5f025f2d1..7b694b72a677719f0c8bd1f6334bd8c24ceeb5d3 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -216,7 +216,7 @@ let compare_kind k1 k2 = match k1, k2 with
if cmp <> 0 then cmp
else
Property.compare p1 p2
- | _,_ -> Transitioning.Stdlib.compare (kind_order k1) (kind_order k2)
+ | _,_ -> Stdlib.compare (kind_order k1) (kind_order k2)
let compare_prop_id pid1 pid2 =
(* This order of comparison groups together prop_pids with same properties *)
@@ -228,7 +228,7 @@ let compare_prop_id pid1 pid2 =
let cmp = compare_kind pid2.p_kind pid1.p_kind in
if cmp <> 0 then cmp
else
- Transitioning.Stdlib.compare pid1.p_part pid2.p_part
+ Stdlib.compare pid1.p_part pid2.p_part
module PropId =
Datatype.Make_with_collections(
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..eb6734b3ca4224a9a3b0f2b872a3d83b8317b4f6 100644
--- a/tests/fc_script/oracle/make_template.res
+++ b/tests/fc_script/oracle/make_template.res
@@ -1,6 +1,15 @@
+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] Created stub for main function: result/fc_stubs.c
+Template created: result/GNUmakefile
Running ptests: cleaning up after tests...