diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 9e7fc4010aba93779273e9d65cb4fc7d625a29ac..cae5f59e1f52990ea1df0ee8aa9ecab4caddfe69 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -359,6 +359,27 @@ module Functions = struct
else
res
+ let mem_name fct_name =
+ try
+ ignore (find_by_name fct_name);
+ true
+ with Not_found ->
+ false
+
+ let mem_def_name fct_name =
+ try
+ ignore (find_def_by_name fct_name);
+ true
+ with Not_found ->
+ false
+
+ let mem_decl_name fct_name =
+ try
+ ignore (find_decl_by_name fct_name);
+ true
+ with Not_found ->
+ false
+
let () =
Parameter_builder.find_kf_by_name := find_by_name;
Parameter_builder.find_kf_def_by_name := find_def_by_name;
@@ -741,10 +762,18 @@ module Types = struct
TypeNameToGlobal.mark_as_computed ()
end
+ let mem_enum_tag x =
+ resolve_types ();
+ Enums.mem x
+
let find_enum_tag x =
resolve_types ();
Enums.find x
+ let mem_type namespace s =
+ resolve_types ();
+ Types.mem (s, namespace)
+
let find_type namespace s =
resolve_types ();
Types.find (s, namespace)
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index c9866e785bfb78a40bbdb1777676d179c47a94c3..9e5293c20ff883cae5aebbac55abd97051e1e499 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -103,6 +103,20 @@ module Functions: sig
val get_params: kernel_function -> varinfo list
val get_vi: kernel_function -> varinfo
+ (** {2 Membership} *)
+
+ val mem_name: string -> bool
+ (** @return [true] iff there is a function with such a name
+ @since Frama-C+dev *)
+
+ val mem_def_name: string -> bool
+ (** @return [true] iff there is a function definition with such a name
+ @since Frama-C+dev *)
+
+ val mem_decl_name: string -> bool
+ (** @return [true] iff there is a function declaration with such a name
+ @since Frama-C+dev *)
+
(** {2 Searching} *)
val find_by_name : string -> kernel_function
@@ -219,10 +233,20 @@ module Types : sig
(** The two functions below are suitable for use in functor
{!Logic_typing.Make} *)
+ val mem_enum_tag: string -> bool
+ (** @return [true] iff there is an enum constant with the given name in the
+ AST.
+ @since Frama-C+dev *)
+
val find_enum_tag: string -> exp * typ
(** Find an enum constant from its name in the AST.
@raise Not_found when no such constant exists. *)
+ val mem_type: Logic_typing.type_namespace -> string -> bool
+ (** @return [true] iff there is a type with the given name in the given
+ namespace in the AST.
+ @since Frama-C+dev *)
+
val find_type: Logic_typing.type_namespace -> string -> typ
(** Find a type from its name in the AST.
@raise Not_found when no such type exists. *)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 441c1594ac728b5cbb08d757ac1ee7eaea8413fa..ea653a36c45d240f33ab4f23cefd7f791e13e4fb 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -168,6 +168,7 @@ module Status =
end)
let self = Status.self
+let () = Ast.add_monotonic_state self
let iter_on_statuses f ip =
try
@@ -231,6 +232,7 @@ end = struct
end)
let self = S.self
+ let () = Ast.add_monotonic_state self
let _mem e path =
try
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 9d0a42e6ebda2f54c326da5882d51ae0154901ce..f602bf07dcbe541966723f30099c0e4fd8d7cce7 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -526,8 +526,20 @@ module Value = struct
let add_formals_to_state = mk_fun "add_formals_to_state"
+ let get_fundec_from_stmt stmt =
+ let kf =
+ try
+ Kernel_function.find_englobing_kf stmt
+ with Not_found ->
+ Kernel.fatal "Unknown statement '%a'" Printer.pp_stmt stmt
+ in
+ try
+ Kernel_function.get_definition kf
+ with Kernel_function.No_Definition ->
+ Kernel.fatal "No definition for function %a" Kernel_function.pretty kf
+
let noassert_get_stmt_state ~after s =
- if !no_results (Kernel_function.(get_definition (find_englobing_kf s)))
+ if !no_results (get_fundec_from_stmt s)
then Cvalue.Model.top
else
let (find, add), find_by_callstack =
@@ -586,7 +598,7 @@ module Value = struct
exception Is_reachable
let is_reachable_stmt stmt =
- if !no_results (Kernel_function.(get_definition (find_englobing_kf stmt)))
+ if !no_results (get_fundec_from_stmt stmt)
then true
else
let ho = try Some (Table_By_Callstack.find stmt) with Not_found -> None in
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 936fc6f57fa40ce5d5602545bb8151cce84eb9a0..a44d27242911d78ca3342a8cac5779d96a85f5d7 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -44,6 +44,13 @@ SRC_LIBRARIES:= \
varname
SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))
+# project initializer
+SRC_PROJECT_INITIALIZER:= \
+ rtl \
+ prepare_ast
+SRC_PROJECT_INITIALIZER:=\
+ $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
+
# analyses
SRC_ANALYSES:= \
rte \
@@ -55,13 +62,6 @@ SRC_ANALYSES:= \
typing
SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
-# project initializer
-SRC_PROJECT_INITIALIZER:= \
- keep_status \
- prepare_ast
-SRC_PROJECT_INITIALIZER:=\
- $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
-
# code generator
SRC_CODE_GENERATOR:= \
constructor \
@@ -100,8 +100,8 @@ PLUGIN_NAME:=E_ACSL
PLUGIN_CMO:= src/local_config \
src/options \
$(SRC_LIBRARIES) \
- $(SRC_ANALYSES) \
$(SRC_PROJECT_INITIALIZER) \
+ $(SRC_ANALYSES) \
$(SRC_CODE_GENERATOR) \
src/main
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index ce93df0d9bec0532b42c14e7fb9742d785bcad18..caec156e2bce6ce838c1bb9d1c4957685e808264 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,11 @@
Plugin E-ACSL <next-release>
############################
+-* E-ACSL [2020-08-28] Fix crash that may occur when translating
+ properties that have been proved valid by another plug-in
+ (frama-c/e-acsl#106).
+-! E-ACSL [2020-08-28] Remove option -e-acsl-prepare-ast.
+-! E-ACSL [2020-08-28] Remove option -e-acsl-check.
- E-ACSL [2020-08-07] Add support for logical array comparison
(frama-c/e-acsl#99).
- E-ACSL [2020-07-28] Add support of bitwise operators
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 27d9be4791f802dbe9eebcb8cd3ed69c8cbe2139..63e742e131e03df9a6f38531c3b56c3ad2b18246 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -59,6 +59,25 @@
url = {publis/hdr.pdf}
}
+@inproceedings{kosmatov20rv,
+ author = {Kosmatov, Nikolai and Maurica, Fonenantsoa and Signoles, Julien},
+ title = {{Efficient Runtime Assertion Checking for Properties over
+ Mathematical Numbers}},
+ booktitle = {International Conference on Runtime Verification (RV)},
+ year = 2020,
+ month = oct,
+}
+
+@inproceedings{ly18hilt,
+ author = {Dara Ly and Nikolai Kosmatov and Fr\'ed\'eric Loulergue
+ and Julien Signoles},
+ title = {Soundness of a Dataflow Analysis for Memory Monitoring},
+ booktitle = {Workshop on Languages and Tools for Ensuring Cyber-Resilience in
+Critical Software-Intensive Systems (HILT)},
+ year = 2018,
+ month = nov,
+}
+
@inproceedings{rvcubes17tool,
author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index c69ab6038c6d344e0bbf612f2d171f4c96482979..034766eaca3e2ae51a6764834055cbb5dc55777e 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -5,6 +5,14 @@ release. First we list changes of the last release.
\section*{E-ACSL \eacslpluginversion}
+\begin{itemize}
+\item \textbf{Simple Example}: Remove option \texttt{-e-acsl-check}
+\item \textbf{Combining E-ACSL with Other PLug-ins}: \texttt{-e-acsl-prepare} is
+ no more necessary.
+\end{itemize}
+
+\section*{E-ACSL 19.0 Potassium}
+
\begin{itemize}
\item \textbf{Runtime Monitor Behavior}: Document global variable
\texttt{\_\_e\_acsl\_sound\_verdict} usable in \texttt{\_\_e\_acsl\_assert}.
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index ec0d86ba6c26d28e71a791c5268787dcd87b2908..c42ab93808d1fb2fbfb644ce3e4293bbeb443485 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -152,9 +152,6 @@ $f$ such that:
\end{itemize}
A violation of such an annotation $a$ is undetected. There is no workaround yet.
-Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
-undefined functions. There is also no workaround yet.
-
\subsection{Incomplete Types}
\index{Type!Incomplete}
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 172397d5d4013c43680dd271eb5b4d7420805874..f2f73c8229cab00bfd68472c81be15710c4f45ae 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -50,8 +50,9 @@ evolve in the future.
\section*{Acknowledgements}
We gratefully thank the people who contributed to this document:
-Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner, Nikola\"i Kosmatov,
-Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and Guillaume Petiot.
+Basile Desloges, Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner,
+Nikola\"i Kosmatov, Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and
+Guillaume Petiot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 18df5fe9d39c61acac7b65e4a931299f9e7f7c71..accd222ac1c299c54589bc2c69647b8855ab3ec6 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -416,7 +416,7 @@ script.
mathematical integers which does not fit in any integral \C type. To circumvent
this issue, \eacsl uses the \gmp library\footnote{\url{http://gmplib.org}}.
Thus, even if \eacsl does its best to use standard integral types instead of
-\gmp~\cite{sac13,jfla15}, it may generate such integers from time to time. It is
+\gmp~\cite{kosmatov20rv}, it may generate such integers from time to time. It is
notably the case if your program contains \lstinline|long long|, either signed
or unsigned.
@@ -544,8 +544,8 @@ model~\cite{pldi16}.
\subsubsection{Maximized Memory Tracking}
By default \eacsl uses static analysis to reduce instrumentation and therefore
-runtime and memory overheads~\cite{scp16}. With respect to memory tracking this
-means that
+runtime and memory overheads~\cite{ly18hilt}. With respect to memory tracking
+this means that
\eacsl may omit recording memory blocks irrelevant for runtime analysis. It
is, however, still possible to systematically instrument the code for handling
potential memory-related annotations even when it is not required. This
@@ -980,22 +980,6 @@ The present implementation of \eacslgcc does not fully support combining \eacsl
with other \framac plug-ins. However it is still possible to instrument programs
with \eacsl directly and use \eacslgcc to compile the generated code.
-If you run the \eacsl plug-in after another one, it first generates
-a new temporary project in which it links the analyzed program against its own
-library in order to generate the \framac internal representation of the \C
-program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
-even if the \eacsl plug-in keeps the maximum amount of information, the results
-of already executed analyzers (such as validity status of annotations) are not
-known in this new project.
-
-\begin{important}
-If you want to keep results of former analysis, you have to set the option
-\shortopt{e-acsl-prepare} when the first analysis is asked for. The standard
-example is running \eacsl after \Eva\index{Eva}: in such a case,
-\shortopt{e-acsl-prepare} must be provided together with the \Eva's
-\shortopt{val} option.
-\end{important}
-
In this context, the \eacsl plug-in does not generate code for annotations
proven valid by another plug-in, except if you explicitly set the option
\shortopt{e-acsl-valid}. For instance, \Eva~\cite{eva} is able to
@@ -1003,21 +987,14 @@ prove that there is no potential overflow in the previous program, so the \eacsl
plug-in does not generate additional code for checking them if you run the
following command.
\begin{shell}
-\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
+\$ frama-c -rte combine.i -then -val -then -e-acsl \
-then-last -print -ocode monitored_combine.i
\end{shell}
-The additional code will be generated with one of the two following commands.
+The additional code will be generated with the two following command.
\begin{shell}
-\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
- -e-acsl-valid -then-last -print -ocode monitored_combine.i
\$ frama-c -rte combine.i -then -val -then -e-acsl \
- -then-last -print -ocode monitored_combine.i
+ -e-acsl-valid -then-last -print -ocode monitored_combine.i
\end{shell}
-In the first case, that is because it is explicitly required by the option
-\shortopt{e-acsl-valid} while, in the second case, that is because the option
-\shortopt{e-acsl-prepare} is not provided on the command line which results in
-the fact that the result of the value analysis are unknown when the \eacsl
-plug-in is running.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1044,20 +1021,6 @@ check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
[e-acsl] translation done in project "foobar".
\end{shell}
-Further, the \eacsl plug-in option \shortopt{e-acsl-check} does not generate a
-new project but verifies that each annotation is translatable. Then it produces
-a summary as shown in the following example (left or right shifts in annotations
-are not yet supported by the \eacsl plug-in~\cite{eacsl-implem}).
-
-\begin{shell}
-\$ frama-c -e-acsl-check check.i
-<skip preprocessing commands>
-check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
- Ignoring annotation.
-[e-acsl] 0 annotation was ignored, being untypable.
-[e-acsl] 1 annotation was ignored, being unsupported.
-\end{shell}
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index ece261d80bc5f5feb371e6a88d13f8b1b3235fc4..41708b793a5ad7c2b97a1cf4fb703068e7457a1f 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -100,8 +100,8 @@ src/local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/main.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/options.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/options.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/project_initializer/rtl.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/project_initializer/rtl.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/project_initializer/prepare_ast.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/project_initializer/prepare_ast.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
tests/print.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index d4eb7bdfe5078af7e5664c03d0d13925f7e028b7..e4c6801d21f29c194931cca19852edad9f241f9f 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -206,8 +206,7 @@ executable found in the system path is used.
.TP
.B --then
separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual
-launch of the \fBE-ACSL\fP plugin. Prepends \fB-e-acsl-prepare\fP to the list
-of options passed to \fBFrama-C\fP.
+launch of the \fBE-ACSL\fP plugin.
.TP
.B --e-acsl-extra=\fI<OPTS>
add \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 3038810fbf9bd7f54a963b46de85a3d8c94c5129..c81e38218fb5c94dd3c75e247668f17b12f8e554 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -557,7 +557,6 @@ do
--then)
shift;
OPTION_THEN=-then
- FRAMAC_FLAGS="-e-acsl-prepare $FRAMAC_FLAGS"
;;
# Extra E-ACSL options
--e-acsl-extra)
@@ -754,7 +753,9 @@ CPPFLAGS="$OPTION_CPPFLAGS"
LDFLAGS="$OPTION_LDFLAGS"
# Extra Frama-C Flags E-ACSL needs
-FRAMAC_FLAGS="$FRAMAC_FLAGS -variadic-no-translation"
+FRAMAC_FLAGS="$FRAMAC_FLAGS \
+ -remove-unused-specified-functions \
+ -variadic-no-translation"
# C, CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT"
diff --git a/src/plugins/e-acsl/src/analyses/lscope.ml b/src/plugins/e-acsl/src/analyses/lscope.ml
index ccf0726b033dfa66f046a0593117e3f4de5f6525..56a9e7ff0fd4d13e4598f15b369e0333686ea6bd 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.ml
+++ b/src/plugins/e-acsl/src/analyses/lscope.ml
@@ -47,6 +47,8 @@ let exists lv t =
in
List.exists is_lv t
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+
exception Lscope_used
let is_used lscope pot =
let o = object inherit Visitor.frama_c_inplace
@@ -57,8 +59,14 @@ let is_used lscope pot =
in
try
(match pot with
- | Misc.PoT_pred p -> ignore (Visitor.visitFramacPredicate o p)
- | Misc.PoT_term t -> ignore (Visitor.visitFramacTerm o t));
+ | PoT_pred p -> ignore (Visitor.visitFramacPredicate o p)
+ | PoT_term t -> ignore (Visitor.visitFramacTerm o t));
false
with Lscope_used ->
true
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/analyses/lscope.mli b/src/plugins/e-acsl/src/analyses/lscope.mli
index f84968eeaa3926b0ca8cefff034d58659b81fc1b..56728c2bdd002181bb5c4a62743ab6cfaac7afd9 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.mli
+++ b/src/plugins/e-acsl/src/analyses/lscope.mli
@@ -48,6 +48,13 @@ val get_all: t -> lscope_var list
The first element is the first [lscope_var] that was added to [t], the
second element is the second [lscope_var] that was added to [t], an so on. *)
-val is_used: t -> Misc.pred_or_term -> bool
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+val is_used: t -> pred_or_term -> bool
(* [is_used lscope pot] returns [true] iff [pot] uses a variable from
[lscope]. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
index 3b655683995066f05739e1669e5e359c33ed4ddd..c480e318b764410dc8acfd272b8c28d27d3f75f6 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
@@ -27,7 +27,7 @@ module Dataflow = Dataflow2
let must_never_monitor vi =
(* E-ACSL, please do not monitor yourself! *)
- Functions.RTL.is_rtl_name vi.vname
+ Rtl.Symbols.mem_vi vi.vname
||
(* extern ghost variables are usually used (by the Frama-C libc) to
represent some internal invisible states in ACSL specifications. They do
@@ -620,7 +620,7 @@ end = struct
let compute init_set kf =
Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf;
- assert (not (Misc.is_library_loc (Kernel_function.get_location kf)));
+ assert (not (Rtl.Symbols.mem_kf kf));
let tbl, is_init =
try Env.find kf, true
with Not_found -> Stmt.Hashtbl.create 17, false
@@ -660,7 +660,7 @@ end = struct
tbl
let get ?init kf =
- if Misc.is_library_loc (Kernel_function.get_location kf) then
+ if Rtl.Symbols.mem_kf kf then
Varinfo.Hptset.empty
else
try
@@ -799,6 +799,6 @@ let use_model () =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli b/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
index 39090f0dfa07a4100864ff0c20883bd9d79e7f3a..8c4967c2797f9c936b3c230b40a9cb0d476f6a37 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
@@ -44,6 +44,6 @@ val must_model_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
(*
Local Variables:
- compile-command: "make"
+ compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/analyses/rte.ml b/src/plugins/e-acsl/src/analyses/rte.ml
index d02641f2bc68d2b157c557ea4ab5272b7fe4768d..96a1afbb988346ccc261a2181d097d949b370c8b 100644
--- a/src/plugins/e-acsl/src/analyses/rte.ml
+++ b/src/plugins/e-acsl/src/analyses/rte.ml
@@ -24,17 +24,6 @@
(** {2 Generic code} *)
(* ************************************************************************** *)
-let apply_rte f x =
- let signed = Kernel.SignedOverflow.get () in
- let unsigned = Kernel.UnsignedOverflow.get () in
- Kernel.SignedOverflow.off ();
- Kernel.UnsignedOverflow.off ();
- let finally () =
- Kernel.SignedOverflow.set signed;
- Kernel.UnsignedOverflow.set unsigned
- in
- Extlib.try_finally ~finally f x
-
let warn_rte warn exn =
if warn then
Options.warning "@[@[cannot run RTE:@ %s.@]@ \
@@ -48,30 +37,24 @@ Ignoring potential runtime errors in annotations."
open Cil_datatype
let stmt ?(warn=true) =
- try
- let f =
- Dynamic.get
- ~plugin:"RteGen"
- "stmt_annotations"
- (Datatype.func2 Kernel_function.ty Stmt.ty
- (let module L = Datatype.List(Code_annotation) in L.ty))
- in
- (fun x y -> apply_rte (f x) y)
+ try
+ Dynamic.get
+ ~plugin:"RteGen"
+ "stmt_annotations"
+ (Datatype.func2 Kernel_function.ty Stmt.ty
+ (let module L = Datatype.List(Code_annotation) in L.ty))
with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
->
warn_rte warn exn;
fun _ _ -> []
let exp ?(warn=true) =
- try
- let f =
- Dynamic.get
- ~plugin:"RteGen"
- "exp_annotations"
- (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty
- (let module L = Datatype.List(Code_annotation) in L.ty))
- in
- (fun x y z -> apply_rte (f x y) z)
+ try
+ Dynamic.get
+ ~plugin:"RteGen"
+ "exp_annotations"
+ (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty
+ (let module L = Datatype.List(Code_annotation) in L.ty))
with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
->
warn_rte warn exn;
@@ -79,6 +62,6 @@ let exp ?(warn=true) =
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/analyses/rte.mli b/src/plugins/e-acsl/src/analyses/rte.mli
index 96d971650079a343cd33cd699d52260720907fe7..6f177451eddc0de564679ef1dbb4e7c8f825e862 100644
--- a/src/plugins/e-acsl/src/analyses/rte.mli
+++ b/src/plugins/e-acsl/src/analyses/rte.mli
@@ -32,6 +32,6 @@ val exp: ?warn:bool -> kernel_function -> stmt -> exp -> code_annotation list
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index a2612ee906f2595622dd37a63cc835b93b44fd9f..04731a08f3ce28a805afc6e0a7f4c52d064976fd 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -512,7 +512,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| LBreads _ ->
Error.not_yet "logic functions performing read accesses"
| LBinductive _ ->
- Error.not_yet "logic functions inductively defined"
+ Error.not_yet "inductive logic functions"
end
| Tunion _ -> Error.not_yet "tset union"
@@ -585,8 +585,13 @@ let rec type_predicate p =
c_int
| LBnone -> (* Eg: \is_finite *)
Error.not_yet "predicate with no definition nor reads clause"
- | LBreads _ | LBterm _ | LBinductive _ ->
+ | LBreads _ ->
+ Error.not_yet "predicate performing read accesses"
+ | LBinductive _ ->
+ Error.not_yet "inductive predicate"
+ | LBterm _ ->
Options.fatal "unexpected logic definition"
+ Printer.pp_predicate p
end
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index 59a6acb5cf95cc7762a67ebbb5af99c854579eed..040c83991edcca505c5758fdf0ad4dea40420c12 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -225,9 +225,9 @@ let to_exp ~loc kf env pot label =
in
(* Creating the pointer *)
let ty = match pot with
- | Misc.PoT_pred _ ->
+ | Lscope.PoT_pred _ ->
Cil.intType
- | Misc.PoT_term t ->
+ | Lscope.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
Typing.get_typ t
@@ -289,7 +289,7 @@ let to_exp ~loc kf env pot label =
let term_to_exp = !term_to_exp_ref in
let named_predicate_to_exp = !predicate_to_exp_ref in
match pot with
- | Misc.PoT_pred p ->
+ | Lscope.PoT_pred p ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e, env = named_predicate_to_exp kf env p in
@@ -303,7 +303,7 @@ let to_exp ~loc kf env pot label =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Constructor.mk_block_stmt block ], env
- | Misc.PoT_term t ->
+ | Lscope.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
let env = Env.push env in
@@ -347,6 +347,6 @@ let to_exp ~loc kf env pot label =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
index 3b6dda222774a0cde05bdce183bc273ef75c4742..f5b51d739bd4de58a55583a2e68cd2f95696b87e 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
@@ -32,7 +32,7 @@ open Cil_datatype
val to_exp:
loc:Location.t -> kernel_function -> Env.t ->
- Misc.pred_or_term -> logic_label -> exp * Env.t
+ Lscope.pred_or_term -> logic_label -> exp * Env.t
(*****************************************************************************)
(**************************** Handling memory ********************************)
@@ -70,6 +70,6 @@ val term_to_exp_ref:
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 4848a1f2e2191770084af933d615f5326926c81c..a38f36ce70e425255853780dbbf358bef43cc0ab 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -98,7 +98,12 @@ let mk_block stmt b = match b.bstmts with
(* ********************************************************************** *)
let mk_lib_call ~loc ?result fname args =
- let vi = Misc.get_lib_fun_vi fname in
+ let vi =
+ try Rtl.Symbols.find_vi fname
+ with Rtl.Symbols.Unregistered _ as exn ->
+ try Builtins.find fname
+ with Not_found -> raise exn
+ in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
let make_args ~variadic args param_ty =
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index 731734839878fda808895f9a71e4fde5858f4d4c..d21c71e53a434f9905a89fc1ca49ab31df10a781 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -79,7 +79,7 @@ val mk_break: loc:location -> stmt
val mk_lib_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
(** Construct a call to a library function with the given name.
- @raise Unregistered_library_function if the given string does not represent
+ @raise Rtl.Symbols.Unregistered if the given string does not represent
such a function or if library functions were never registered (only possible
when using E-ACSL through its API). *)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index a0357a168fdf9772d83de8409e5734b3062a43da..dd1222051d790f8757da083c9f9628ac3be4d877 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -68,9 +68,9 @@ let inject_in_local_init loc env kf vi = function
when Options.Validate_format_strings.get ()
&& Functions.Libc.is_printf_name fvi.vname
->
- (* rewrite format functions (e.g., [printf]). *)
- let name = Functions.RTL.get_rtl_replacement_name fvi.vname in
- let new_vi = Misc.get_lib_fun_vi name in
+ (* rewrite libc function names (e.g., [printf]). *)
+ let name = Functions.RTL.libc_replacement_name fvi.vname in
+ let new_vi = try Builtins.find name with Not_found -> assert false in
let fmt = Functions.Libc.get_printf_argument_str ~loc fvi.vname args in
ConsInit(new_vi, fmt :: args, kind), env
@@ -80,7 +80,7 @@ let inject_in_local_init loc env kf vi = function
->
(* rewrite names of functions for which we have alternative definitions in
the RTL. *)
- fvi.vname <- Functions.RTL.get_rtl_replacement_name fvi.vname;
+ fvi.vname <- Functions.RTL.libc_replacement_name fvi.vname;
init, env
| AssignInit init ->
@@ -109,7 +109,7 @@ let rename_caller loc args exp = match exp.enode with
when Options.Replace_libc_functions.get ()
&& Functions.RTL.has_rtl_replacement vi.vname
->
- vi.vname <- Functions.RTL.get_rtl_replacement_name vi.vname;
+ vi.vname <- Functions.RTL.libc_replacement_name vi.vname;
exp, args
| Lval(Var vi, _)
@@ -120,12 +120,12 @@ let rename_caller loc args exp = match exp.enode with
from the above because argument list of format functions is extended with
an argument describing actual variadic arguments *)
(* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *)
- let name = Functions.RTL.get_rtl_replacement_name vi.vname in
+ let name = Functions.RTL.libc_replacement_name vi.vname in
(* variadic arguments descriptor *)
let fmt = Functions.Libc.get_printf_argument_str ~loc vi.vname args in
- (* get the name of the library function we need. Cannot just rewrite the
- name as AST check will then fail *)
- let vi = Misc.get_lib_fun_vi name in
+ (* get the library function we need. Cannot just rewrite the name as AST
+ check will then fail *)
+ let vi = try Rtl.Symbols.find_vi name with Not_found -> assert false in
Cil.evar vi, fmt :: args
| _ ->
@@ -232,7 +232,7 @@ let add_new_block_in_stmt env kf stmt =
in
let mk_post_env env stmt =
Annotations.fold_code_annot
- (fun _ a env -> Translate.translate_post_code_annotation kf env a)
+ (fun _ a env -> Translate.translate_post_code_annotation kf stmt env a)
stmt
env
in
@@ -252,7 +252,7 @@ let add_new_block_in_stmt env kf stmt =
let env = mk_post_env env stmt in
(* also handle the postcondition of the function and clear the
env *)
- Translate.translate_post_spec kf env (Annotations.funspec kf)
+ Translate.translate_post_spec kf Kglobal env (Annotations.funspec kf)
else
env
in
@@ -450,7 +450,7 @@ and inject_in_stmt env kf stmt =
(* translate the precondition of the function *)
if Functions.check kf then
let funspec = Annotations.funspec kf in
- Translate.translate_pre_spec kf env funspec
+ Translate.translate_pre_spec kf Kglobal env funspec
else env
else
env
@@ -459,7 +459,7 @@ and inject_in_stmt env kf stmt =
let env =
if Functions.check kf then
Annotations.fold_code_annot
- (fun _ a env -> Translate.translate_pre_code_annotation kf env a)
+ (fun _ a env -> Translate.translate_pre_code_annotation kf stmt env a)
stmt
env
else
@@ -589,6 +589,7 @@ let inject_in_fundec main fundec =
in
List.iter unghost_formal fundec.sformals;
(* update environments *)
+ (* TODO: do it only for built-ins *)
Builtins.update vi.vname vi;
(* track function addresses but the main function that is tracked internally
via RTL *)
@@ -628,17 +629,15 @@ let unghost_vi vi =
let inject_in_global (env, main) = function
(* library functions and built-ins *)
| GVarDecl(vi, _) | GVar(vi, _, _)
- | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
- when Misc.is_library_loc vi.vdecl || Builtins.mem vi.vname ->
- Misc.register_library_function vi;
- if Builtins.mem vi.vname then Builtins.update vi.vname vi;
+ | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
+ Builtins.update vi.vname vi;
env, main
(* Cil built-ins and other library globals: nothing to do *)
| GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
when Misc.is_fc_or_compiler_builtin vi ->
env, main
- | g when Misc.is_library_loc (Global.loc g) ->
+ | g when Rtl.Symbols.mem_global g ->
env, main
(* variable declarations *)
@@ -845,7 +844,6 @@ let reset_all ast =
Options.Run.off ();
(* reset all the E-ACSL environments to their original states *)
Mmodel_analysis.reset ();
- Misc.reset ();
Logic_functions.reset ();
Literal_strings.reset ();
Global_observer.reset ();
@@ -862,8 +860,6 @@ let inject () =
Options.feedback ~level:2
"injecting annotations as code in project %a"
Project.pretty (Project.current ());
- Keep_status.before_translation ();
- Misc.reorder_ast ();
Gmp_types.init ();
let ast = Ast.get () in
inject_in_file ast;
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index b9dfc2390c42fb5519843333f0fb83f8b0bc2c0d..009763c7931d6f8d47f548698052917a7551ed21 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -686,7 +686,7 @@ and context_insensitive_term_to_exp kf env t =
e, env, C_number, ""
| Tat(t', label) ->
let lscope = Env.Logic_scope.get env in
- let pot = Misc.PoT_term t' in
+ let pot = Lscope.PoT_term t' in
if Lscope.is_used lscope pot then
let e, env = At_with_lscope.to_exp ~loc kf env pot label in
e, env, C_number, ""
@@ -947,7 +947,7 @@ and named_predicate_content_to_exp ?name kf env p =
named_predicate_to_exp kf env p
| Pat(p', label) ->
let lscope = Env.Logic_scope.get env in
- let pot = Misc.PoT_pred p' in
+ let pot = Lscope.PoT_pred p' in
if Lscope.is_used lscope pot then
At_with_lscope.to_exp ~loc kf env pot label
else begin
@@ -1128,19 +1128,35 @@ let term_to_exp typ t =
let env = Env.rte env false in
let e, env =
try term_to_exp (Kernel_function.dummy ()) env t
- with Misc.Unregistered_library_function _ -> raise (No_simple_translation t)
+ with Rtl.Symbols.Unregistered _ -> raise (No_simple_translation t)
in
if not (Env.has_no_new_stmt env) then raise (No_simple_translation t);
e
(* ************************************************************************** *)
(* [translate_*] translates a given ACSL annotation into the corresponding C
- statement (if any) for runtime assertion checking.
-
- IMPORTANT: the order of translation of pre-/post-spec must be consistent with
- the pushes done in [Keep_status] *)
+ statement (if any) for runtime assertion checking. *)
(* ************************************************************************** *)
+let must_translate ppt =
+ Options.Valid.get ()
+ || match Property_status.get ppt with
+ | Never_tried
+ | Inconsistent _
+ | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
+ true
+ | Best (True, _) ->
+ (* [TODO] generating code for "valid under hypotheses" properties could be
+ useful for some use cases (in particular, when E-ACSL does not stop on
+ the very first error).
+ ==> introduce a new option or modify the behavior of -e-acsl-valid,
+ see e-acsl#35 *)
+ false
+
+let must_translate_opt = function
+ | None -> false
+ | Some ppt -> must_translate ppt
+
let assumes_predicate bhv =
List.fold_left
(fun acc p ->
@@ -1151,14 +1167,14 @@ let assumes_predicate bhv =
Logic_const.ptrue
bhv.b_assumes
-let translate_preconditions kf env behaviors =
+let translate_preconditions kf kinstr env behaviors =
let env = Env.set_annotation_kind env Constructor.Precondition in
let do_behavior env b =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env p ->
let do_it env =
- if Keep_status.must_translate kf Keep_status.K_Requires then
+ if must_translate (Property.ip_of_requires kf kinstr b p) then
let loc = p.ip_content.pred_loc in
let p =
Logic_const.pimplies
@@ -1176,16 +1192,16 @@ let translate_preconditions kf env behaviors =
in
List.fold_left do_behavior env behaviors
-let translate_postconditions kf env behaviors =
+let translate_postconditions kf kinstr env behaviors =
let env = Env.set_annotation_kind env Constructor.Postcondition in
(* generate one guard by postcondition of each behavior *)
let do_behavior env b =
let env =
handle_error
(fun env ->
- (* test ordering does matter for keeping statuses consistent *)
- if b.b_assigns <> WritesAny
- && Keep_status.must_translate kf Keep_status.K_Assigns
+ let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
+ let ppt = Property.ip_assigns_of_behavior kf kinstr ~active b in
+ if b.b_assigns <> WritesAny && must_translate_opt ppt
then not_yet env "assigns clause in behavior";
(* ignore b.b_extended since we never translate them *)
env)
@@ -1193,8 +1209,8 @@ let translate_postconditions kf env behaviors =
in
let assumes_pred = assumes_predicate b in
List.fold_left
- (fun env (t, p) ->
- if Keep_status.must_translate kf Keep_status.K_Ensures then
+ (fun env ((t, p) as tp) ->
+ if must_translate (Property.ip_of_ensures kf kinstr b tp) then
let do_it env =
match t with
| Normal ->
@@ -1221,56 +1237,53 @@ let translate_postconditions kf env behaviors =
in
List.fold_left do_behavior env bhvs
-let translate_pre_spec kf env spec =
+let translate_pre_spec kf kinstr env spec =
let unsupported f x = ignore (handle_error (fun env -> f x; env) env) in
let convert_unsupported_clauses env =
unsupported
- (Extlib.may
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Decreases then
- not_yet env "variant clause"))
- spec.spec_variant;
+ (fun spec ->
+ let ppt = Property.ip_decreases_of_spec kf kinstr spec in
+ if must_translate_opt ppt then not_yet env "variant clause")
+ spec;
(* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
unsupported
- (Extlib.may
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Terminates then
- not_yet env "terminates clause"))
- spec.spec_terminates;
- (match spec.spec_complete_behaviors with
- | [] -> ()
- | l ->
- unsupported
- (List.iter
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Complete then
- not_yet env "complete behaviors"))
- l);
- (match spec.spec_disjoint_behaviors with
- | [] -> ()
- | l ->
- unsupported
- (List.iter
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Disjoint then
- not_yet env "disjoint behaviors"))
- l);
+ (fun spec ->
+ let ppt = Property.ip_terminates_of_spec kf kinstr spec in
+ if must_translate_opt ppt then not_yet env "terminates clause")
+ spec;
+ let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
+ let ppts = Property.ip_complete_of_spec kf kinstr ~active spec in
+ unsupported
+ (fun ppts ->
+ List.iter
+ (fun ppt ->
+ if must_translate ppt then not_yet env "complete behaviors")
+ ppts)
+ ppts;
+ let ppts = Property.ip_disjoint_of_spec kf kinstr ~active spec in
+ unsupported
+ (fun ppts ->
+ List.iter
+ (fun ppt ->
+ if must_translate ppt then not_yet env "disjoint behaviors")
+ ppts)
+ ppts;
env
in
let env = convert_unsupported_clauses env in
handle_error
- (fun env -> translate_preconditions kf env spec.spec_behavior)
+ (fun env -> translate_preconditions kf kinstr env spec.spec_behavior)
env
-let translate_post_spec kf env spec =
+let translate_post_spec kf kinstr env spec =
handle_error
- (fun env -> translate_postconditions kf env spec.spec_behavior)
+ (fun env -> translate_postconditions kf kinstr env spec.spec_behavior)
env
-let translate_pre_code_annotation kf env annot =
+let translate_pre_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
| AAssert(l, _, p) ->
- if Keep_status.must_translate kf Keep_status.K_Assert then
+ if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
let env = Env.set_annotation_kind env Constructor.Assertion in
if l <> [] then
not_yet env "@[assertion applied only on some behaviors@]";
@@ -1280,9 +1293,9 @@ let translate_pre_code_annotation kf env annot =
| AStmtSpec(l, spec) ->
if l <> [] then
not_yet env "@[statement contract applied only on some behaviors@]";
- translate_pre_spec kf env spec ;
+ translate_pre_spec kf (Kstmt stmt) env spec ;
| AInvariant(l, loop_invariant, p) ->
- if Keep_status.must_translate kf Keep_status.K_Invariant then
+ if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
let env = Env.set_annotation_kind env Constructor.Invariant in
if l <> [] then
not_yet env "@[invariant applied only on some behaviors@]";
@@ -1291,26 +1304,31 @@ let translate_pre_code_annotation kf env annot =
else
env
| AVariant _ ->
- if Keep_status.must_translate kf Keep_status.K_Variant
+ if must_translate (Property.ip_of_code_annot_single kf stmt annot)
then not_yet env "variant"
else env
| AAssigns _ ->
- (* TODO: it is not a precondition *)
- if Keep_status.must_translate kf Keep_status.K_Assigns
- then not_yet env "assigns"
- else env
+ (* TODO: it is not a precondition --> should not be handled here,
+ to be fixed when implementing e-acsl#29 *)
+ let ppts = Property.ip_of_code_annot kf stmt annot in
+ List.iter
+ (fun ppt -> if must_translate ppt then not_yet env "assigns")
+ ppts;
+ env
| AAllocation _ ->
- if Keep_status.must_translate kf Keep_status.K_Allocation
- then not_yet env "allocation"
- else env
+ let ppts = Property.ip_of_code_annot kf stmt annot in
+ List.iter
+ (fun ppt -> if must_translate ppt then not_yet env "allocation")
+ ppts;
+ env
| APragma _ -> not_yet env "pragma"
| AExtended _ -> env (* never translate extensions. *)
in
handle_error convert env
-let translate_post_code_annotation kf env annot =
+let translate_post_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
- | AStmtSpec(_, spec) -> translate_post_spec kf env spec
+ | AStmtSpec(_, spec) -> translate_post_spec kf (Kstmt stmt) env spec
| AAssert _
| AInvariant _
| AVariant _
diff --git a/src/plugins/e-acsl/src/code_generator/translate.mli b/src/plugins/e-acsl/src/code_generator/translate.mli
index b38599d54403b537afbb1dec5277430e3b4d0a6c..64a83c76113bbe3e29142f4d4d6981e74ae81d00 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate.mli
@@ -26,12 +26,12 @@ open Cil_types
statement (if any) for runtime assertion checking. This C statements are
part of the resulting environment. *)
-val translate_pre_spec: kernel_function -> Env.t -> funspec -> Env.t
-val translate_post_spec: kernel_function -> Env.t -> funspec -> Env.t
+val translate_pre_spec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
+val translate_post_spec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
val translate_pre_code_annotation:
- kernel_function -> Env.t -> code_annotation -> Env.t
+ kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
val translate_post_code_annotation:
- kernel_function -> Env.t -> code_annotation -> Env.t
+ kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
val translate_named_predicate:
kernel_function -> Env.t -> predicate -> Env.t
@@ -50,6 +50,6 @@ val predicate_to_exp: kernel_function -> predicate -> exp
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/libraries/builtins.ml b/src/plugins/e-acsl/src/libraries/builtins.ml
index 9bfe9fe7d7bf79638487c00e265ee2a35b533a79..fa5d9adf70ae5c12f251f9ba96bbcea4bc56558c 100644
--- a/src/plugins/e-acsl/src/libraries/builtins.ml
+++ b/src/plugins/e-acsl/src/libraries/builtins.ml
@@ -83,6 +83,6 @@ let () = Cmdline.run_after_configuring_stage init
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/libraries/builtins.mli b/src/plugins/e-acsl/src/libraries/builtins.mli
index 95dce5b8aab5bc88615f90a2274bccc9b79d521c..d15f53f6ef5284904b9f4c709a95cb78e7c6d5fc 100644
--- a/src/plugins/e-acsl/src/libraries/builtins.mli
+++ b/src/plugins/e-acsl/src/libraries/builtins.mli
@@ -35,6 +35,6 @@ val update: string -> Cil_types.varinfo -> unit
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml
index b939bcff401d0ea330544988bf4e96d8c43e0c02..37cf8f8319f67d966635e0704b8ed32bd6a5f91e 100644
--- a/src/plugins/e-acsl/src/libraries/functions.ml
+++ b/src/plugins/e-acsl/src/libraries/functions.ml
@@ -92,12 +92,10 @@ module RTL = struct
let is_generated_kf kf =
is_generated_name (Kernel_function.get_name kf)
- let is_rtl_name name = startswith e_acsl_api_prefix name
-
let is_generated_literal_string_name name =
startswith e_acsl_lit_string_prefix name
- let get_rtl_replacement_name fn = e_acsl_builtin_prefix ^ fn
+ let libc_replacement_name fn = e_acsl_builtin_prefix ^ fn
let has_rtl_replacement = function
| "strcpy" | "strncpy" | "strlen" | "strcat" | "strncat" | "strcmp"
diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli
index a99291b585ff361c53aafa6450d5f06da1ea33bc..4963870c28539b1b89d055be1bb0285158b71366 100644
--- a/src/plugins/e-acsl/src/libraries/functions.mli
+++ b/src/plugins/e-acsl/src/libraries/functions.mli
@@ -59,10 +59,6 @@ module RTL: sig
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_name] but for kernel functions *)
- val is_rtl_name: string -> bool
- (** @return [true] if the prefix of the given name indicates that it
- belongs to the public API of the E-ACSL Runtime Library *)
-
val is_generated_literal_string_name: string -> bool
(** Same as [is_generated_name] but indicates that the name represents a local
variable that replaced a literal string. *)
@@ -71,7 +67,7 @@ module RTL: sig
(** Retrieve the name of the kernel function and strip prefix that indicates
that it has been generated by the instrumentation. *)
- val get_rtl_replacement_name: string -> string
+ val libc_replacement_name: string -> string
(** Given the name of C library function return the name of the RTL function
that potentially replaces it. *)
@@ -178,3 +174,9 @@ module Libc: sig
In GCC/Clang [alloca] is typically implemented via [__builtin_alloca] *)
end (* Libc *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 0f4d38ef3fb6f37bd2ab33dd37c1f0d1ff021063..0b2cd0d3ad79f9a6f08f442da392e7013fd38041 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-module RTL = Functions.RTL
open Cil_types
open Cil_datatype
@@ -28,20 +27,6 @@ open Cil_datatype
(** {2 Handling the E-ACSL's C-libraries, part I} *)
(* ************************************************************************** *)
-let library_files () =
- List.map
- (fun d -> Options.Share.get_file ~mode:`Must_exist d)
- [ "e_acsl_gmp_api.h";
- "e_acsl.h" ]
-
-let is_library_loc (loc, _) = List.mem loc.Filepath.pos_path (library_files ())
-
-let library_functions = Datatype.String.Hashtbl.create 17
-let register_library_function vi =
- Datatype.String.Hashtbl.add library_functions vi.vname vi
-
-let reset () = Datatype.String.Hashtbl.clear library_functions
-
let is_fc_or_compiler_builtin vi =
Cil.is_builtin vi
||
@@ -51,20 +36,6 @@ let is_fc_or_compiler_builtin vi =
let prefix = String.sub vi.vname 0 prefix_length in
Datatype.String.equal prefix "__builtin_")
-(* ************************************************************************** *)
-(** {2 Builders} *)
-(* ************************************************************************** *)
-
-exception Unregistered_library_function of string
-let get_lib_fun_vi fname =
- try Datatype.String.Hashtbl.find library_functions fname
- with Not_found ->
- try Builtins.find fname
- with Not_found ->
- (* should not happen in normal mode, but could be raised when E-ACSL is
- used as a library *)
- raise (Unregistered_library_function fname)
-
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
@@ -89,17 +60,6 @@ let result_vi kf = match result_lhost kf with
let term_addr_of ~loc tlv ty =
Logic_const.taddrof ~loc tlv (Ctype (TPtr(ty, [])))
-let reorder_ast () =
- let ast = Ast.get() in
- let is_from_library = function
- | GType(ti, _) when ti.tname = "size_t" || ti.tname = "FILE"
- || RTL.is_rtl_name ti.tname -> true
- | GCompTag (ci, _) when RTL.is_rtl_name ci.cname -> true
- | GFunDecl(_, _, loc) | GVarDecl(_, loc) when is_library_loc loc -> true
- | _ -> false in
- let rtl, other = List.partition is_from_library ast.globals in
- ast.globals <- rtl @ other
-
let cty = function
| Ctype ty -> ty
| lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
@@ -186,8 +146,6 @@ let term_has_lv_from_vi t =
with Lv_from_vi_found ->
true
-type pred_or_term = PoT_pred of predicate | PoT_term of term
-
let mk_ptr_sizeof typ loc =
match Cil.unrollType typ with
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 1d2359202f752f482e32557377726c0719f23d3f..f9c92c19e8097a872a37edc83fa83301a79dd645 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -24,14 +24,6 @@
open Cil_types
-(* ************************************************************************** *)
-(** {2 Builders} *)
-(* ************************************************************************** *)
-
-exception Unregistered_library_function of string
-val get_lib_fun_vi: string -> varinfo
-(** @return varinfo corresponding to a name of a given library function *)
-
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
@@ -43,27 +35,13 @@ val result_vi: kernel_function -> varinfo
(** @return the varinfo corresponding to \result in the given function *)
(* ************************************************************************** *)
-(** {2 Handling the E-ACSL's C-libraries} *)
+(** {2 Other stuff} *)
(* ************************************************************************** *)
-val library_files: unit -> Datatype.Filepath.t list
-val is_library_loc: location -> bool
-val register_library_function: varinfo -> unit
-val reset: unit -> unit
-
val is_fc_or_compiler_builtin: varinfo -> bool
-(* ************************************************************************** *)
-(** {2 Other stuff} *)
-(* ************************************************************************** *)
-
val term_addr_of: loc:location -> term_lval -> typ -> term
-val reorder_ast: unit -> unit
-(* Reorder current AST by bringing all global declarations belonging to the
- * E-ACSL runtime library and their dependencies (e.g., typedef size_t) to
- * the very top of the file. *)
-
val cty: logic_type -> typ
(** Assume that the logic type is indeed a C type. Just return it. *)
@@ -90,8 +68,6 @@ val term_has_lv_from_vi: term -> bool
(** @return true iff the given term contains a variables that originates from
a C varinfo, that is a non-purely logic variable. *)
-type pred_or_term = PoT_pred of predicate | PoT_term of term
-
val mk_ptr_sizeof: typ -> location -> exp
(** [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
to a [typ] typ and returns [sizeof(typ)]. *)
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 0c6c931c4754a04db314b86e69710985c304155f..703ef6b8c0d8d8d7e6683ebf4a88a48c84c572ce 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -20,101 +20,6 @@
(* *)
(**************************************************************************)
-let check () = assert false (* [TODO ARCHI] kill check *)
-
-let check =
- Dynamic.register
- ~plugin:"e-acsl"
- ~journalize:true
- "check"
- (Datatype.func Datatype.unit Datatype.bool)
- check
-
-type extended_project =
- | To_be_extended
- | Already_extended of Project.t option (* None = keep the current project *)
-
-let extended_ast_project: extended_project ref = ref To_be_extended
-
-let unmemoized_extend_ast () =
- let extend () =
- let share = Options.Share.get_dir ~mode:`Must_exist "." in
- Options.feedback ~level:3 "setting kernel options for E-ACSL.";
- Kernel.CppExtraArgs.add
- (Format.asprintf " -DE_ACSL_MACHDEP=%s -I%a/memory_model"
- (Kernel.Machdep.get ())
- Datatype.Filepath.pp_abs share);
- Kernel.Keep_unused_specified_functions.off ();
- if Plugin.is_present "variadic" then
- Dynamic.Parameter.Bool.off "-variadic-translation" ();
- let ppc, ppk = File.get_preprocessor_command () in
- let register s =
- File.pre_register
- (File.NeedCPP
- (s,
- ppc
- ^ Format.asprintf " -I%a" Datatype.Filepath.pp_abs share,
- ppk))
- in
- List.iter register (Misc.library_files ())
- in
- if Ast.is_computed () then begin
- (* do not modify the existing project: work on a copy.
- Must also extend the current AST with the E-ACSL's library files. *)
- Options.feedback ~level:2
- "AST already computed: E-ACSL is going to work on a copy.";
- let name = Project.get_name (Project.current ()) in
- let tmpfile =
- Extlib.temp_file_cleanup_at_exit ("e_acsl_" ^ name) ".i" in
- let cout = open_out tmpfile in
- let fmt = Format.formatter_of_out_channel cout in
- File.pretty_ast ~fmt ();
- let selection =
- State_selection.diff
- State_selection.full
- (State_selection.with_dependencies Ast.self)
- in
- let prj =
- Project.create_by_copy
- ~last:false
- ~selection
- (Format.asprintf "%s for E-ACSL" name)
- in
- Project.on prj
- (fun () ->
- Kernel.Files.set [ Datatype.Filepath.of_string tmpfile ];
- extend ())
- ();
- Some prj
- end else begin
- extend ();
- None
- end
-
-let extend_ast () = match !extended_ast_project with
- | To_be_extended ->
- let prj = unmemoized_extend_ast () in
- extended_ast_project := Already_extended prj;
- (match prj with
- | None -> Project.current ()
- | Some prj -> prj)
- | Already_extended None ->
- Project.current ()
- | Already_extended(Some prj) ->
- prj
-
-let apply_on_e_acsl_ast f x =
- let tmp_prj = extend_ast () in
- let res = Project.on tmp_prj f x in
- (match !extended_ast_project with
- | To_be_extended -> assert false
- | Already_extended None -> ()
- | Already_extended (Some prj) ->
- assert (Project.equal prj tmp_prj);
- extended_ast_project := To_be_extended;
- if Options.Debug.get () = 0 then Project.remove ~project:tmp_prj ());
- res
-
module Resulting_projects =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
@@ -133,32 +38,65 @@ let () =
let generate_code =
Resulting_projects.memo
(fun name ->
- apply_on_e_acsl_ast
+ Options.feedback "beginning translation.";
+ Temporal.enable (Options.Temporal_validity.get ());
+ if Plugin.is_present "variadic" then begin
+ let opt_name = "-variadic-translation" in
+ if Dynamic.Parameter.Bool.get opt_name () then begin
+ if Ast.is_computed () then
+ Options.abort
+ "The variadic translation must be turned off for E-ACSL. \
+ Please use option '-variadic-no-translation'";
+ Options.warning "deactivating variadic translation";
+ Dynamic.Parameter.Bool.off opt_name ();
+ end
+ end;
+ (* slightly more efficient to copy the project before computing the AST
+ if it is not yet computed *)
+ let rtl_prj_name = Options.Project_name.get () ^ " RTL" in
+ let rtl_prj = Project.create_by_copy ~last:false rtl_prj_name in
+ (* force AST computation before copying the project it belongs to *)
+ Ast.compute ();
+ let copied_prj = Project.create_by_copy ~last:true name in
+ Project.on
+ copied_prj
(fun () ->
- Options.feedback "beginning translation.";
- Temporal.enable (Options.Temporal_validity.get ());
- let copied_prj =
- Project.create_by_copy name ~last:true
+ (* preparation of the AST does not concern the E-ACSL RTL:
+ do it first *)
+ Prepare_ast.prepare ();
+ Rtl.link rtl_prj;
+ (* the E-ACSL type system ensures the soundness of the generated
+ arithmetic operations. Therefore, deactivate the corresponding
+ options in order to prevent RTE to generate spurious alarms. *)
+ let signed = Kernel.SignedOverflow.get () in
+ let unsigned = Kernel.UnsignedOverflow.get () in
+ (* we do know that setting these flags does not modify the program's
+ semantics: using their unsafe variants is thus safe and preserve
+ all emitted property statuses. *)
+ Kernel.SignedOverflow.unsafe_set false;
+ Kernel.UnsignedOverflow.unsafe_set false;
+ let finally () =
+ Kernel.SignedOverflow.unsafe_set signed;
+ Kernel.UnsignedOverflow.unsafe_set unsigned
+ in
+ Extlib.try_finally ~finally Injector.inject ();
+ (* remove the RTE's results computed from E-ACSL: they are partial
+ and associated with the wrong kernel function (the one of the old
+ project). *)
+ (* [TODO] what if RTE was already computed? To be fixed when
+ redoing the RTE management system *)
+ let selection =
+ State_selection.union
+ (State_selection.with_dependencies !Db.RteGen.self)
+ (State_selection.with_dependencies Options.Run.self)
in
- Project.on
- copied_prj
- (fun () ->
- Prepare_ast.prepare ();
- Injector.inject ();
- (* remove the RTE's results computed from E-ACSL: they are
- partial and associated with the wrong kernel function (the
- one of the old project). *)
- (* [TODO ARCHI] what if RTE was already computed? *)
- let selection =
- State_selection.with_dependencies !Db.RteGen.self
- in
- Project.clear ~selection ~project:copied_prj ();
- Resulting_projects.mark_as_computed ())
- ();
- Options.feedback "translation done in project \"%s\"."
- (Options.Project_name.get ());
- copied_prj)
- ())
+ Project.clear ~selection ~project:copied_prj ();
+ Resulting_projects.mark_as_computed ())
+ ();
+ if not (Options.debug_atleast 1) then Project.remove ~project:rtl_prj ();
+ Options.feedback "translation done in project \"%s\"."
+ (Options.Project_name.get ());
+ copied_prj)
let generate_code =
Dynamic.register
@@ -177,15 +115,6 @@ let predicate_to_exp =
Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
Translate.predicate_to_exp
-let add_e_acsl_library _files =
- if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
-
-(* extending the AST as soon as possible reduce the amount of time the AST is
- duplicated:
- - that is faster
- - locations are better (indicate an existing file, and not a temp file) *)
-let () = Cmdline.run_after_configuring_stage add_e_acsl_library
-
(* The Frama-C standard library contains specific built-in variables prefixed by
"__fc_" and declared as extern: they prevent the generated code to be
linked. This modification of the default printer replaces them by their
@@ -248,17 +177,10 @@ let change_printer =
end
let main () =
- Keep_status.clear ();
if Options.Run.get () then begin
change_printer ();
- ignore (generate_code (Options.Project_name.get ()))
- end else
- if Options.Check.get () then
- apply_on_e_acsl_ast
- (fun () ->
- Gmp_types.init ();
- ignore (check ()))
- ()
+ ignore (generate_code (Options.Project_name.get ()));
+ end
let () = Db.Main.extend main
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index da21806929227ab689d12a3f31fcd40632a80445..8c98ca1657933ca519eef73fa5697877efa50842 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -31,13 +31,6 @@ module P = Plugin.Register
module PP = P (* [PP] required to avoid an ocamldoc error in OCaml 4.02 *)
include PP
-module Check =
- False
- (struct
- let option_name = "-e-acsl-check"
- let help = "only type check E-ACSL annotated program"
- end)
-
module Run =
False
(struct
@@ -63,13 +56,6 @@ module Valid =
let help = "translate annotation which have been proven valid"
end)
-module Prepare =
- False
- (struct
- let option_name = "-e-acsl-prepare"
- let help = "prepare the AST to be directly usable by E-ACSL"
- end)
-
module Gmp_only =
False
(struct
@@ -163,7 +149,9 @@ let parameter_states =
Functions.self;
Instrument.self ]
-let must_visit () = Run.get () || Check.get ()
+let emitter = Emitter.create "E-ACSL" [ Funspec ] ~correctness:[] ~tuning:[]
+
+let must_visit () = Run.get ()
let dkey_analysis = register_category "analysis"
let dkey_prepare = register_category "preparation"
@@ -172,6 +160,6 @@ let dkey_typing = register_category "typing"
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index 8e8114594f8b8da0f1dac3d204fef317ac144a57..d5065c6a51dbbade2b491b5cf91fea75d17e7f23 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -22,10 +22,8 @@
include Plugin.S (** implementation of Log.S for E-ACSL *)
-module Check: Parameter_sig.Bool
module Run: Parameter_sig.Bool
module Valid: Parameter_sig.Bool
-module Prepare: Parameter_sig.Bool
module Gmp_only: Parameter_sig.Bool
module Full_mmodel: Parameter_sig.Bool
module Project_name: Parameter_sig.String
@@ -38,6 +36,7 @@ module Functions: Parameter_sig.Kernel_function_set
module Instrument: Parameter_sig.Kernel_function_set
val parameter_states: State.t list
+val emitter: Emitter.t
val must_visit: unit -> bool
@@ -48,6 +47,6 @@ val dkey_typing: category
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/project_initializer/keep_status.ml b/src/plugins/e-acsl/src/project_initializer/keep_status.ml
deleted file mode 100644
index f4b83a501b0900b1e0599e48031a3a0f033a82b9..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/project_initializer/keep_status.ml
+++ /dev/null
@@ -1,162 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-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). *)
-(* *)
-(**************************************************************************)
-
-(* E-ACSL needs to access to the property status of every property (in
- particular for the option -e-acsl-valid). However, the necessary elements for
- building a property are copied/modified several times from the original
- project to the final project and the property statuses are destroyed when
- creating the intermediate projects; so there is no easy way to access to
- property statuses from the final project.
-
- This module aims at solving this issue by providing an access to property
- statuses from the final project. To work properly, it requires to visit every
- property during the final visit in the very same order than during the AST
- preparation visit. Indeed, for each function, it associates to each
- property an unique integer corresponding to its visit ordering. *)
-
-(* the kind is only used for a few additional consistency checks between [push]
- and [must_translate]*)
-type kind =
- | K_Assert
- | K_Invariant
- | K_Variant
- | K_StmtSpec
- | K_Allocation
- | K_Assigns
- | K_Decreases
- | K_Terminates
- | K_Complete
- | K_Disjoint
- | K_Requires
- | K_Ensures
-
-let pretty_kind fmt k =
- Format.fprintf fmt "%s"
- (match k with
- | K_Assert -> "assert"
- | K_Invariant -> "invariant"
- | K_Variant -> "variant"
- | K_StmtSpec -> "stmtspec"
- | K_Allocation -> "allocation"
- | K_Assigns -> "assigns"
- | K_Decreases -> "decreases"
- | K_Terminates -> "terminates"
- | K_Complete -> "complete"
- | K_Disjoint -> "disjoint"
- | K_Requires -> "requires"
- | K_Ensures -> "ensures")
-
-(* information attached to every kernel_function containing an annotation *)
-type kf_info =
- { mutable cpt: int
- (* counter building the relationship between [push] and [must_translate] *);
- mutable statuses: (kind * bool) Datatype.Int.Map.t
- (* map associating a property as an integer to its kind and status
- ([true] = proved) *) }
-
-(* statuses for each function represented by its name (because the [kf] itself
- changes from a project to another). *)
-let keep_status
- : kf_info Datatype.String.Hashtbl.t
- = Datatype.String.Hashtbl.create 17
-
-(* will contain the value of a few options from the original project
- in order to safely use them from the final project. *)
-let option_valid = ref false
-let option_check = ref false
-
-let clear () =
- Datatype.String.Hashtbl.clear keep_status;
- option_valid := Options.Valid.get ();
- option_check := Options.Check.get ()
-
-let push kf kind ppt =
- (* Options.feedback "PUSHING %a for %a"
- pretty_kind kind
- Kernel_function.pretty kf;*)
- (* no registration when -e-acsl-check or -e-acsl-valid *)
- if not (!option_check || !option_valid) then
- let keep =
- let open Property_status in
- match get ppt with
- | Never_tried
- | Inconsistent _
- | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
- true
- | Best (True, _) ->
- false
- in
- let status = kind, keep in
- let name = Kernel_function.get_name kf in
- try
- let info = Datatype.String.Hashtbl.find keep_status name in
- info.cpt <- info.cpt + 1;
- info.statuses <- Datatype.Int.Map.add info.cpt status info.statuses
- with Not_found ->
- let info = { cpt = 1; statuses = Datatype.Int.Map.singleton 1 status } in
- Datatype.String.Hashtbl.add keep_status name info
-
-let before_translation () =
- (* reset all counters *)
- Datatype.String.Hashtbl.iter (fun _ info -> info.cpt <- 0) keep_status
-
-let must_translate kf kind =
- (* Options.feedback "GETTING %a for %a"
- pretty_kind kind
- Kernel_function.pretty kf;*)
- !option_check
- ||
- !option_valid
- ||
- (* function contracts have been moved from the original function to its
- duplicate by [Dup_function] but they are still associated to the original
- function here *)
- let name = Functions.RTL.get_original_name kf in
- try
- let info =
- try Datatype.String.Hashtbl.find keep_status name
- with Not_found ->
- Options.fatal "[keep_status] unbound function" Datatype.String.pretty kf
- in
- info.cpt <- info.cpt + 1;
- let kind', keep =
- try Datatype.Int.Map.find info.cpt info.statuses
- with Not_found ->
- Options.fatal "[keep_status] unbound annotation (id %d)@ in function %a"
- info.cpt
- Kernel_function.pretty kf
- in
- (* check kind consistency in order to detect more abnormal behaviors *)
- if kind <> kind' then
- Options.fatal
- "[keep_status] incorrect kind '%a' (expected: '%a')@ in function %a"
- pretty_kind kind
- pretty_kind kind'
- Kernel_function.pretty kf;
- keep
- with Not_found -> true
-
-(*
-Local Variables:
-compile-command: "make -C ../../../../.."
-End:
-*)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 57458a5688878cb8930006420b56b818aa7905d5..2f167b55c03dbf9eb5fc203cdc93d569dfcd8323 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Cil_datatype
let dkey = Options.dkey_prepare
@@ -28,81 +29,69 @@ let dkey = Options.dkey_prepare
(* Environment *)
(* ********************************************************************** *)
-let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
-
-(* The purpose of [actions] is similar to the Frama-C visitor's
- [get_filling_actions] but we need to fill it outside the visitor. So it is
- our own version. *)
-let actions = Queue.create ()
-
-(* global table for ensuring that logic info are not shared between a function
- definition and its duplicate *)
-module Global: sig
- val add_logic_info: logic_info -> unit
- val mem_logic_info: logic_info -> bool
+module Dup_functions: sig
+ val generate_vi: varinfo -> varinfo (* return the new varinfo *)
+ val mem: varinfo -> bool
+ val find: varinfo -> varinfo
val reset: unit -> unit
end = struct
- let tbl = Cil_datatype.Logic_info.Hashtbl.create 7
- let add_logic_info x = Cil_datatype.Logic_info.Hashtbl.add tbl x ()
- let mem_logic_info x = Cil_datatype.Logic_info.Hashtbl.mem tbl x
- let reset () = Cil_datatype.Logic_info.Hashtbl.clear tbl
+ let tbl: varinfo Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
+
+ (* assume [vi] is not already in [tbl] *)
+ let generate_vi vi =
+ let new_name = Functions.RTL.mk_gen_name vi.vname in
+ let new_vi =
+ Cil.makeGlobalVar
+ ~referenced:vi.vreferenced
+ ~loc:vi.vdecl
+ new_name
+ vi.vtype
+ in
+ Varinfo.Hashtbl.add tbl vi new_vi;
+ new_vi
-end
+ let mem = Varinfo.Hashtbl.mem tbl
+ let find = Varinfo.Hashtbl.find tbl
+ let reset () = Varinfo.Hashtbl.clear tbl
-let reset () =
- Kernel_function.Hashtbl.clear fct_tbl;
- Global.reset ();
- Queue.clear actions
+end
(* ********************************************************************** *)
(* Duplicating a function *)
(* ********************************************************************** *)
-(* [tbl] associates the old formals to the new ones *)
-let dup_funspec tbl bhv spec =
+(* [formals] associates the old formals to the new ones in order to
+ substitute them in [spec]. *)
+let dup_funspec formals spec =
(* Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
let o = object
- inherit Cil.genericCilVisitor bhv
-
- val already_visited = Cil_datatype.Logic_var.Hashtbl.create 7
-
- method !vlogic_info_use li =
- if Global.mem_logic_info li then
- Cil.ChangeDoChildrenPost
- ({ li with l_var_info = li.l_var_info } (* force a copy *),
- Visitor_behavior.Get.logic_info bhv)
- else
- Cil.JustCopy
+ inherit Visitor.frama_c_refresh (Project.current ())
- method !vterm_offset _ =
- Cil.DoChildrenPost
- (function (* no way to directly visit fieldinfo and model_info uses *)
- | TField(fi, off) ->
- TField(Visitor_behavior.Get.fieldinfo bhv fi, off)
- | TModel(mi, off) ->
- TModel(Visitor_behavior.Get.model_info bhv mi, off)
- | off ->
- off)
+ val already_visited = Logic_var.Hashtbl.create 7
+ (* just substituting in [!vvrbl] (when using a varinfo) does not work
+ because varinfo's occurrences are shared in logic_vars, so modifying the
+ varinfo would modify any logic_var based on it, even if it is not part of
+ this [spec] (e.g., if it is in another annotation of the same
+ function) *)
method !vlogic_var_use orig_lvi =
match orig_lvi.lv_origin with
| None ->
Cil.JustCopy
| Some vi ->
try
- let new_lvi =
- Cil_datatype.Logic_var.Hashtbl.find already_visited orig_lvi
- in
+ let new_lvi = Logic_var.Hashtbl.find already_visited orig_lvi in
+ (* recreate sharing of the logic_var in this [spec] *)
Cil.ChangeTo new_lvi
with Not_found ->
+ (* first time visiting this logic var *)
Cil.ChangeDoChildrenPost
({ orig_lvi with lv_id = orig_lvi.lv_id } (* force a copy *),
fun lvi ->
try
- let new_vi = Cil_datatype.Varinfo.Hashtbl.find tbl vi in
- Cil_datatype.Logic_var.Hashtbl.add
- already_visited orig_lvi lvi;
+ let new_vi = Varinfo.Hashtbl.find formals vi in
+ Logic_var.Hashtbl.add already_visited orig_lvi lvi;
(* [lvi] is the logic counterpart of a formal varinfo that has
been replaced by a new one: propagate this change *)
lvi.lv_id <- new_vi.vid;
@@ -112,20 +101,12 @@ let dup_funspec tbl bhv spec =
lvi
with Not_found ->
assert vi.vglob;
- (* using [Visitor_behavior.Get.logic_var bhv lvi] is correct
- only because the lv_id used to compare the lvi does not
- change between the original one and this copy *)
- Visitor_behavior.Get.logic_var bhv lvi)
+ lvi)
- method !videntified_term _ =
- Cil.DoChildrenPost Logic_const.refresh_identified_term
-
- method !videntified_predicate _ =
- Cil.DoChildrenPost Logic_const.refresh_predicate
end in
- Cil.visitCilFunspec o spec
+ Cil.visitCilFunspec (o :> Cil.cilVisitor) spec
-let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
+let dup_fundec loc spec sound_verdict_vi kf vi new_vi =
new_vi.vdefined <- true;
let formals = Kernel_function.get_formals kf in
let mk_formal vi =
@@ -174,9 +155,9 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
let locals = match res with None -> [] | Some r -> [ r ] in
let body = Cil.mkBlock stmts in
body.blocals <- locals;
- let tbl = Cil_datatype.Varinfo.Hashtbl.create 7 in
- List.iter2 (Cil_datatype.Varinfo.Hashtbl.add tbl) formals new_formals;
- let new_spec = dup_funspec tbl bhv spec in
+ let tbl = Varinfo.Hashtbl.create 7 in
+ List.iter2 (Varinfo.Hashtbl.add tbl) formals new_formals;
+ let new_spec = dup_funspec tbl spec in
let fundec =
{ svar = new_vi;
sformals = new_formals;
@@ -192,54 +173,69 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
Cfg.cfgFun fundec;
fundec
-let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
+let dup_global loc spec sound_verdict_vi kf vi new_vi =
let name = vi.vname in
Options.feedback ~dkey ~level:2 "entering in function %s" name;
- let fundec = dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi in
- let fct = Definition(fundec, loc) in
- let new_spec = fundec.sspec in
- let new_kf = { fundec = fct; spec = new_spec } in
- Queue.add
- (fun () ->
- Kernel_function.Hashtbl.add fct_tbl new_kf ();
- Globals.Functions.register new_kf;
- Globals.Functions.replace_by_definition new_spec fundec loc;
- Annotations.register_funspec new_kf;
- if new_vi.vname = "main" then begin
- (* recompute the info about the old main since its name has changed;
- see the corresponding part in the main visitor *)
- Globals.Functions.remove vi;
- Globals.Functions.register kf
- end)
- actions;
- (* remove the specs attached to the previous kf iff it is a definition:
- it is necessary to keep stable the number of annotations in order to get
- [Keep_status] working fine. *)
- let kf = Visitor_behavior.Get.kernel_function bhv kf in
+ let new_fundec = dup_fundec loc spec sound_verdict_vi kf vi new_vi in
+ let new_fct = Definition(new_fundec, loc) in
+ let new_spec = new_fundec.sspec in
+ let new_kf = { fundec = new_fct; spec = new_spec } in
+ Globals.Functions.register new_kf;
+ Globals.Functions.replace_by_definition new_spec new_fundec loc;
+ Annotations.register_funspec new_kf;
+ if Datatype.String.equal new_vi.vname "main" then begin
+ (* recompute kernel's info about the old main since its name has changed;
+ see the corresponding part in the main visitor *)
+ Globals.Functions.remove vi;
+ Globals.Functions.register kf
+ end;
+ (* copy property statuses to the new spec *)
+ let copy old_ip new_ip =
+ let open Property_status in
+ let cp status ep =
+ let e = Emitter.Usable_emitter.get ep.emitter in
+ if ep.logical_consequence
+ then logical_consequence e new_ip ep.properties
+ else emit e new_ip ~hyps:ep.properties status
+ in
+ match get old_ip with
+ | Never_tried ->
+ ()
+ | Best(s, epl) ->
+ List.iter (cp s) epl
+ | Inconsistent icst ->
+ List.iter (cp True) icst.valid;
+ (* either the program is reachable and [False_and_reachable] is
+ fine, or the program point is not reachable and it does not
+ matter for E-ACSL that checks it at runtime. *)
+ List.iter (cp False_and_reachable) icst.invalid
+ in
+ let ips kf s = Property.ip_of_spec kf Kglobal ~active:[] s in
+ List.iter2 copy (ips kf spec) (ips new_kf new_spec);
+ (* remove annotations from the old spec. Yet keep them in functions only
+ declared since, otherwise, the kernel would complain about functions
+ with neither contract nor body *)
if Kernel_function.is_definition kf then begin
- Queue.add
- (fun () ->
- let bhvs =
- Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
- in
- List.iter
- (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
- bhvs;
- Annotations.iter_decreases
- (fun e _ -> Annotations.remove_decreases e kf)
- kf;
- Annotations.iter_terminates
- (fun e _ -> Annotations.remove_terminates e kf)
- kf;
- Annotations.iter_complete
- (fun e l -> Annotations.remove_complete e kf l)
- kf;
- Annotations.iter_disjoint
- (fun e l -> Annotations.remove_disjoint e kf l)
- kf)
- actions
+ let old_bhvs =
+ Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
+ in
+ List.iter
+ (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
+ old_bhvs;
+ Annotations.iter_decreases
+ (fun e _ -> Annotations.remove_decreases e kf)
+ kf;
+ Annotations.iter_terminates
+ (fun e _ -> Annotations.remove_terminates e kf)
+ kf;
+ Annotations.iter_complete
+ (fun e l -> Annotations.remove_complete e kf l)
+ kf;
+ Annotations.iter_disjoint
+ (fun e l -> Annotations.remove_disjoint e kf l)
+ kf
end;
- GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
+ GFun(new_fundec, loc), GFunDecl(new_spec, new_vi, loc)
(* ********************************************************************** *)
(* Alignment *)
@@ -293,356 +289,187 @@ let require_alignment vi algn =
Cil.bitsSizeOf vi.vtype < algn*8 && not (sufficiently_aligned vi algn)
(* ********************************************************************** *)
-(* Visitor *)
+(* Visiting the globals *)
(* ********************************************************************** *)
-class prepare_visitor = object (self)
- inherit Visitor.frama_c_inplace
-
- val mutable has_new_stmt_in_fundec = false
-
- (* ---------------------------------------------------------------------- *)
- (* visitor's local variable *)
- (* ---------------------------------------------------------------------- *)
-
- val terms = Misc.Id_term.Hashtbl.create 7
- (* table for ensuring absence of term sharing *)
-
- val unduplicable_functions =
- let white_list =
- [ "__builtin_va_arg";
- "__builtin_va_end";
- "__builtin_va_start";
- "__builtin_va_copy" ]
- in
- List.fold_left
- (fun acc s -> Datatype.String.Set.add s acc)
- Datatype.String.Set.empty
- white_list
-
- val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
- val mutable new_definitions: global list = []
- (* new definitions of the annotated functions which will contain the
- translation of the E-ACSL contract *)
-
- (* the variable [sound_verdict] belongs to the E-ACSL's RTL and indicates
- whether the verdict emitted by E-ACSL is sound. It needs to be visible at
- that point because it is set in all function duplicates
- (see [dup_fundec]). *)
- val mutable sound_verdict_vi =
- let name = Functions.RTL.mk_api_name "sound_verdict" in
- let vi = Cil.makeGlobalVar name Cil.intType in
- vi.vstorage <- Extern;
- vi.vreferenced <- true;
- vi
-
- (* ---------------------------------------------------------------------- *)
- (* visitor's private methods *)
- (* ---------------------------------------------------------------------- *)
-
- method private is_variadic_function vi =
- match Cil.unrollType vi.vtype with
- | TFun(_, _, variadic, _) -> variadic
- | _ -> true
-
- (* IMPORTANT: for keeping property statuses, we must preserve the ordering of
- translation, see function [Translate.translate_pre_spec] and
- [Translate.translate_post_spec]: be careful when modifying it. *)
-
- method private push_pre_spec s =
- let kf = Extlib.the self#current_kf in
- let kinstr = self#current_kinstr in
- let open Keep_status in
- Extlib.may
- (fun v -> push kf K_Decreases (Property.ip_of_decreases kf kinstr v))
- s.spec_variant;
- Extlib.may
- (fun t -> push kf K_Terminates (Property.ip_of_terminates kf kinstr t))
- s.spec_terminates;
- List.iter
- (fun l ->
- push kf K_Complete (Property.ip_of_complete kf kinstr ~active:[] l))
- s.spec_complete_behaviors;
- List.iter
- (fun l ->
- push kf K_Disjoint (Property.ip_of_disjoint kf kinstr ~active:[] l))
- s.spec_disjoint_behaviors;
- List.iter
- (fun b ->
- List.iter
- (fun p -> push kf K_Requires (Property.ip_of_requires kf kinstr b p))
- b.b_requires)
- s.spec_behavior
-
- method private push_post_spec spec =
- let do_behavior b =
- let kf = Extlib.the self#current_kf in
- let ki = match self#current_stmt with
- | None -> Kglobal
- | Some stmt -> Kstmt stmt
- in
- let open Keep_status in
- Extlib.may
- (push kf K_Assigns)
- (Property.ip_of_assigns
- kf
- ki
- (Property.Id_contract (Datatype.String.Set.empty (* TODO *), b))
- b.b_assigns);
- List.iter
- (fun p -> push kf K_Ensures (Property.ip_of_ensures kf ki b p))
- b.b_post_cond
- in
- (* fix ordering of behaviors' iterations *)
- let bhvs =
- List.sort
- (fun b1 b2 -> String.compare b1.b_name b2.b_name)
- spec.spec_behavior
- in
- List.iter do_behavior bhvs
-
- method private push_pre_code_annot a =
- let kf = Extlib.the self#current_kf in
- let stmt = Extlib.the self#current_stmt in
- let push_single k a =
- Keep_status.push kf k (Property.ip_of_code_annot_single kf stmt a)
- in
- let open Keep_status in
- match a.annot_content with
- | AAssert _ -> push_single K_Assert a
- | AStmtSpec(_ (* TODO *), s) -> self#push_pre_spec s
- | AInvariant _ -> push_single K_Invariant a
- | AVariant v ->
- push kf K_Variant (Property.ip_of_decreases kf (Kstmt stmt) v)
- | AAssigns _ ->
- (* TODO: should be a postcondition, but considered as an unhandled
- precondition in translate.ml right now; and we need to preserve the
- same ordering *)
- Extlib.may
- (push kf K_Assigns)
- (Property.ip_assigns_of_code_annot kf (Kstmt stmt) a)
- | AAllocation(_ (* TODO *), alloc) ->
- Extlib.may
- (push kf K_Allocation)
- (Property.ip_of_allocation kf (Kstmt stmt) (Property.Id_loop a) alloc)
- | APragma _ ->
- (* not yet translated *)
- ()
- | AExtended _ ->
- (* never translate extensions *)
- ()
-
- method private push_post_code_annot a = match a.annot_content with
- | AStmtSpec(_ (* TODO *), s) -> self#push_post_spec s
- | AAssert _
- | AInvariant _
- | AVariant _
- | AAssigns _
- | AAllocation _
- | APragma _
- | AExtended _ -> ()
-
- (* ---------------------------------------------------------------------- *)
- (* visitor's method overloading *)
- (* ---------------------------------------------------------------------- *)
-
- method !vlogic_info_decl li =
- Global.add_logic_info li;
- Cil.SkipChildren
-
- method !vvrbl vi =
- try
- let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
- (* replace functions at callsite by its duplicated version *)
- Cil.ChangeTo new_vi
- with Not_found ->
- Cil.SkipChildren
-
- method !vterm _t =
- Cil.DoChildrenPost
- (fun t ->
- if Misc.Id_term.Hashtbl.mem terms t then
- (* remove term sharing for soundness of E-ACSL typing
- (see typing.ml) *)
- { t with term_node = t.term_node }
- else begin
- Misc.Id_term.Hashtbl.add terms t ();
- t
- end)
-
- (* Add align attributes to local variables (required by temporal analysis) *)
- method !vblock _ =
- if Options.Temporal_validity.get () then
- Cil.DoChildrenPost
- (fun blk ->
- List.iter
- (fun vi ->
- (* 4 bytes alignment is required to allow sufficient space for
- storage of 32-bit timestamps in a 1:1 shadow. *)
- if require_alignment vi 4 then
- vi.vattr <-
- Attr("aligned", [ AInt Integer.four ]) :: vi.vattr)
- blk.blocals;
- blk)
- else
- Cil.DoChildren
-
- method !vstmt_aux stmt =
- Annotations.iter_code_annot
- (fun _ a -> self#push_pre_code_annot a)
- stmt;
- Cil.DoChildrenPost
- (fun _ ->
- Annotations.iter_code_annot
- (fun _ a -> self#push_post_code_annot a)
- stmt;
- stmt)
-
- method !vfunc fundec =
- Cil.DoChildrenPost
- (fun _ ->
- if has_new_stmt_in_fundec then begin
- has_new_stmt_in_fundec <- false;
- (* recompute the CFG *)
- Cfg.clearCFGinfo ~clear_id:false fundec;
- Cfg.cfgFun fundec;
- end;
- fundec)
-
- method !vglob_aux = function
- | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when (* duplicate a function iff: *)
- (* it is not already duplicated *)
- not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
- && (* it is duplicable *)
- not (Datatype.String.Set.mem vi.vname unduplicable_functions)
- && (* it is not a variadic function *)
- not (self#is_variadic_function vi)
- && (* it is not in the E-ACSL's RTL *)
- not (Misc.is_library_loc loc)
- && (* it is not a built-in *)
- not (Misc.is_fc_or_compiler_builtin vi)
- &&
- (let kf =
- try Globals.Functions.get vi with Not_found -> assert false
- in
- (* either explicitely listed as to be not instrumented *)
- not (Functions.instrument kf)
- ||
- (* or: *)
- ((* it has a function contract *)
- not (Cil.is_empty_funspec
- (Annotations.funspec ~populate:false
- (Extlib.the self#current_kf)))
- && (* its annotations must be monitored *)
- Functions.check kf))
- ->
- let name = Functions.RTL.mk_gen_name vi.vname in
- let new_vi = Cil.makeGlobalVar name vi.vtype in
- Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
- Cil.DoChildrenPost
- (fun l -> match l with
- | [ GFunDecl(_, vi, _) | GFun({ svar = vi }, _) as g ]
- ->
- let kf = Extlib.the self#current_kf in
- (match g with
- | GFunDecl _ ->
- if not (Kernel_function.is_definition kf)
- && vi.vname <> "malloc" && vi.vname <> "free"
- then
- Options.warning
- "@[annotating undefined function `%a':@ \
- the generated program may miss memory instrumentation@ \
- if there are memory-related annotations.@]"
- Printer.pp_varinfo vi
- | GFun _ -> ()
- | _ -> assert false);
- let spec = Annotations.funspec ~populate:false kf in
- self#push_pre_spec spec;
- self#push_post_spec spec;
- let tmp = vi.vname in
- if tmp = "main" then begin
- (* the new function becomes the new main: *)
- (* 1. swap the name of both functions *)
- vi.vname <- new_vi.vname;
- new_vi.vname <- tmp;
- (* 2. force recomputation of the entry point if necessary *)
- if Kernel.MainFunction.get () = tmp then begin
- let selection =
- State_selection.with_dependencies Kernel.MainFunction.self
- in
- Project.clear ~selection ()
- end
- (* 3. recompute what is necessary in [Globals.Functions]:
- done in [dup_global] *)
- end;
- let new_g, new_decl =
- dup_global
- loc
- self#get_filling_actions
- spec
- self#behavior
- sound_verdict_vi
- kf
- vi
- new_vi
- in
- (* postpone the introduction of the new function definition to the
- end *)
- new_definitions <- new_g :: new_definitions;
- (* put the declaration before the original function in order to
- solve issue with recursive functions *)
- [ new_decl; g ]
- | _ -> assert false)
-
- | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi ->
- Cil.DoChildren
+(* perform a few modifications in the [kf]'s code and annotations that are
+ required by E-ACSL's analyses and transformations *)
+let prepare_fundec kf =
+ let o = object
+ inherit Visitor.frama_c_inplace
+
+ (* table for ensuring absence of term sharing *)
+ val terms = Misc.Id_term.Hashtbl.create 7
+
+ (* substitute function's varinfos by their duplicate in function calls *)
+ method !vvrbl vi =
+ try Cil.ChangeTo (Dup_functions.find vi)
+ with Not_found -> Cil.SkipChildren
+
+ (* temporal analysis requires that attributes are aligned to local
+ variables *)
+ method !vblock _ =
+ if Options.Temporal_validity.get () then
+ Cil.DoChildrenPost
+ (fun blk ->
+ List.iter
+ (fun vi ->
+ (* 4 bytes alignment is required to allow sufficient space for
+ storage of 32-bit timestamps in a 1:1 shadow. *)
+ if require_alignment vi 4 then
+ vi.vattr <-
+ Attr("aligned", [ AInt Integer.four ]) :: vi.vattr)
+ blk.blocals;
+ blk)
+ else
+ Cil.DoChildren
- | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when not (self#is_variadic_function vi)
- ->
- assert (* handled by the 2 cases above *)
- (not (Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi));
- let kf = Extlib.the self#current_kf in
- let s = Annotations.funspec ~populate:false kf in
+ (* remove term sharing introduced by the Frama-C kernel. For instance, an
+ annotation such as [a <= t <= b] is replaced by [a <= t && t <= b] with
+ both occurrences of [t] being shared. Yet, the E-ACSL type system may
+ require to assign them different types. *)
+ method !vterm _ =
Cil.DoChildrenPost
- (fun f ->
- self#push_pre_spec s;
- self#push_post_spec s;
- f)
+ (fun t ->
+ if Misc.Id_term.Hashtbl.mem terms t then
+ { t with term_node = t.term_node }
+ else begin
+ Misc.Id_term.Hashtbl.add terms t ();
+ t
+ end)
- | _ ->
+ method !videntified_predicate _ =
+ (* when entering a new annotation, clear the context to keep it small:
+ anyway, no sharing is possible between two identified predicates *)
+ Misc.Id_term.Hashtbl.clear terms;
Cil.DoChildren
- method !vfile f =
- Cil.DoChildrenPost
- (fun _ ->
- match new_definitions with
- | [] -> f
- | _ :: _ ->
- (* add the generated definitions of libc at the end of
- [new_definitions]. This way, we are sure that they have access to
- all of it (in particular, the memory model, GMP and the soundness
- variable). Also add the [__e_acsl_sound_verdict] variable at the
- beginning *)
- let new_globals =
- GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
- :: f.globals
- @ new_definitions
- in
- f.globals <- new_globals;
- f)
-
- initializer
- reset ()
-
-end
+ end in
+ ignore (Visitor.visitFramacKf o kf)
+
+(* the variable [sound_verdict] belongs to the E-ACSL's RTL and indicates
+ whether the verdict emitted by E-ACSL is sound. It needs to be visible at
+ that point because it is set in all function duplicates (see
+ [dup_fundec]). *)
+let sound_verdict_vi =
+ lazy
+ (let name = Functions.RTL.mk_api_name "sound_verdict" in
+ let vi = Cil.makeGlobalVar name Cil.intType in
+ vi.vstorage <- Extern;
+ vi.vreferenced <- true;
+ vi)
+
+let is_variadic_function vi = match Cil.unrollType vi.vtype with
+ | TFun(_, _, variadic, _) -> variadic
+ | _ -> false
+
+(* set of functions that must never be duplicated *)
+let unduplicable_functions =
+ let white_list =
+ [ "__builtin_va_arg";
+ "__builtin_va_end";
+ "__builtin_va_start";
+ "__builtin_va_copy";
+ (* *alloc and free should not be duplicated. *)
+ (* [TODO:] it preserves the former behavior. Should be modified latter by
+ checking only preconditions for any libc functions, see e-acsl#35 *)
+ "malloc";
+ "calloc";
+ "realloc";
+ "free" ]
+ in
+ List.fold_left
+ (fun acc s -> Datatype.String.Set.add s acc)
+ Datatype.String.Set.empty
+ white_list
+
+let must_duplicate kf vi =
+ (* it is not already duplicated *)
+ not (Dup_functions.mem vi)
+ && (* it is duplicable *)
+ not (Datatype.String.Set.mem vi.vname unduplicable_functions)
+ && (* it is not a variadic function *)
+ not (is_variadic_function vi)
+ && (* it is not a built-in *)
+ not (Misc.is_fc_or_compiler_builtin vi)
+ &&
+ ((* either explicitely listed as to be not instrumented *)
+ not (Functions.instrument kf)
+ ||
+ (* or: *)
+ ((* it has a function contract *)
+ not (Cil.is_empty_funspec (Annotations.funspec ~populate:false kf))
+ && (* its annotations must be monitored *)
+ Functions.check kf))
+
+let prepare_global (globals, new_defs) = function
+ | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc) as g ->
+ let kf = try Globals.Functions.get vi with Not_found -> assert false in
+ if must_duplicate kf vi then begin
+ let new_vi = Dup_functions.generate_vi vi in
+ if Kernel_function.is_definition kf then
+ prepare_fundec kf
+ else
+ (* TODO: this warning could be more precise if emitted during code
+ generation; see also E-ACSL issue #85 about partial verdicts *)
+ Options.warning
+ "@[annotating undefined function `%a':@ \
+ the generated program may miss memory instrumentation@ \
+ if there are memory-related annotations.@]"
+ Printer.pp_varinfo vi;
+ let tmp = vi.vname in
+ if Datatype.String.equal tmp "main" then begin
+ (* the new function becomes the new main: *)
+ (* 1. swap the name of both functions *)
+ vi.vname <- new_vi.vname;
+ new_vi.vname <- tmp;
+ (* 2. force recomputation of the entry point if necessary *)
+ if Kernel.MainFunction.get () = tmp then begin
+ let selection =
+ State_selection.with_dependencies Kernel.MainFunction.self
+ in
+ Project.clear ~selection ()
+ end
+ end;
+ let new_def, new_decl =
+ dup_global
+ loc
+ (Annotations.funspec ~populate:false kf)
+ (Lazy.force sound_verdict_vi)
+ kf
+ vi
+ new_vi
+ in
+ (* postpone the introduction of the new function definition *)
+ let new_defs = new_def :: new_defs in
+ (* put the declaration before the original function in order to solve
+ issues with recursive functions *)
+ g :: new_decl :: globals, new_defs
+ end else begin (* not duplicated *)
+ prepare_fundec kf;
+ g :: globals, new_defs
+ end
+ | g ->
+ (* nothing to do for globals that are not functions *)
+ g :: globals, new_defs
+
+let prepare_file file =
+ Dup_functions.reset ();
+ let rev_globals, new_defs =
+ List.fold_left prepare_global ([], []) file.globals
+ in
+ match new_defs with
+ | [] -> ()
+ | _ :: _ ->
+ (* insert the new_definitions at the end and reverse back the globals *)
+ let globals = List.fold_left (fun acc g -> g :: acc) new_defs rev_globals in
+ (* insert [__e_acsl_sound_verdict] at the beginning *)
+ let sg = GVarDecl(Lazy.force sound_verdict_vi, Location.unknown) in
+ file.globals <- sg :: globals
let prepare () =
Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
- Visitor.visitFramacFile (new prepare_visitor) (Ast.get ());
- Queue.iter (fun f -> f ()) actions;
+ prepare_file (Ast.get ());
Ast.mark_as_grown ()
(*
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index 5237a7d39d59ca87564a0f4d6329972f641c9f42..65ea62daf1854443f8523737c7f519d9e18e9dd6 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -25,7 +25,6 @@
More precisely, this module performs the following tasks:
- generating a new definition for functions with contract;
- removing term sharing;
- - storing what is necessary to translate in [Keep_status];
- in case of temporal validity checks, adding the attribute "aligned" to
variables that are not sufficiently aligned. *)
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
new file mode 100644
index 0000000000000000000000000000000000000000..38f3fb5809f3adc1a37e721dbb726d3a46f31393
--- /dev/null
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -0,0 +1,270 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+let rtl_files () =
+ List.map
+ (fun d -> Options.Share.get_file ~mode:`Must_exist d)
+ [ "e_acsl_gmp_api.h";
+ "e_acsl.h" ]
+
+(* create the RTL AST in a fresh project *)
+let create_rtl_ast prj =
+ Project.on
+ prj
+ (fun () ->
+ (* compute the RTL AST in the standard E-ACSL setting *)
+ if Plugin.is_present "variadic" then
+ Dynamic.Parameter.Bool.off "-variadic-translation" ();
+ Kernel.Keep_unused_specified_functions.off ();
+ Kernel.CppExtraArgs.add
+ (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
+ Kernel.Files.set (rtl_files ());
+ Ast.get ())
+ ()
+
+(* Note: vids, sids and eids are shared between projects (see implementation of
+ [Cil_const]). Therefore, no need to set them when inserting the corresponding
+ global into the AST. *)
+
+(* Tables that contain RTL's symbols. Useful to know whether some symbols is
+ part of the RTL. *)
+module Symbols: sig
+ val add_global: global -> unit
+ val mem_global: global -> bool
+ val add_kf: kernel_function -> unit
+ val mem_kf: kernel_function -> bool
+ val add_vi: string -> varinfo -> unit
+ val mem_vi: string -> bool
+ exception Unregistered of string
+ val find_vi: string -> varinfo (* may raise Unregistered *)
+ (* val debug: unit -> unit*)
+end = struct
+
+ let globals: unit Global.Hashtbl.t = Global.Hashtbl.create 17
+ let kfs: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 17
+ let vars
+ : varinfo Datatype.String.Hashtbl.t
+ = Datatype.String.Hashtbl.create 17
+
+ let add_global g = Global.Hashtbl.add globals g ()
+ let mem_global g = Global.Hashtbl.mem globals g
+
+ let add_kf g = Kernel_function.Hashtbl.add kfs g ()
+ let mem_kf g = Kernel_function.Hashtbl.mem kfs g
+
+ let add_vi s vi = Datatype.String.Hashtbl.add vars s vi
+ let mem_vi s = Datatype.String.Hashtbl.mem vars s
+ exception Unregistered of string
+ let find_vi s =
+ try Datatype.String.Hashtbl.find vars s
+ with Not_found -> raise (Unregistered s)
+
+(*
+ let debug () =
+ Global.Hashtbl.iter
+ (fun g1 () -> Format.printf "RTL %a@." Printer.pp_global g1)
+ rtl;
+ Varinfo.Hashtbl.iter
+ (fun g1 g2 -> Format.printf "VAR %a -> %a@."
+ Printer.pp_varinfo g1
+ Printer.pp_varinfo g2)
+ vars;
+ Typ.Hashtbl.iter
+ (fun g1 g2 -> Format.printf "TYP %a -> %a@."
+ Printer.pp_typ g1
+ Printer.pp_typ g2)
+ types;
+ Global_annotation.Hashtbl.iter
+ (fun g1 g2 -> Format.printf "ANNOT %a -> %a@."
+ Printer.pp_global_annotation g1
+ Printer.pp_global_annotation g2)
+ annots
+*)
+end
+
+(* NOTE: do not use [Mergecil.merge] since all [ast]'s symbols must be kept
+ unchanged: so do it ourselves. Thanksfully, we merge in a particular
+ setting because we know what the RTL is. Therefore merging is far from being
+ as complicated as [Mergecil]. *)
+
+(* lookup globals from [rtl_ast] in the current [ast] and fill the [Symbols]'
+ tables.
+ @return the list of globals to be inserted into [ast], in reverse order. *)
+let lookup_rtl_globals rtl_ast =
+ (* [do_it ~add mem acc l g] checks whether the global does exist in the user's
+ AST. If not, add it to the corresponding symbol table(s). *)
+ let rec do_it ?(add=fun _g -> ()) mem acc l g =
+ if mem g then do_globals (g :: acc) l
+ else begin
+ add g;
+ Symbols.add_global g;
+ do_globals (g :: acc) l
+ end
+ (* [do_ty] is [do_it] for types *)
+ and do_ty acc l g kind tname =
+ do_it (fun _ -> Globals.Types.mem_type kind tname) acc l g
+ and do_globals acc globs =
+ match globs with
+ | [] ->
+ acc
+ | GType(ti, _loc) as g :: l ->
+ do_ty acc l g Logic_typing.Typedef ti.tname
+ | GCompTag(ci, _loc) | GCompTagDecl(ci, _loc) as g :: l ->
+ let k = if ci.cstruct then Logic_typing.Struct else Logic_typing.Union in
+ do_ty acc l g k ci.cname
+ | GEnumTag(ei, _loc) | GEnumTagDecl(ei, _loc) as g :: l ->
+ do_ty acc l g Logic_typing.Enum ei.ename
+ | GVarDecl(vi, (pos, _)) | GVar(vi, _, (pos, _)) as g :: l ->
+ let tunit = Translation_unit pos.Filepath.pos_path in
+ let mem _g =
+ let g = Globals.Syntactic_search.find_in_scope vi.vorig_name tunit in
+ Option.is_some g
+ in
+ let add g =
+ Symbols.add_vi vi.vname vi;
+ match g with
+ | GVarDecl _ -> Globals.Vars.add_decl vi
+ | GVar(_, ii, _) -> Globals.Vars.add vi ii
+ | _ -> assert false
+ in
+ do_it ~add mem acc l g
+ | GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc) as g :: l ->
+ let add _g =
+ Symbols.add_vi vi.vname vi;
+ (* functions will be registered in kernel's table after substitution of
+ RTL's symbols inside them *)
+ in
+ do_it ~add (fun _ -> Globals.Functions.mem_name vi.vname) acc l g
+ | GAnnot _ :: l ->
+ (* ignoring annotations from the AST *)
+ do_globals acc l
+ | GAsm _ | GPragma _ | GText _ as g :: _l ->
+ Kernel.fatal "unexpected global %a" Printer.pp_global g
+ in
+ do_globals [] rtl_ast.globals
+
+(* [substitute_rtl_symbols] registers the correct symbols for RTL's functions *)
+let substitute_rtl_symbols rtl_prj = function
+ | GVarDecl _ | GVar _ as g ->
+ g
+ | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc) as g ->
+ let get_kf vi =
+ try
+ Globals.Functions.get vi
+ with Not_found ->
+ Options.fatal "unknown function %s in project %a"
+ vi.vname
+ Project.pretty (Project.current ())
+ in
+ let selection =
+ State_selection.of_list
+ [ Globals.Functions.self; Annotations.funspec_state ]
+ in
+ (* get the RTL's formals and spec *)
+ let formals, spec =
+ Project.on
+ rtl_prj
+ ~selection
+ (fun vi ->
+ let kf = get_kf vi in
+ Kernel_function.get_formals kf,
+ Annotations.funspec ~populate:false kf)
+ vi
+ in
+ (match g with
+ | GFunDecl _ ->
+ Globals.Functions.replace_by_declaration spec vi loc
+ | GFun(fundec, _) ->
+ Globals.Functions.replace_by_definition spec fundec loc
+ | _ -> assert false);
+ (* [Globals.Functions.replace_by_declaration] assigns new vids to formals:
+ get them back to their original ids in order to have the correct ids in
+ [spec] *)
+ let kf = get_kf vi in
+ List.iter2
+ (fun rtl_vi src_vi -> src_vi.vid <- rtl_vi.vid)
+ formals
+ (Kernel_function.get_formals kf);
+ Cil.unsafeSetFormalsDecl vi formals;
+ Annotations.register_funspec ~emitter:Options.emitter kf;
+ Symbols.add_kf kf;
+ g
+ | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _
+ | GAnnot _ | GAsm _ | GPragma _ | GText _ ->
+ assert false
+
+(* [insert_rtl_globals] adds the rtl symbols into the user's AST *)
+let insert_rtl_globals rtl_prj rtl_globals ast =
+ let add_ty acc old_g new_g =
+ let g = if Symbols.mem_global old_g then old_g else new_g in
+ (* keep them in the AST even if already in the user's one to prevent forward
+ references *)
+ g :: acc
+ in
+ let rec add acc = function
+ | [] ->
+ acc
+ | GType _ | GCompTagDecl _ | GEnumTagDecl _ as g :: l ->
+ (* RTL types contain no libc values: no need to substitute inside them *)
+ let acc = add_ty acc g g in
+ add acc l
+ | GCompTag(ci, loc) as g :: l ->
+ (* RTL's structure definitions that are already defined in the AST shall
+ be only declared *)
+ let acc = add_ty acc g (GCompTagDecl(ci, loc)) in
+ add acc l
+ | GEnumTag(ei, loc) as g :: l ->
+ (* RTL's enum definitions that are already defined in the AST shall be
+ only declared *)
+ let acc = add_ty acc g (GEnumTagDecl(ei, loc)) in
+ add acc l
+ | GVarDecl _ | GVar _ | GFunDecl _ | GFun _ as g :: l ->
+ let acc =
+ if Symbols.mem_global g then
+ let g = substitute_rtl_symbols rtl_prj g in
+ g :: acc
+ else
+ acc
+ in
+ add acc l
+ | GAnnot _ | GAsm _ | GPragma _ | GText _ as g :: _l ->
+ Kernel.fatal "unexpected global %a" Printer.pp_global g
+ in
+ ast.globals <- add ast.globals rtl_globals
+
+let link rtl_prj =
+ Options.feedback ~level:2 "link the E-ACSL RTL with the user source code";
+ let rtl_ast = create_rtl_ast rtl_prj in
+ let ast = Ast.get () in
+ let rtl_globals = lookup_rtl_globals rtl_ast in
+ (* Symbols.debug ();*)
+ insert_rtl_globals rtl_prj rtl_globals ast;
+ Ast.mark_as_grown ()
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/project_initializer/keep_status.mli b/src/plugins/e-acsl/src/project_initializer/rtl.mli
similarity index 61%
rename from src/plugins/e-acsl/src/project_initializer/keep_status.mli
rename to src/plugins/e-acsl/src/project_initializer/rtl.mli
index 455662756b7abdf51f79185ee20d09bf03fddd8a..ff7cf96526a68a6ab7a22d40c14865cf2825326c 100644
--- a/src/plugins/e-acsl/src/project_initializer/keep_status.mli
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.mli
@@ -20,41 +20,29 @@
(* *)
(**************************************************************************)
-(** Make the property statuses of the initial project accessible when
- doing the main translation *)
+(** This module links the E-ACSL's RTL to the user source code. *)
-type kind =
- | K_Assert
- | K_Invariant
- | K_Variant
- | K_StmtSpec
- | K_Allocation
- | K_Assigns
- | K_Decreases
- | K_Terminates (* TODO: should be removed: not part of the E-ACSL subset *)
- | K_Complete
- | K_Disjoint
- | K_Requires
- | K_Ensures
+val link: Project.t -> unit
+(** [link prj] links the RTL's AST contained in [prj] to the AST of the current
+ project. *)
-val clear: unit -> unit
-(** to be called before any program transformation *)
+(** Tables that contain RTL's symbols. Useful to know whether some symbols is
+ part of the RTL. *)
+module Symbols: sig
+ open Cil_types
-val push: Kernel_function.t -> kind -> Property.t -> unit
-(** store the given property of the given kind for the given function *)
+ val mem_global: global -> bool
+ val mem_kf: kernel_function -> bool
-val before_translation: unit -> unit
-(** to be called just before injecting the code *)
+ val mem_vi: string -> bool
+ exception Unregistered of string
+ val find_vi: string -> varinfo
+ (** @raise Unregistered if the given name is not part of the RTL. *)
-val must_translate: Kernel_function.t -> kind -> bool
-(** To be called just before transforming a property of the given kind for the
- given function.
- VERY IMPORTANT: the property of the n-th call to this function exactly
- correspond to the n-th pushed property (see {!push}).
- @return true if and only if the translation must occur. *)
+end
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
index 5f3956f765f048f6cac3858217ecfd51bfe4f7ea..b3d1e5df6a10a1ce8fb80e3003fc4f942cdff13b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void duffcopy(char *to, char *from, int count)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
index 6c992808644dc2b1a22a287bec261511fb770b8d..8f4aa78a77722c4c1bc7163cc8680bf7cc800d3a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
index 519c77cc7f1e326c2caa8402207cbea2b6564600..14dd1ab575af5a0d4560ecc5a1ac7ae3bc49a5d3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
@@ -36,24 +36,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& b));
__e_acsl_store_block((void *)(& a),(size_t)2);
__e_acsl_full_init((void *)(& a));
- __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_tmpnam));
- __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
- __e_acsl_full_init((void *)(& __fc_tmpnam));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdin),(size_t)8);
- __e_acsl_full_init((void *)(& stdin));
- __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_random48_counter));
- __e_acsl_store_block((void *)(random48_counter),(size_t)6);
- __e_acsl_full_init((void *)(& random48_counter));
- __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_random48_init));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
}
return;
}
@@ -62,15 +44,6 @@ void __e_acsl_globals_delete(void)
{
__e_acsl_delete_block((void *)(& b));
__e_acsl_delete_block((void *)(& a));
- __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
- __e_acsl_delete_block((void *)(__fc_tmpnam));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
index e7da245320f44ca617784993e0bf842400a92cff..574d904ff3e9f01ffb34f47c1945664f8330ef7b 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
@@ -35,24 +35,6 @@ void __e_acsl_globals_init(void)
__e_acsl_already_run = 1;
__e_acsl_store_block((void *)(& f),(size_t)1);
__e_acsl_full_init((void *)(& f));
- __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_tmpnam));
- __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
- __e_acsl_full_init((void *)(& __fc_tmpnam));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdin),(size_t)8);
- __e_acsl_full_init((void *)(& stdin));
- __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_random48_counter));
- __e_acsl_store_block((void *)(random48_counter),(size_t)6);
- __e_acsl_full_init((void *)(& random48_counter));
- __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_random48_init));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
}
return;
}
@@ -60,15 +42,6 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_delete(void)
{
__e_acsl_delete_block((void *)(& f));
- __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
- __e_acsl_delete_block((void *)(__fc_tmpnam));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c
index 483a08acdeca626a3024b416c9922f1356da660c..8de0529d5b4ebe3a34852ca95b5cd4d28c4e9816 100644
--- a/src/plugins/e-acsl/tests/memory/local_init.c
+++ b/src/plugins/e-acsl/tests/memory/local_init.c
@@ -1,7 +1,7 @@
/* run.config_ci
COMMENT: test of a local initializer which contains an annotation
LOG: gen_@PTEST_NAME@.c
- STDOPT: #"@MACHDEP@ @EACSL_PREPARE@ -lib-entry -eva -then -no-lib-entry"
+ STDOPT: #"@MACHDEP@ -lib-entry -eva -then -no-lib-entry"
*/
int X = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
index 15a99b43c04dacb8866abecb8ce0ef28e7db4bbf..4e43d7e9cff59e04b077b46a1e9d90fc81d9e076 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
index cc458e4e367b7f4f52387e3d42d727f7ff9f4df6..f38474ba466e667532e9d52c1e92653513013858 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
@@ -1,5 +1,6 @@
/* Generated by Frama-C */
#include "errno.h"
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
index 2cf1cc44c0cd0dd389bce183c8fa9c4fdb3ef873..3d26e79512a996e7a619a62f0c495e06bb09a0ee 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
index cd9cd223bf692bfcd3df82812937c41f4ebd306e..86e9de278227b7ff043988d6464c7b6120e761ae 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
index 7e7362461bb1ec5e09bc5b26370fcda40ddbc4c3..f0a98343e01d91146897001094205c0d8d01a50e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
@@ -1,6 +1,46 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
+/*@ requires valid_memptr: \valid(memptr);
+ requires
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+ allocates *\old(memptr);
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+ ensures result_zero: \result ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(size);
+ ensures result_non_zero: \result < 0 ∨ \result > 0;
+ assigns \result;
+ assigns \result \from (indirect: alignment);
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size);
+
+void *aligned_alloc(size_t alignment, size_t size);
+
int main(int argc, char const **argv)
{
int __retres;
@@ -11,7 +51,8 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& memptr),(size_t)8);
__e_acsl_full_init((void *)(& memptr));
int res2 =
- posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+ __gen_e_acsl_posix_memalign((void **)memptr,(unsigned long)256,
+ (unsigned long)15);
/*@ assert Eva: initialization: \initialized(memptr); */
char *p = *memptr;
__e_acsl_store_block((void *)(& p),(size_t)8);
@@ -138,4 +179,82 @@ int main(int argc, char const **argv)
return __retres;
}
+/*@ requires valid_memptr: \valid(memptr);
+ requires
+ alignment_is_a_suitable_power_of_two:
+ alignment ≥ sizeof(void *) ∧
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+ allocates *\old(memptr);
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+ ensures result_zero: \result ≡ 0;
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: alignment), size, __fc_heap_status;
+ assigns \result
+ \from (indirect: alignment), (indirect: size),
+ (indirect: __fc_heap_status);
+
+ behavior no_allocation:
+ assumes cannot_allocate: ¬is_allocable(size);
+ ensures result_non_zero: \result < 0 ∨ \result > 0;
+ assigns \result;
+ assigns \result \from (indirect: alignment);
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size)
+{
+ int __retres;
+ {
+ int __gen_e_acsl_valid;
+ int __gen_e_acsl_and;
+ __e_acsl_store_block((void *)(& memptr),(size_t)8);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)memptr,sizeof(void *),
+ (void *)memptr,(void *)(& memptr));
+ __e_acsl_assert(__gen_e_acsl_valid,"Precondition","posix_memalign",
+ "\\valid(memptr)","FRAMAC_SHARE/libc/stdlib.h",666);
+ if (alignment >= 8UL) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_band;
+ unsigned long __gen_e_acsl__3;
+ __gmpz_init_set_ui(__gen_e_acsl_,alignment);
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_band);
+ __gmpz_and(__gen_e_acsl_band,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_band));
+ __gen_e_acsl_and = __gen_e_acsl__3 == 0UL;
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_band);
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,"Precondition","posix_memalign",
+ "alignment >= sizeof(void *) &&\n((size_t)alignment & ((size_t)alignment - 1)) == 0",
+ "FRAMAC_SHARE/libc/stdlib.h",668);
+ }
+ __retres = posix_memalign(memptr,alignment,size);
+ __e_acsl_delete_block((void *)(& memptr));
+ return __retres;
+}
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
index 60fc5642381eca2bf0accc0e9093530f27e8f3c0..afc1d47904c708484482355ef4be0aaf6fcd4c2b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
@@ -1,6 +1,8 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern size_t __e_acsl_heap_allocation_size;
+
int main(int argc, char **argv)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
index 49ec6cf163ec5ba0edfad147a4fa237e95bb0678..75bddabfbe9edd97d7bff4bac71129cf540e7428 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
index 674eddac861dff410a723d4a8016853a5ce17ca5..bcfe10a812c72940b682369df2ac5f11caaaecba 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
@@ -1,4 +1,33 @@
[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `posix_memalign':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] tests/memory/memalign.c:38: Warning:
+ E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/memory/memalign.c:38: Warning:
+ E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:669: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
+ E-ACSL construct `predicate performing read accesses' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning:
+ E-ACSL construct `predicate performing read accesses' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:668: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
+ ignoring unsupported \allocates clause
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:679: Warning:
+ function __gen_e_acsl_posix_memalign, behavior allocation: postcondition 'allocation' got status unknown.
[eva:alarm] tests/memory/memalign.c:14: Warning:
accessing uninitialized left-value. assert \initialized(memptr);
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-valid.c b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
index 8cdb54fbcec93c33303e8fdebfa537406b57fb98..f84464d00758640dd8187876d1d0cd3bcefbcf50 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
@@ -1,6 +1,6 @@
/* run.config_ci, run.config_dev
COMMENT: test option -e-acsl-no-valid
- STDOPT: #"@MACHDEP@ @EACSL_PREPARE@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid"
+ STDOPT: #"@GLOBAL@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid"
MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -eva -eva-verbose 0
MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid
*/
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
index 666d954b82bcc4f6965b8b8b575a7f5f11c3a01e..3e24ef3f308c7f68f1fb6accf0ea4b6e604afe72 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
index 9ccb27aa258ca9cd5f58e030f4523d3535aec27f..007456238249612053c6ccc263073ada9d9840ba 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string_4;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
index 0f86c7371d4c879dc64808a673a75ca10dbe1a7a..3b0511fa9b1b81d990817fb3c5eb74072f572a8d 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config_ci.in
index 0a68607fc713abce8bf5ac09479dd477ff07e1dd..2c9748e535a049455c62e15f0f0ed3469bc5df95 100644
--- a/src/plugins/e-acsl/tests/test_config_ci.in
+++ b/src/plugins/e-acsl/tests/test_config_ci.in
@@ -1,7 +1,6 @@
MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
MACRO: MACHDEP -machdep gcc_x86_64
-MACRO: EACSL_PREPARE -e-acsl-prepare -e-acsl-share ./share/e-acsl
-MACRO: GLOBAL @MACHDEP@ -variadic-no-translation -verbose 0
+MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -variadic-no-translation -verbose 0
MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs