diff --git a/Changelog b/Changelog
index 8c9a705d3c372b62fee986ca97d723c021c62eec..c4be996965f6c843d60644c383d06de96e3536c3 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,8 @@
Open Source Release <next-release>
##################################
+- Eva [2019/10/23] New option -eva-auto-loop-unroll N to unroll all
+ loops whose number of iterations can be easily bounded by <N>.
- Eva [2019/10/21] New octagon domain inferring relations of the form
l ≤ ±X±Y ≤ e between pairs of integer variables X and Y. Enabled
with option -eva-octagon-domain. Only infers relations between
diff --git a/Makefile b/Makefile
index 9b155e7bc488aa52e135290be8d80d3fbbdcf288..6662ccfbd0253bbaa9cb0a55ffe13667951e5926 100644
--- a/Makefile
+++ b/Makefile
@@ -822,7 +822,7 @@ PLUGIN_ENABLE:=$(ENABLE_EVA)
PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
PLUGIN_EXTRA_DIRS:=engine values domains domains/cvalue domains/apron \
- domains/gauges domains/equality legacy slevel utils gui_files \
+ domains/gauges domains/equality legacy partitioning utils gui_files \
values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
@@ -855,12 +855,12 @@ endif
# General rules for ordering files within PLUGIN_CMO:
# - try to keep the legacy Value before Eva
-PLUGIN_CMO:= slevel/split_strategy value_parameters \
+PLUGIN_CMO:= partitioning/split_strategy value_parameters \
utils/value_perf utils/value_util utils/red_statuses \
utils/mark_noresults \
utils/widen_hints_ext utils/widen utils/partitioning_annots \
- engine/split_return \
- slevel/per_stmt_slevel \
+ partitioning/split_return \
+ partitioning/per_stmt_slevel \
utils/library_functions \
utils/eval_typ utils/backward_formals \
alarmset eval utils/structure utils/abstract \
@@ -898,10 +898,10 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
domains/cvalue/cvalue_domain \
engine/subdivided_evaluation engine/evaluation engine/abstractions \
engine/recursion engine/transfer_stmt engine/transfer_specification \
- engine/partitioning_index engine/mem_exec \
- engine/partition engine/partitioning_parameters engine/trace_partitioning \
- engine/iterator \
- engine/initialization \
+ partitioning/auto_loop_unroll \
+ partitioning/partition partitioning/partitioning_parameters \
+ partitioning/partitioning_index partitioning/trace_partitioning \
+ engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
diff --git a/doc/value/main.tex b/doc/value/main.tex
index a221390057992576d1a39bbb6e2d2fa99b6dddee..abb6737522fbfad435bb1ad7827f77e80a0dbe01 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -645,16 +645,28 @@ Before we spend any of our time looking at each of these alarms,
trying to determine whether they are true or false,
it is a good idea to make the analyzer spend more of {\em its} time
trying to determine the same thing.
-There are different settings that influence the compromise
-between precision and resource consumption. When dealing with bounded loops,
-the best approach consists in using an ACSL annotation, \verb+//@ loop unroll N+,
-to direct \Eva{} to analyze precisely the N first iterations of the loop
-before approximating the results.
+There are different settings that influence the trade-off
+between precision and resource consumption.
-Currently, annotating loops is done manually; in future releases of Frama-C,
-this will be partly automated. In simple loops, you can obtain its
-bounds via the GUI, by inspecting the values taken by the loop counter,
-as in the example below:
+When dealing with bounded loops, option \verb+-eva-auto-loop-unroll N+
+automatically unrolls simple loops that have less than \verb+N+ iterations.
+This option is based on syntactic heuristics to improve the precision
+at a low cost, and will not handle complex loops.
+It should be enabled in most analyses.
+
+If automatic loop unrolling is insufficient, the next best approach consists in
+using an ACSL annotation, \verb+//@ loop unroll N+, to direct \Eva{} to analyze
+precisely the \verb+N+ first iterations of the loop before approximating the
+results.
+
+Note: both approaches can be combined to enable automatic loop unrolling
+{\em except} in a few chosen loops: since the \verb+@loop unroll+ annotation
+takes precedence over other options, adding \verb+@loop unroll 0;+ to a loop
+will prevent it from being unrolled, even when \verb+-eva-auto-loop-unroll+
+is active.
+
+Frama-C's graphical interface can help estimating loop bounds by inspecting the
+values taken by the loop counter, as in the example below:
\begin{figure}[hbt]
\centering
@@ -682,7 +694,7 @@ then add the loop unroll annotation, as follows:
The value 4 is sufficient to completely unroll the loop, even though \verb|i|
ranges from 0 to 4 (5 values in total). One way to confirm the unrolling is
-complete is to check that the ``starting to merge loop iterations'' is no
+complete is to check that ``starting to merge loop iterations'' is no
longer emitted when entering the loop. Also, when a loop unroll annotation
is present but insufficient to unroll the loop, a message is emitted:
@@ -3281,16 +3293,16 @@ on its own in a generic context.
\section{Improving precision in loops}
\label{boucles-traitement}
-The default treatment of loops by the analyzer may produce
-results that are too approximate. Tuning
-the treatment of loops can improve precision.
+The default treatment of loops by the analyzer often produces
+results that are too approximate.
+Fine-tuning loops is one of the main ways to improve precision in the analysis.
When encountering a loop, the analyzer tries to compute a state
-that contains all the concrete states possible at
-run-time, including the initial concrete state just before
-entering the loop. This englobing state may be too imprecise
-by construction: typically, if the analyzed loop is initializing
-an array, the user does not expect to see the initial values of
+that contains all the possible concrete states at run-time,
+including the initial concrete state just before entering the loop.
+This enclosing state, by construction, is often imprecise:
+typically, if the analyzed loop is initializing an array,
+the user does not expect to see the initial values of
the array appear in the state computed by the analyzer.
The solution in this case is to either unroll loops, using one of several
available methods, or to add annotations (widening hints or loop invariants)
@@ -3300,23 +3312,57 @@ time remains bounded.
\subsection{Loop unrolling}
\label{loop-unroll}
-Loop unrolling is often easier to apply, since it does not require much
-knowledge about the loop, other than an estimate of the number of iterations.
-This estimate may not improve precision if too low
-or lead to unnecessary work if too high,
-but will never affect its correctness.
-
-\subsubsection{Loop unroll annotations}
-
Whenever a loop has a fixed number of iterations (or a known upper bound),
-an easy and precise way to handle it is to include a
-\lstinline|loop unroll <n>| annotation, where
-\lstinline|<n>| is the number of iterations of the loop.
-It will indicate \Eva{} to analyze the loop by semantically unrolling each
-iteration, avoiding merging states from different iterations.
+Eva can precisely analyze it by semantically unrolling each iteration,
+avoiding merging states from different iterations.
This leads to increased cost in terms of analysis, but usually the cost
increase is worth the improvement in precision.
+Loop unrolling is often easy to apply, since it does not require much
+knowledge about the loop, other than an estimate of the number of iterations.
+If the estimate is too low, precision won't improve; if it is too high,
+it may lead to unnecessary work; but under no circumstances will it affect the
+correctness of the analysis.
+
+\subsubsection{Automatic loop unrolling}
+
+\Eva{} includes a syntactic heuristic to automatically unroll simple loops
+whose number of iterations can be easily bounded.
+It is enabled via option \lstinline|-eva-auto-loop-unroll <n>|, where
+\lstinline|<n>| is the maximum number of iterations to unroll: loops with
+less than \lstinline|<n>| iterations will be completely unrolled.
+If the analysis cannot infer that a loop terminates within less than
+\lstinline|<n>| iterations, then no unrolling is performed.
+
+\lstinline|-eva-auto-loop-unroll| is recommended as the first approach towards
+loop unrolling, due to its low cost and ease of setup. An unrolling limit
+up to a few hundred seems suitable in most cases.
+
+If \emph{all} loops in a program need to be unrolled, one way to do it quickly
+consists in using option \lstinline|-eva-min-loop-unroll <n>|,
+where \lstinline|<n>| is the number of iterations to unroll in each loop.
+This option is very expensive, and its use should be limited.
+
+For a more fine-grained analysis and for non-trivial loops,
+annotations are available to configure the loop unrolling on a case by case
+basis.
+These annotations take precedence over the automatic loop unrolling mechanism
+and can be combined with them, e.g. to automatically unroll {\em all but} a few
+loops.
+
+With options \lstinline|-eva-auto-loop-unroll AUTO -eva-min-loop-unroll MIN|:
+\begin{itemize}
+\item if a loop has a loop unroll annotation, it is unrolled accordingly;
+\item otherwise, if a loop has evidently less than \lstinline|AUTO| iterations,
+ it is completely unrolled;
+\item otherwise, the \lstinline|MIN| first iterations of the loop are unrolled.
+\end{itemize}
+
+\subsubsection{Loop unroll annotations}
+
+Individual loops can be unrolled by preceding them with a
+\lstinline|loop unroll <n>| annotation, where \lstinline|<n>| is the number
+of iterations to unroll.
Such annotations must be placed just before the loop (i.e. before the
\lstinline|while|, \lstinline|for| or \lstinline|do| introducing the loop),
and one annotation is required per loop, including nested ones. For instance:
@@ -3368,14 +3414,9 @@ Note that using an unrolling parameter which is higher than the actual number
of iterations of a loop doesn't generally have an effect on the analysis.
The analyzer will usually detect that further iterations are not useful.
-If all loops in a program need to be unrolled, one way to do it quickly
-consists in using option \lstinline|-eva-min-loop-unroll <n>|,
-where \lstinline|<n>| is the number of iterations to unroll in each loop.
-This option has lower precedence than \lstinline|loop unroll| annotations:
-\Eva{} will always consider the latter if it is present in a loop.
-This allows, for instance, to prevent unrolling of an infinite loop by
-adding \lstinline|loop unroll 0| before it, while unrolling the remaining
-loops by the specified amount in \lstinline|-eva-min-loop-unroll|.
+Loop annotations can also be used to prevent the automatic loop unrolling
+for some specific loops: adding \lstinline|loop unroll 0| before a loop
+ensures that no iteration of the loop will be unrolled.
\subsubsection{Unrolling via option {\em -eva-slevel}}
\label{slevel}
@@ -5384,29 +5425,30 @@ return \lstinline|6| and \lstinline|36| respectively.
\question{Which option should I use to improve the handling of loops
in my program?}
-The recommended way is to use \lstinline|loop unroll| annotations on a case by
-case basis, which is the most precise and stable mechanism currently in \Eva{}.
-Alternatively, using \lstinline|-eva-slevel| is the next best approach.
-This option is more costly, often hard to predict, and can only be specified
-globally or at the function level (via \lstinline|-eva-slevel-function|).
-However, it works for loops that are built using \lstinline|goto|s instead of
-\lstinline|for| or \lstinline|while|, and it also improves precision when
-evaluating \lstinline|if| or \lstinline|switch| conditionals (but it is consumed
-by them, which can be confusing for the user).
-
-Both approaches do have a minor drawback, in that they do not allow to observe
-a specific iteration step of the loop. The main advantage of these options is
-that they leave the source code unchanged.
-
-The Frama-C kernel has an option \lstinline|-ulevel|, which performs a
-syntactic modification of the analyzed source code. Its advantage is that,
-by explicitly separating iteration steps, it allows to use
-the graphical user interface to observe values or express properties for a
-specific iteration step of the loop. However, the duplication of loop
-statements and variables can lead to cluttered code. Also, the transformation
-increases the size of the code in the Frama-C AST and, for large functions,
-this has a significant impact in the analysis
-time. For these reasons, \lstinline|-ulevel| is seldom used nowadays.
+Start with \lstinline|-eva-auto-loop-unroll|. If automatic unrolling is not
+sufficient, the recommended way is to use \lstinline|loop unroll| annotations
+on a case by case basis. This is the most precise and stable mechanism
+currently in \Eva{}. It does have the drawback of requiring changes to the
+source code, however.
+
+If none of the above techniques is suitable, using \lstinline|-eva-slevel|
+is the next best approach. Compared to the previous ones, this option is more
+costly, often hard to predict, and can only be specified globally or at the
+function level (via \lstinline|-eva-slevel-function|), however it works with
+loops that are built using \lstinline|goto|s instead of \lstinline|for| or
+\lstinline|while|. It also improves precision when evaluating \lstinline|if| or
+\lstinline|switch| conditionals (but it is consumed by them, which can be
+confusing for the user).
+
+Finally, there is an option from the Frama-C kernel, \lstinline|-ulevel|,
+which performs a syntactic modification of the analyzed source code.
+Its advantage is that, by explicitly separating iteration steps,
+it allows using the graphical user interface to observe values or express
+properties for a specific iteration step of the loop.
+However, the duplication of loop statements and variables can clutter the code.
+Also, the transformation increases the size of the code in the Frama-C AST and,
+for large functions, this has a significant impact in the analysis time.
+For these reasons, \lstinline|-ulevel| is seldom used nowadays.
\question{Alarms that occur after a true alarm in the analyzed code
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index e498c994b2737da8e4628e247bf936aef0efb7fb..3a00fb89591cebef116a40d4612856c551d31075 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1215,20 +1215,10 @@ src/plugins/value/engine/iterator.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/iterator.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/mem_exec.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/mem_exec.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/partition.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/partition.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/partitioning_index.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/partitioning_index.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/partitioning_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/partitioning_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/recursion.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/recursion.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/split_return.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/split_return.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/subdivided_evaluation.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/subdivided_evaluation.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/trace_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/trace_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_logic.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_logic.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_specification.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1259,10 +1249,22 @@ src/plugins/value/legacy/function_args.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/legacy/function_args.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/slevel/per_stmt_slevel.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/slevel/per_stmt_slevel.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/slevel/split_strategy.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/slevel/split_strategy.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/auto_loop_unroll.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/auto_loop_unroll.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/partition.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/partition.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/partitioning_index.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/partitioning_index.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/partitioning_parameters.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/partitioning_parameters.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/per_stmt_slevel.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/per_stmt_slevel.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/split_return.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/split_return.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/split_strategy.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/split_strategy.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/trace_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/partitioning/trace_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/test.assert.sh: .ignore
src/plugins/value/test.sh: .ignore
src/plugins/value/utils/abstract.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 3d7cdeb70656b929e2f259a7dcb20977f6eea92b..b9f8d8529c95358a14b00b53f6ee29139f433a23 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -1161,6 +1161,42 @@ let join v1 v2 =
pretty v1 pretty v2 pretty result; *)
result
+let complement_int_under ~size ~signed i =
+ let e = Int.two_power_of_int (if signed then size - 1 else size) in
+ let b = if signed then Int.neg e else Int.zero in
+ let e = Int.pred e in
+ let inject_range min max = `Value (inject_range (Some min) (Some max)) in
+ match i with
+ | Float _ -> `Bottom
+ | Set [||] -> inject_range b e
+ | Set set ->
+ let l = Array.length set in
+ let array = Array.make (l + 2) Int.zero in
+ array.(0) <- b;
+ Array.blit set 0 array 1 l;
+ array.(l+1) <- e;
+ let index = ref (-1) in
+ let max_delta = ref Int.zero in
+ for i = 0 to l do
+ let delta = Int.sub array.(i+1) array.(i) in
+ if Int.gt delta !max_delta then begin
+ index := i;
+ max_delta := delta
+ end
+ done;
+ inject_range array.(!index) array.(!index + 1)
+ | Top (min, max, _rem, _modu) ->
+ match min, max with
+ | None, None -> `Bottom
+ | Some min, None -> inject_range b (Int.pred min)
+ | None, Some max -> inject_range (Int.succ max) e
+ | Some min, Some max ->
+ let delta_min = Int.sub min b in
+ let delta_max = Int.sub e max in
+ if Int.le delta_min delta_max
+ then inject_range (Int.succ max) e
+ else inject_range b (Int.pred min)
+
let fold_int f v acc =
match v with
Top(None,_,_,_) | Top(_,None,_,_) | Float _ ->
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index cc7f8630939e8ca2024d3abea7fadb2075d7f635..a94f2aa8f8c32356edcef3dd7c3c67add75b029c 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -319,6 +319,9 @@ val reinterpret_as_int: size:Integer.t -> signed:bool -> t -> t
(** Bitwise reinterpretation of the given value, of size [size], as an integer
of the given signedness (and size). *)
+val complement_int_under: size:int -> signed:bool -> t -> t Bottom.or_bottom
+(** Returns an under-approximation of the integers of the given size and
+ signedness that are *not* represented by the given ival. *)
val pretty_debug : Format.formatter -> t -> unit
diff --git a/src/plugins/loop_analysis/README.org b/src/plugins/loop_analysis/README.org
index 7e90c89f5c08ff7b35874f7c359e89ee128be981..6e4388ee4b5e2b4be3761f62fd1d6dc811a255d5 100644
--- a/src/plugins/loop_analysis/README.org
+++ b/src/plugins/loop_analysis/README.org
@@ -1,5 +1,9 @@
Loop and "slevel" analysis.
+Note: this plug-in has been deprecated in favor of newer Eva features, such as
+ `-eva-auto-loop-unroll`, `//@ loop unroll` annotations and trace
+ partitioning. It will be removed in a future release.
+
* Overview
This plugin performs two analyses.
diff --git a/src/plugins/loop_analysis/options.ml b/src/plugins/loop_analysis/options.ml
index 58848be42e5c1533a915fe22df28d5cc5193cf5f..7c6339d5e1fc82016a5d90fed670510fdca3bcc8 100644
--- a/src/plugins/loop_analysis/options.ml
+++ b/src/plugins/loop_analysis/options.ml
@@ -24,13 +24,15 @@ include Plugin.Register
(struct
let name = "loop"
let shortname = "loop"
- let help = "Find number of iterations in loops, and slevel value"
+ let help = "[DEPRECATED: use Eva's loop unroll annotations and options] \
+ Find number of iterations in loops, and slevel value"
end)
module Run = False
(struct
let option_name = "-loop"
- let help = "Launch loop analysis"
+ let help = "[deprecated: use Eva loop unroll annotations or \
+ -eva-auto-loop-unroll] Launch loop analysis"
end)
module MaxIterations = Int
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
new file mode 100644
index 0000000000000000000000000000000000000000..37e2b81bbcb2bc8aa15f66167cb37d4ac62fd1e4
--- /dev/null
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -0,0 +1,452 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* Heuristic for automatic loop unrolling: when the number of iterations of a
+ loop can be bounded under a given limit, then unroll the loop.
+ The limit is defined by the option -eva-auto-loop-unroll. *)
+
+(* Gist of the heuristic:
+ - find a loop exit condition, in the form of a statement "if(cond) break;".
+ such that exactly one lvalue [lval] in the condition [cond] is modified
+ within the loop; all other lvalues must be constant in the loop.
+ - find a value [v_exit] such that [lval] ∈ [v_exit] ⇒ [cond] holds.
+ - evaluate [lval] to its initial value [v_init] in the loop entry state.
+ - compute an over-approximation of the increment [v_delta] of [lval] in one
+ iteration of the loop.
+
+ If [v_init] + k × [v_delta] ⊂ [v_exit], then the number of iterations
+ is bounded by the limit [k].
+
+ The heuristic is syntactic and limited to the current function: it does not
+ handle assignment through pointers or function calls.
+ Thus, the condition [cond] should only contains direct accesses to variables
+ whose address is never taken (they cannot be modified through pointers). If
+ the loop contains a function call, the condition [cond] should not contain
+ global variables (as they may be modified in the function called).
+ A first analyze of the loop gathers all such variables modified within the
+ loop; all others are constant, and can be evaluated in the loop entry state.
+
+ When computing the increment [v_delta] of a lvalue [v] in the loop, the
+ heuristic searches assignments "v = v ± i;". Any other assignment of [v]
+ cancels the heuristic. *)
+
+open Cil_types
+
+(* Is a statement a loop exit condition? If so, returns the condition and
+ whether the condition must hold to exit the loop. Otherwise, returns None. *)
+let is_conditional_break stmt =
+ match stmt.skind with
+ | If (cond, {bstmts=[{skind=Break _}]}, _, _) -> Some (cond, true)
+ | If (cond, _, {bstmts=[{skind=Break _}]}, _) -> Some (cond, false)
+ | _ -> None
+
+(* Returns a loop exit condition, as the conditional expression and whether
+ the condition must be zero or non-zero to exit the loop. *)
+let find_loop_exit_condition loop =
+ let rec aux = function
+ | [] -> None
+ | stmt :: tl ->
+ match is_conditional_break stmt with
+ | Some _ as x -> x
+ | None -> aux tl
+ in
+ aux loop.bstmts
+
+(* Effects of a loop:
+ - set of varinfos that are directly modified within the loop. Pointer
+ accesses are ignored.
+ - does the loop contain a call? If so, any global variable may also be
+ modified in the loop. *)
+type loop_effect =
+ { written_vars: Cil_datatype.Varinfo.Set.t;
+ call: bool; }
+
+(* Visitor to compute the effects of a loop. *)
+let loop_effect_visitor = object (self)
+ inherit Visitor.frama_c_inplace
+
+ val mutable written_vars = Cil_datatype.Varinfo.Set.empty
+ val mutable call = false
+ val mutable assembly = false
+
+ (* Returns None if the loop contains assembly code. *)
+ method compute_effect block =
+ written_vars <- Cil_datatype.Varinfo.Set.empty;
+ call <- false;
+ assembly <- false;
+ ignore Visitor.(visitFramacBlock (self :> frama_c_inplace) block);
+ if assembly then None else Some { written_vars; call; }
+
+ method !vinst instr =
+ let () = match instr with
+ | Set ((Var varinfo, _), _, _)
+ | Call (Some (Var varinfo, _), _, _, _) ->
+ written_vars <- Cil_datatype.Varinfo.Set.add varinfo written_vars;
+ | _ -> ()
+ in
+ let () = match instr with
+ | Asm _ -> assembly <- true
+ | Call _ -> call <- true
+ | _ -> ()
+ in
+ Cil.SkipChildren
+end
+
+(* The status of a lvalue for the automatic loop unroll heuristic. *)
+type var_status =
+ | Constant (* The lvalue is probably constant within the loop. *)
+ | Candidate (* The lvalue is a good candidate for the heuristic:
+ integer type, access to a varinfo whose address is not taken,
+ modified within the loop but not in another function called
+ in the loop. *)
+ | Unsuitable (* Cannot be used for the heuristic. *)
+
+let is_integer lval = Cil.isIntegralType (Cil.typeOfLval lval)
+
+(* Computes the status of a lvalue for the heuristic, according to the
+ loop effects. *)
+let classify loop_effect lval =
+ let rec is_const_expr expr =
+ match expr.enode with
+ | Lval lval -> classify_lval lval = Constant
+ | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> is_const_expr e
+ | BinOp (_, e1, e2, _) -> is_const_expr e1 && is_const_expr e2
+ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
+ | AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> true
+ and classify_lval = function
+ | Var varinfo, offset ->
+ if (varinfo.vglob && loop_effect.call)
+ || not (is_const_offset offset)
+ then Unsuitable
+ else if Cil_datatype.Varinfo.Set.mem varinfo loop_effect.written_vars
+ then
+ if is_integer lval && not varinfo.vaddrof then Candidate else Unsuitable
+ else
+ (* If the address of the variable is taken, it could be modified within
+ the loop. We suppose here that this is not the case, but this could
+ lead to some loop unrolling. *)
+ Constant
+ | Mem _, _ -> Unsuitable (* Pointers are not supported by the heuristic. *)
+ and is_const_offset = function
+ | NoOffset -> true
+ | Field (_, offset) -> is_const_offset offset
+ | Index (e, offset) -> is_const_expr e && is_const_offset offset
+ in
+ classify_lval lval
+
+(* Returns the list of all lvalues appearing in an expression. *)
+let rec get_lvalues expr =
+ match expr.enode with
+ | Lval lval -> [ lval ]
+ | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> get_lvalues e
+ | BinOp (_op, e1, e2, _typ) -> get_lvalues e1 @ get_lvalues e2
+ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
+ | AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> []
+
+(* Finds the unique candidate lvalue for the automatic loop unrolling
+ heuristic in the expression [expr], if it exists. Returns None otherwise. *)
+let find_lonely_candidate loop_effect expr =
+ let lvalues = get_lvalues expr in
+ let rec aux acc list =
+ match list with
+ | [] -> acc
+ | lval :: tl ->
+ match classify loop_effect lval with
+ | Unsuitable -> None
+ | Constant -> aux acc tl
+ | Candidate -> if acc = None then aux (Some lval) tl else None
+ in
+ aux None lvalues
+
+(* Returns true if the instruction assigns [lval]. *)
+let is_safe_instruction lval = function
+ | Set (lv, _, _)
+ | Call (Some lv, _, _, _) -> not (Cil_datatype.LvalStructEq.equal lval lv)
+ | Call (None, _, _, _) | Local_init _ | Skip _ | Code_annot _ -> true
+ | Asm _ -> false
+
+(* Returns true if the statement may assign [lval] during an iteration of the
+ loop [loop]. [lval] is a candidate for the automatic loop unroll heuristic,
+ and thus is modified within the loop. *)
+let is_safe lval ~loop stmt =
+ (* The current block being checked for a goto statement. *)
+ let current_block = ref None in
+ let rec is_safe_stmt stmt =
+ match stmt.skind with
+ | Instr instr -> is_safe_instruction lval instr
+ | Return _ | Break _ | Continue _ -> true
+ | If (_, b_then, b_else, _) -> is_safe_block b_then && is_safe_block b_else
+ | Block b
+ | Switch (_, b, _, _)
+ | Loop (_, b, _, _, _) -> is_safe_block b
+ | UnspecifiedSequence list ->
+ List.for_all (fun (stmt, _, _, _, _) -> is_safe_stmt stmt) list
+ | Goto (dest, _) -> begin
+ let dest_blocks = Kernel_function.find_all_enclosing_blocks !dest in
+ (* If the goto leaves the loop, then it is safe. *)
+ if List.mem loop dest_blocks then true else
+ (* If the goto moves into the block currently being checked, then it
+ is safe if the block is safe (which we are currently checking). *)
+ match !current_block with
+ | Some current_block when List.mem current_block dest_blocks -> true
+ | _ ->
+ (* Otherwise, we need to check that the whole block englobing
+ both the source and the destination of the goto is safe. *)
+ let block = Kernel_function.common_block !dest stmt in
+ current_block := Some block;
+ (* If this block is the loop itself, then it is not safe, as [lval]
+ is modified within the loop. *)
+ not (block = loop) && is_safe_block block
+ end
+ | _ -> false
+ (* A block is safe if all its statements are safe. *)
+ and is_safe_block block = List.for_all is_safe_stmt block.bstmts in
+ is_safe_stmt stmt
+
+
+module Make (Abstract: Abstractions.Eva) = struct
+
+ open Eval
+ open Abstract
+ module Valuation = Abstract.Eval.Valuation
+ module Clear_Valuation = Clear_Valuation (Valuation)
+
+ let (>>) v f = match v with `Value v -> f v | _ -> None
+ let (>>=) v f = match v with Some v -> f v | None -> None
+
+ let cvalue_complement typ cvalue =
+ let open Eval_typ in
+ match Eval_typ.classify_as_scalar typ with
+ | Some (TSFloat _ | TSPtr _) | None -> None
+ | Some (TSInt ik) ->
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ Ival.complement_int_under ~size:ik.i_bits ~signed:ik.i_signed ival
+ >> fun ival -> Some (Cvalue.V.inject_ival ival)
+ with Cvalue.V.Not_based_on_null -> None
+
+ (* Reduces the condition "[condition] = [positive]" to a sufficient hypothesis
+ on the value of the expression [expr]: computes a value [v] such that
+ if the expression [expr] evaluates to [v], then [condition] = [positive].
+ [valuation] contains additional hypotheses, i.e. the value of some constant
+ lvalues of the [condition]. All computations must be done in the top state
+ and in the given valuation. *)
+ let reduce_to_expr valuation ~expr ~condition ~positive =
+ let state = Abstract.Dom.top in
+ (* Reduces [expr] by assuming that [condition] is [positive]. *)
+ let reduce positive =
+ (* Assumes that [condition] is [positive]. *)
+ fst (Eval.reduce ~valuation state condition positive) >> fun valuation ->
+ (* Finds the value of [expr] in the resulting valuation. *)
+ Valuation.find valuation expr >> fun record ->
+ record.value.v >> fun value ->
+ (* If the new value of [expr] is top, no reduction has been performed. *)
+ if Val.(equal top value) then None else Some (value, record)
+ in
+ (* Different strategies whether cvalue is present. *)
+ match Val.get Main_values.CVal.key with
+ | Some get_cvalue ->
+ (* Assumes that [condition] is NOT [positive]. *)
+ reduce (not positive) >>= fun (value, _record) ->
+ (* [value] is an over-approximation of the values of [expr] for which
+ [condition] is NOT positive; its complement is an under-approximation
+ of the values for which [condition] is positive. *)
+ let cvalue = get_cvalue value in
+ cvalue_complement (Cil.typeOf expr) cvalue >>= fun cvalue ->
+ Some (Val.set Main_values.CVal.key cvalue Val.top)
+ | None ->
+ (* Assumes that [condition] is [positive]. Returns an over-approximation
+ of the values for which [condition] is [positive]. *)
+ reduce positive >>= fun (value, record) ->
+ (* Evaluates [condition] with the hypothesis [expr] ∈ [value], to check
+ whether [expr] ∈ [value] ⇒ [condition] = [positive]. *)
+ let valuation = Valuation.add valuation expr record in
+ fst (Eval.evaluate ~valuation ~reduction:false state condition)
+ >> fun (_valuation, v) ->
+ let satisfied =
+ if positive
+ then not Val.(is_included zero v)
+ else Val.(equal zero v)
+ in
+ if satisfied then Some value else None
+
+ (* Same as [reduce_to_expr] above, but builds the proper valuation from the
+ [state]. [state] is the entry state of the loop, and [expr] is the only
+ part of [condition] that is not constant within the loop. [state] can thus
+ be used to evaluate all other subparts of [condition], before computing
+ the value of [expr] that satisfies [condition]. *)
+ let reduce_to_lval_from_state state lval condition positive =
+ let expr = Cil.new_exp ~loc:condition.eloc (Lval lval) in
+ (* Evaluate the [condition] in the given [state]. *)
+ fst (Eval.evaluate state condition) >> fun (valuation, _v) ->
+ (* In the resulting valuation, replace the value of [expr] by [top_int]
+ and removes all expressions depending on [expr]. *)
+ Valuation.find valuation expr >> fun record ->
+ let value = { record.value with v = `Value Val.top_int } in
+ let record = { record with value } in
+ let valuation =
+ Clear_Valuation.clear_englobing_exprs
+ valuation ~expr:condition ~subexpr:expr
+ in
+ let valuation = Valuation.add valuation expr record in
+ reduce_to_expr valuation ~expr ~condition ~positive
+
+ (* Over-approximation of the increment of a lvalue in one loop iteration.*)
+ type delta =
+ { current: Val.t or_bottom; (* current delta being computed*)
+ final: Val.t or_bottom; (* final delta after a continue statement. *)
+ }
+
+ let join_delta d1 d2 =
+ { current = Bottom.join Val.join d1.current d2.current;
+ final = Bottom.join Val.join d1.final d2.final; }
+
+ let final_delta delta = Bottom.join Val.join delta.current delta.final
+
+ (* Raised when no increment can be computed for the given lvalue in one
+ loop iteration. *)
+ exception NoIncrement
+
+ (* Adds or subtracts the integer value of [expr] to the current delta
+ [delta.current], according to [binop] which can be PlusA or MinusA.
+ Raises NoIncrement if [expr] is not a constant integer expression. *)
+ let add_to_delta binop delta expr =
+ let typ = Cil.typeOf expr in
+ match Cil.constFoldToInt expr with
+ | None -> raise NoIncrement
+ | Some i ->
+ let value = Val.inject_int typ i in
+ let current = match delta.current with
+ | `Bottom -> `Value value
+ | `Value v -> Val.forward_binop typ binop v value
+ in
+ { delta with current }
+
+ (* Adds to [delta] the increment from the assignement of [lval] to the value
+ of [expr]. Raises NoIncrement if this is not an increment of [lval]. *)
+ let rec delta_assign lval delta expr =
+ (* Is the expression [e] equal to the lvalue [lval] (modulo cast)? *)
+ let rec is_lval e = match e.enode with
+ | Lval lv -> Cil_datatype.LvalStructEq.equal lval lv
+ | CastE (typ, e) -> Cil.isIntegralType typ && is_lval e
+ | Info (e, _) -> is_lval e
+ | _ -> false
+ in
+ match expr.enode with
+ | BinOp ((PlusA | MinusA) as binop, e1, e2, _) ->
+ if is_lval e1
+ then add_to_delta binop delta e2
+ else if is_lval e2 && binop = PlusA
+ then add_to_delta binop delta e1
+ else raise NoIncrement
+ | CastE (typ, e) when Cil.isIntegralType typ -> delta_assign lval delta e
+ | Info (e, _) -> delta_assign lval delta e
+ | _ -> raise NoIncrement
+
+ let delta_instruction lval delta = function
+ | Set (lv, expr, _loc) ->
+ if Cil_datatype.LvalStructEq.equal lval lv
+ then delta_assign lval delta expr
+ else delta
+ | Call (Some lv, _, _, _) ->
+ if Cil_datatype.LvalStructEq.equal lval lv
+ then raise NoIncrement (* No increment can be computed for a call. *)
+ else delta
+ | Call (None, _, _, _) | Local_init _ | Skip _ | Code_annot _ -> delta
+ | Asm _ -> raise NoIncrement
+
+ (* Computes an over-approximation of the increment of [lval] in the block
+ [loop]. Only syntactic assignments of [lval] are considered, so [lval]
+ should be a direct access to a variable whose address is not taken,
+ and which should not be global if the loop contains function calls.
+ Returns None if no increment can be computed. *)
+ let compute_delta lval loop =
+ let rec delta_stmt acc stmt =
+ match stmt.skind with
+ | Instr instr -> delta_instruction lval acc instr
+ | Break _ ->
+ (* No increment, as the statement leaves the loop. *)
+ { current = `Bottom; final = `Bottom }
+ | Continue _ ->
+ (* The current increment becomes the final increment. *)
+ { current = `Bottom; final = final_delta acc }
+ | If (_e, b1, b2, _loc) ->
+ join_delta (delta_block acc b1) (delta_block acc b2)
+ | Block b -> delta_block acc b
+ | _ ->
+ (* For other statements, we only check that they do not modify [lval]. *)
+ if is_safe lval ~loop stmt then acc else raise NoIncrement
+ and delta_block acc block =
+ List.fold_left delta_stmt acc block.bstmts
+ in
+ try
+ let zero_delta = { current = `Value Val.zero; final = `Bottom; } in
+ let delta = delta_block zero_delta loop in
+ final_delta delta >> fun d -> Some d
+ with NoIncrement -> None
+
+ (* Evaluates the lvalue [lval] in the state [state]. Returns None if the value
+ may be undeterminate. *)
+ let evaluate_lvalue state lval =
+ fst (Eval.copy_lvalue state lval) >> fun (_valuation, flagged_value) ->
+ if not flagged_value.initialized || flagged_value.escaping
+ then None
+ else flagged_value.v >> fun v -> Some v
+
+ (* Is the number of iterations of a loop bounded by [limit]?
+ [state] is the loop entry state, and [loop_block] the block of the loop. *)
+ let is_bounded_loop state limit loop_block =
+ (* Computes the effect of the loop. Stops if it contains assembly code. *)
+ loop_effect_visitor#compute_effect loop_block >>= fun loop_effect ->
+ (* Finds the first loop exit condition, or stops. *)
+ find_loop_exit_condition loop_block >>= fun (condition, positive) ->
+ (* Finds the unique integer lvalue modified within the loop in [condition].
+ Stops if it does not exist is not a good candidate for the heuristic. *)
+ find_lonely_candidate loop_effect condition >>= fun lval ->
+ (* Reduce [condition] to a sufficient hypothesis over the [lval] value:
+ if [lval] ∈ [v_exit] then [condition = positive]. *)
+ reduce_to_lval_from_state state lval condition positive >>= fun v_exit ->
+ (* Evaluates the initial value [v_init] of [lval] in the loop entry state. *)
+ evaluate_lvalue state lval >>= fun v_init ->
+ (* Computes an over-approximation [v_delta] of the increment of [lval]
+ in one iteration of the loop. *)
+ compute_delta lval loop_block >>= fun v_delta ->
+ let typ = Cil.typeOfLval lval in
+ let limit = Val.inject_int typ (Integer.of_int limit) in
+ (* Checks whether [v_init] + [limit] × [v_delta] ⊂ [v_exit]. *)
+ let binop op v1 v2 = Bottom.non_bottom (Val.forward_binop typ op v1 v2) in
+ let value = binop PlusA v_init (binop Mult limit v_delta) in
+ Some (Val.is_included value v_exit)
+
+ (* Computes an automatic loop unrolling for statement [stmt] in state [state],
+ with a maximum limit. Returns None for no automatic loop unrolling. *)
+ let compute ~max_unroll state stmt =
+ try
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let loop_stmt = Kernel_function.find_enclosing_loop kf stmt in
+ match loop_stmt.skind with
+ | Loop (_code_annot, block, _loc, _, _) ->
+ is_bounded_loop state max_unroll block >>= fun bounded ->
+ if bounded then Some max_unroll else None
+ | _ -> None
+ with Not_found -> None
+end
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.mli b/src/plugins/value/partitioning/auto_loop_unroll.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e16a7ec2e1d1f7e3567de026e8d35441c9e1cd75
--- /dev/null
+++ b/src/plugins/value/partitioning/auto_loop_unroll.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Heuristic for automatic loop unrolling. *)
+
+module Make (Abstract: Abstractions.Eva) : sig
+
+ val compute:
+ max_unroll:int -> Abstract.Dom.t -> Cil_types.stmt -> int option
+
+end
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/partitioning/partition.ml
similarity index 96%
rename from src/plugins/value/engine/partition.ml
rename to src/plugins/value/partitioning/partition.ml
index 644e3bf20b5a617f34df40a686b12dadabab3bf4..eb378dc20bbd738c1af9512c6a722d57450098c7 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -164,6 +164,7 @@ let to_list (p : 'a partition) : 'a list =
type unroll_limit =
| ExpLimit of Cil_types.exp
| IntLimit of int
+ | AutoUnroll of Cil_types.stmt * int * int
type split_kind = Static | Dynamic
@@ -219,7 +220,11 @@ struct
let union (p1 : t) (p2 : t) : t =
p1 @ p2
- (* --- Evalution and split functions -------------------------------------- *)
+ (* --- Automatic loop unrolling ------------------------------------------- *)
+
+ module AutoLoopUnroll = Auto_loop_unroll.Make (Abstract)
+
+ (* --- Evaluation and split functions ------------------------------------- *)
(* Domains transfer functions. *)
module TF = Abstract.Dom.Transfer (Abstract.Eval.Valuation)
@@ -403,6 +408,14 @@ struct
let limit = try match limit_kind with
| ExpLimit exp -> eval_exp_to_int x exp
| IntLimit i -> i
+ | AutoUnroll (stmt, min_unroll, max_unroll) ->
+ match AutoLoopUnroll.compute ~max_unroll x stmt with
+ | None -> min_unroll
+ | Some i ->
+ Value_parameters.warning ~once:true ~current:true
+ ~wkey:Value_parameters.wkey_loop_unroll
+ "Automatic loop unrolling.";
+ i
with
| Operation_failed -> 0
in
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/partitioning/partition.mli
similarity index 95%
rename from src/plugins/value/engine/partition.mli
rename to src/plugins/value/partitioning/partition.mli
index 2a5177c756849b8abeb1bebb32e939066a11374f..cf1c7426b1d5a4dffcf9f10ce5b9278579ca45a9 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -76,12 +76,16 @@ type rationing
(** Creates a new rationing, that can be used successively on several flows. *)
val new_rationing: limit:int -> merge:bool -> rationing
-(** The unroll limit of a loop can be specified as an integer, or as a C
- expression, which is evaluated when entering the loop in each incoming
- state. The expression must always evaluate to a singleton integer. *)
+(** The unroll limit of a loop. *)
type unroll_limit =
| ExpLimit of Cil_types.exp
+ (** Value of the expression for each incoming state. The expression must
+ evaluate to a singleton integer in each state. *)
| IntLimit of int
+ (** Integer limit. *)
+ | AutoUnroll of Cil_types.stmt * int * int
+ (** [AutoUnroll(stmt, min, max)] requests to find a "good" unrolling limit
+ between [min] and [max] for the loop [stmt]. *)
(** Splits on an expression can be static or dynamic:
- static splits are processed once: the expression is only evaluated at the
diff --git a/src/plugins/value/engine/partitioning_index.ml b/src/plugins/value/partitioning/partitioning_index.ml
similarity index 100%
rename from src/plugins/value/engine/partitioning_index.ml
rename to src/plugins/value/partitioning/partitioning_index.ml
diff --git a/src/plugins/value/engine/partitioning_index.mli b/src/plugins/value/partitioning/partitioning_index.mli
similarity index 100%
rename from src/plugins/value/engine/partitioning_index.mli
rename to src/plugins/value/partitioning/partitioning_index.mli
diff --git a/src/plugins/value/engine/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
similarity index 95%
rename from src/plugins/value/engine/partitioning_parameters.ml
rename to src/plugins/value/partitioning/partitioning_parameters.ml
index b480f4e425da2b3ce6f1dd62384c0ffd326a1151..33ad321a5cba2cdbbf4c053b7f77fb153a91656b 100644
--- a/src/plugins/value/engine/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -58,7 +58,7 @@ struct
!Db.Properties.Interp.term_to_exp ~result:None term
let min_loop_unroll = MinLoopUnroll.get ()
-
+ let auto_loop_unroll = AutoLoopUnroll.get ()
let default_loop_unroll = DefaultLoopUnroll.get ()
let warn_no_loop_unroll stmt =
@@ -76,7 +76,11 @@ struct
"%s loop without unroll annotation" loop_kind
let unroll stmt =
- let default = Partition.IntLimit min_loop_unroll in
+ let default =
+ if auto_loop_unroll > min_loop_unroll
+ then Partition.AutoUnroll (stmt, min_loop_unroll, auto_loop_unroll)
+ else Partition.IntLimit min_loop_unroll
+ in
match get_unroll_annot stmt with
| [] -> warn_no_loop_unroll stmt; default
| [None] -> Partition.IntLimit default_loop_unroll
diff --git a/src/plugins/value/engine/partitioning_parameters.mli b/src/plugins/value/partitioning/partitioning_parameters.mli
similarity index 100%
rename from src/plugins/value/engine/partitioning_parameters.mli
rename to src/plugins/value/partitioning/partitioning_parameters.mli
diff --git a/src/plugins/value/slevel/per_stmt_slevel.ml b/src/plugins/value/partitioning/per_stmt_slevel.ml
similarity index 100%
rename from src/plugins/value/slevel/per_stmt_slevel.ml
rename to src/plugins/value/partitioning/per_stmt_slevel.ml
diff --git a/src/plugins/value/slevel/per_stmt_slevel.mli b/src/plugins/value/partitioning/per_stmt_slevel.mli
similarity index 100%
rename from src/plugins/value/slevel/per_stmt_slevel.mli
rename to src/plugins/value/partitioning/per_stmt_slevel.mli
diff --git a/src/plugins/value/engine/split_return.ml b/src/plugins/value/partitioning/split_return.ml
similarity index 100%
rename from src/plugins/value/engine/split_return.ml
rename to src/plugins/value/partitioning/split_return.ml
diff --git a/src/plugins/value/engine/split_return.mli b/src/plugins/value/partitioning/split_return.mli
similarity index 100%
rename from src/plugins/value/engine/split_return.mli
rename to src/plugins/value/partitioning/split_return.mli
diff --git a/src/plugins/value/slevel/split_strategy.ml b/src/plugins/value/partitioning/split_strategy.ml
similarity index 100%
rename from src/plugins/value/slevel/split_strategy.ml
rename to src/plugins/value/partitioning/split_strategy.ml
diff --git a/src/plugins/value/slevel/split_strategy.mli b/src/plugins/value/partitioning/split_strategy.mli
similarity index 100%
rename from src/plugins/value/slevel/split_strategy.mli
rename to src/plugins/value/partitioning/split_strategy.mli
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
similarity index 100%
rename from src/plugins/value/engine/trace_partitioning.ml
rename to src/plugins/value/partitioning/trace_partitioning.ml
diff --git a/src/plugins/value/engine/trace_partitioning.mli b/src/plugins/value/partitioning/trace_partitioning.mli
similarity index 100%
rename from src/plugins/value/engine/trace_partitioning.mli
rename to src/plugins/value/partitioning/trace_partitioning.mli
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 0f972433fe475cecf2c6f1a3981bafea11ed233f..cb768383cb9b97233cb24d3f48c4fe5ba8e1b3e6 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -812,6 +812,20 @@ module MinLoopUnroll =
let () = add_precision_dep MinLoopUnroll.parameter
let () = MinLoopUnroll.set_range 0 max_int
+let () = Parameter_customize.set_group precision_tuning
+module AutoLoopUnroll =
+ Int
+ (struct
+ let option_name = "-eva-auto-loop-unroll"
+ let arg_name = "n"
+ let default = 0
+ let help = "limit of the automatic loop unrolling: all loops whose \
+ number of iterations can be easily bounded by <n> \
+ are completely unrolled."
+ end)
+let () = add_precision_dep AutoLoopUnroll.parameter
+let () = AutoLoopUnroll.set_range 0 max_int
+
let () = Parameter_customize.set_group precision_tuning
module DefaultLoopUnroll =
Int
@@ -1532,6 +1546,7 @@ let get array n = if n < 0 then 0 else array.(n)
let () =
bind (module MinLoopUnroll) (fun n -> max 0 (n - 4));
+ bind (module AutoLoopUnroll) (fun n -> if n = 0 then 0 else 4 lsl n);
bind (module SemanticUnrollingLevel) (get slevel_power);
bind (module WideningDelay) (fun n -> 1 + n / 2);
bind (module ILevel) (get ilevel_power);
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8cda781691b11799c8f0277f35bab8803cc53206..7ead8310a01f463bd9cd8f75d995a2ecce1af21a 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -93,6 +93,7 @@ module SlevelFunction:
module SlevelMergeAfterLoop: Parameter_sig.Kernel_function_set
module MinLoopUnroll : Parameter_sig.Int
+module AutoLoopUnroll : Parameter_sig.Int
module DefaultLoopUnroll : Parameter_sig.Int
module HistoryPartitioning : Parameter_sig.Int
module ValuePartitioning : Parameter_sig.String_set
diff --git a/tests/impact/depend5.i b/tests/impact/depend5.i
index fcae6034c68e975b5cd0c0712356523269a25e33..52b560fbce0feb000e1bab6d409c7d022216c822 100644
--- a/tests/impact/depend5.i
+++ b/tests/impact/depend5.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-calldeps -then -impact-pragma g"
+ STDOPT: #"@EVA_OPTIONS@ -calldeps -then -impact-pragma g"
*/
int a, b, c, d, e;
diff --git a/tests/impact/oracle/depend5.res.oracle b/tests/impact/oracle/depend5.res.oracle
index 415d327aa48e2ce9f2a753cf94e0667a2ea0b345..f75abc0f8070015f2b9e02de9243b93be8905853 100644
--- a/tests/impact/oracle/depend5.res.oracle
+++ b/tests/impact/oracle/depend5.res.oracle
@@ -8,26 +8,28 @@
c ∈ {0}
d ∈ {0}
e ∈ {0}
+[eva] computing for function f <- main.
+ Called from tests/impact/depend5.i:23.
+[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
+[eva] Done for function f
+[eva] computing for function g <- main.
+ Called from tests/impact/depend5.i:25.
+[eva] computing for function f <- g <- main.
+ Called from tests/impact/depend5.i:18.
+[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
+[eva] Done for function f
+[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
+[eva] Done for function g
+[eva] Recording results for main
[from] Computing for function main
[from] Done for function main
[eva] done for function main
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 3 functions analyzed (out of 3): 100% coverage.
- In these functions, 13 statements reached (out of 13): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 0 alarms generated by the analysis.
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to f at tests/impact/depend5.i:18 (by g):
b FROM a; e
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index e08f72217afc5872f078df8e68ece4bf9bd9d130..1f733301b5c7942857df1515ef02528852f4a8bf 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,11 +1,11 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva -out -input -deps -eva-show-progress ./@PTEST_DIR@/@PTEST_NAME@.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
- EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav @PTEST_DIR@/@PTEST_NAME@.i -eva -out -input -deps -eva-show-progress > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
- STDOPT: +"-load ./tests/saveload/result/basic.sav -eva -out -input -deps -journal-disable"
+ EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./@PTEST_DIR@/@PTEST_NAME@.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
+ EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav @PTEST_DIR@/@PTEST_NAME@.i -eva @EVA_OPTIONS@ -out -input -deps > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
+ STDOPT: +"-load ./tests/saveload/result/basic.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva -out -input -deps -journal-disable -print"
- STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva -out -input -deps -journal-disable"
+ STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print"
+ STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
EXECNOW: make -s @PTEST_DIR@/status.cmxs
EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-module @PTEST_DIR@/status -save ./tests/saveload/result/status.sav @PTEST_DIR@/@PTEST_NAME@.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
STDOPT: +"-load-module @PTEST_DIR@/status -load ./tests/saveload/result/status.sav"
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index 5453ccfe23850403af7beb11fbc4ed95c3ce6534..5f757c7f0cf39a6306df9054d570f2ef8bb52c8f 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/bool.sav -eva -eva-show-progress ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
+ EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/bool.sav -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
STDOPT: +"-load ./tests/saveload/result/bool.sav -out -input -deps"
- STDOPT: +"-load ./tests/saveload/result/bool.sav -eva"
+ STDOPT: +"-load ./tests/saveload/result/bool.sav -eva @EVA_OPTIONS@"
*/
#include "stdbool.h"
diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i
index 1e7dddc3a3c06bda23bc341a1df1a8b95e3d7922..ee704399b403bbf61ee9da3eab241d193b7a9426 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s ./tests/saveload/deps_A.cmxs ./tests/saveload/deps_B.cmxs ./tests/saveload/deps_C.cmxs ./tests/saveload/deps_D.cmxs ./tests/saveload/deps_E.cmxs
- EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module ./tests/saveload/deps_A.cmxs -eva -out -input -deps -eva-show-progress ./tests/saveload/deps.i -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err
- STDOPT: +"-load-module ./tests/saveload/deps_A -load ./tests/saveload/result/deps.sav -eva -out -input -deps "
+ EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module ./tests/saveload/deps_A.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/deps.i -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err
+ STDOPT: +"-load-module ./tests/saveload/deps_A -load ./tests/saveload/result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps "
STDOPT: +"-load-module ./tests/saveload/deps_B -load ./tests/saveload/result/deps.sav -out -input -deps "
STDOPT: +"-load-module ./tests/saveload/deps_C -load ./tests/saveload/result/deps.sav -out -input -deps "
STDOPT: +"-load-module ./tests/saveload/deps_D -load ./tests/saveload/result/deps.sav -out -input -deps "
diff --git a/tests/saveload/isset.c b/tests/saveload/isset.c
index e490c3405e835d7c65980bd84767a42dd5f47449..720c3d635f2f3bc362c24fe83422bf51766ddfa6 100644
--- a/tests/saveload/isset.c
+++ b/tests/saveload/isset.c
@@ -1,9 +1,9 @@
/* run.config
- EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav ./bin/toplevel.opt -quiet -eva -save tests/saveload/result/isset.sav tests/saveload/isset.c > ./tests/saveload/result/isset_sav.res 2> ./tests/saveload/result/isset_sav.err
+ EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav ./bin/toplevel.opt -quiet -eva @EVA_OPTIONS@ -save tests/saveload/result/isset.sav tests/saveload/isset.c > ./tests/saveload/result/isset_sav.res 2> ./tests/saveload/result/isset_sav.err
STDOPT: +"-quiet -load ./tests/saveload/result/isset.sav"
STDOPT: +"-load ./tests/saveload/result/isset.sav"
- STDOPT: +"-eva -load ./tests/saveload/result/isset.sav"
- STDOPT: +"-quiet -eva -load ./tests/saveload/result/isset.sav"
+ STDOPT: +"-eva @EVA_OPTIONS@ -load ./tests/saveload/result/isset.sav"
+ STDOPT: +"-quiet -eva @EVA_OPTIONS@ -load ./tests/saveload/result/isset.sav"
*/
int main() {
diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i
index 3a98905ee05a858635d65a496b77f0e75e664535..ab0d9a44fd15de6c80394627618705578bd54744 100644
--- a/tests/saveload/multi_project.i
+++ b/tests/saveload/multi_project.i
@@ -1,9 +1,9 @@
/* run.config
- EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/multi_project.sav -eva-show-progress -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
+ EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
STDOPT: +"-load ./tests/saveload/result/multi_project.sav -journal-disable"
CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -eva -eva-show-progress
+ OPT: -eva @EVA_OPTIONS@
*/
int f(int x) {
return x + x;
diff --git a/tests/saveload/oracle/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res
index d2c84cb5472a81605ccd30aad3736fefb3012431..056059606204259f47c4619d6aa71f6dd14adaa0 100644
--- a/tests/saveload/oracle/basic_sav.1.res
+++ b/tests/saveload/oracle/basic_sav.1.res
@@ -15,21 +15,6 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 12 statements reached (out of 12): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 1 valid 0 unknown 0 invalid 1 total
- Preconditions 0 valid 0 unknown 0 invalid 0 total
- 100% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res
index d2c84cb5472a81605ccd30aad3736fefb3012431..056059606204259f47c4619d6aa71f6dd14adaa0 100644
--- a/tests/saveload/oracle/basic_sav.res
+++ b/tests/saveload/oracle/basic_sav.res
@@ -15,21 +15,6 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 12 statements reached (out of 12): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 1 valid 0 unknown 0 invalid 1 total
- Preconditions 0 valid 0 unknown 0 invalid 0 total
- 100% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/bool_sav.res b/tests/saveload/oracle/bool_sav.res
index 42cfadd177d9795b61e0ab5ef909a7f2ab78dc5c..91b80def8d2d6316bebfd69690759d3c1442a3d0 100644
--- a/tests/saveload/oracle/bool_sav.res
+++ b/tests/saveload/oracle/bool_sav.res
@@ -54,18 +54,3 @@
x ∈ {1}
y ∈ {2}
S___fc_stdout[0..1] ∈ [--..--]
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 2 functions analyzed (out of 2): 100% coverage.
- In these functions, 24 statements reached (out of 24): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 1 valid 0 unknown 0 invalid 1 total
- Preconditions 5 valid 0 unknown 0 invalid 5 total
- 100% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
diff --git a/tests/saveload/oracle/deps_sav.res b/tests/saveload/oracle/deps_sav.res
index c52779de1ee27f18ae17e8ab60348d97820dbefe..40f9aeda11453a63ab6d1a1c2a1b0b9083ec2cbe 100644
--- a/tests/saveload/oracle/deps_sav.res
+++ b/tests/saveload/oracle/deps_sav.res
@@ -14,18 +14,6 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 11 statements reached (out of 11): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/multi_project.1.res.oracle b/tests/saveload/oracle/multi_project.1.res.oracle
index 1ca91d867296f076e2a0a71a83f86eddebc8b32a..1cd5eaed301e7605d863fc6f45aa6e8ca1326a5a 100644
--- a/tests/saveload/oracle/multi_project.1.res.oracle
+++ b/tests/saveload/oracle/multi_project.1.res.oracle
@@ -18,20 +18,6 @@
x ∈ {2}
y ∈ {4}
__retres ∈ {8}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 2 functions analyzed (out of 2): 100% coverage.
- In these functions, 7 statements reached (out of 7): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 0 alarms generated by the analysis.
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 1 valid 0 unknown 0 invalid 1 total
- Preconditions 0 valid 0 unknown 0 invalid 0 total
- 100% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
[kernel] Checking "foo"
[kernel] Checking "foobar"
[kernel] Checking "default"
diff --git a/tests/saveload/oracle/multi_project_sav.res b/tests/saveload/oracle/multi_project_sav.res
index 6968a8ec6bec3d45c4bafa4c62f29beab29467df..c6cb667f22790752799c6073a046dd5a4f4d07a2 100644
--- a/tests/saveload/oracle/multi_project_sav.res
+++ b/tests/saveload/oracle/multi_project_sav.res
@@ -12,20 +12,6 @@
[eva] tests/saveload/multi_project.i:15: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 2 functions analyzed (out of 2): 100% coverage.
- In these functions, 7 statements reached (out of 7): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 0 alarms generated by the analysis.
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 1 valid 0 unknown 0 invalid 1 total
- Preconditions 0 valid 0 unknown 0 invalid 0 total
- 100% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
/* Generated by Frama-C */
int f(int x)
{
diff --git a/tests/saveload/oracle/segfault_datatypes_sav.res b/tests/saveload/oracle/segfault_datatypes_sav.res
index 1cf0a3182aa799855b6b8135f9bfc4bcc08f6746..a67d19e53c35d8b2b99e4d14186c88dd929a4f51 100644
--- a/tests/saveload/oracle/segfault_datatypes_sav.res
+++ b/tests/saveload/oracle/segfault_datatypes_sav.res
@@ -14,18 +14,6 @@
i ∈ [-2147483648..9]
j ∈ {5}
__retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 11 statements reached (out of 11): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/segfault_datatypes.i b/tests/saveload/segfault_datatypes.i
index 0e64333dd66e888dfbe6f51bc17a9c3f820de664..7d6c97c42832cdb0edb6beadd038443b9e925186 100644
--- a/tests/saveload/segfault_datatypes.i
+++ b/tests/saveload/segfault_datatypes.i
@@ -1,8 +1,8 @@
/* run.config
EXECNOW: make -s ./tests/saveload/segfault_datatypes_A.cmxs ./tests/saveload/segfault_datatypes_B.cmxs
- EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -load-module ./tests/saveload/segfault_datatypes_A -eva -out -input -deps ./tests/saveload/segfault_datatypes.i -eva-show-progress -save ./tests/saveload/result/segfault_datatypes.sav > ./tests/saveload/result/segfault_datatypes_sav.res 2> ./tests/saveload/result/segfault_datatypes_sav.err
+ EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -load-module ./tests/saveload/segfault_datatypes_A -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/segfault_datatypes.i -save ./tests/saveload/result/segfault_datatypes.sav > ./tests/saveload/result/segfault_datatypes_sav.res 2> ./tests/saveload/result/segfault_datatypes_sav.err
CMD: @frama-c@ -load-module ./tests/saveload/segfault_datatypes_B
- STDOPT: +"-load ./tests/saveload/result/segfault_datatypes.sav -eva -out -input -deps -journal-disable"
+ STDOPT: +"-load ./tests/saveload/result/segfault_datatypes.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
*/
diff --git a/tests/test_config b/tests/test_config
index 6efe608ac844b6bfd35b978ccf9915ef6adab07f..3349a7b04de557ca065dddc3267824bed2662dbb 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index 2d6cff1926f6598e15c22f97ede264377dedf042..f2cc7c99925549ed501f9c2920742c71f2896639 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-apron-oct -eva-msg-key experimental-ok
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-apron-oct -eva-msg-key experimental-ok
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 7e1be236655fdf63e47056f790c1e3c9b30dcdb0..78b3b47c351dd5164adf860a4276680135700ccb 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-bitwise-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-bitwise-domain
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_equalities b/tests/test_config_equalities
index d84a7e2a8b21674dad528c1927b0630aa948a2f3..c386ea89a05c577a7ce1ca5f9a01308c1b02948a 100644
--- a/tests/test_config_equalities
+++ b/tests/test_config_equalities
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-equality-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-equality-domain
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index b6a460ae1e45ec4c85dc60eb2a4851b6d84f63b7..bc7593f4e6be173da86718fce2727ad8c60be77e 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-gauges-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-gauges-domain
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index 47ce23088d402b091d071c21699c8fb9d4f7f268..8cbbc295b177df03ddd9d2655b1bba2d2e68acde 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-symbolic-locations-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-symbolic-locations-domain
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
new file mode 100644
index 0000000000000000000000000000000000000000..d3a1a1ce141f3d23490482ee26cd1bd80b54995b
--- /dev/null
+++ b/tests/value/auto_loop_unroll.c
@@ -0,0 +1,192 @@
+/* run.config*
+ STDOPT: +"-eva-auto-loop-unroll 10"
+ STDOPT: +"-eva-auto-loop-unroll 128"
+*/
+
+/* Tests the automatic loop unrolling heuristic. */
+
+#include <__fc_builtin.h>
+
+volatile int undet;
+
+int g = 0;
+void incr_g () {
+ g++;
+}
+
+int incr (int i) {
+ return i+1;
+}
+
+void simple_loops () {
+ int res = 0;
+ /* This loop should be automatically unrolled on the second run. */
+ for (int i = 0; i < 100; i++) {
+ res++;
+ }
+ Frama_C_show_each_auto(res);
+ res = 0;
+ /* This loop should not be automatically unrolled. */
+ for (int i = 0; i < 1000; i++) {
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* The annotation has priority over the automatic loop unrolling:
+ this loop should never be unrolled. */
+ /*@ loop unroll 0; */
+ for (int i = 0; i < 100; i++) {
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* The annnotation has priority over the automatic loop unrolling:
+ this loop should always be unrolled. */
+ /*@ loop unroll 100; */
+ for (int i = 0; i < 100; i++) {
+ res++;
+ }
+ Frama_C_show_each_singleton(res);
+}
+
+/* Examples of various loops that should be automatically unrolled
+ on the second run, but not on the first. */
+void various_loops () {
+ int res = 0;
+ /* Decreasing loop counter. */
+ for (int i = 64; i > 0; i--)
+ res++;
+ Frama_C_show_each_64(res);
+ res = 0;
+ /* Decrements the loop counter by 3. */
+ for (int i = 120; i > 0; i -= 3)
+ res++;
+ Frama_C_show_each_40(res);
+ res = 0;
+ /* Several increments of the loop counter. */
+ for (int i = 0; i < 160; i++) {
+ i += 2;
+ res++;
+ i--;
+ }
+ Frama_C_show_each_80(res);
+ res = 0;
+ /* Random increments of the loop counter. */
+ for (int i = 0; i < 160;) {
+ res++;
+ if (undet)
+ i += 2;
+ else
+ i += 5;
+ }
+ Frama_C_show_each_32_80(res);
+ res = 0;
+ /* Other loop breaking condition. */
+ for (int i = 0; i < 111; i++) {
+ res++;
+ if (undet && res > 10)
+ break;
+ }
+ Frama_C_show_each_11_111(res);
+ res = 0;
+ /* More complex loop condition. */
+ int x = 24;
+ int k = Frama_C_interval(0, 10);
+ for (int i = 75; i + x > 2 * k; i -= 2)
+ res++;
+ Frama_C_show_each_40_50(res);
+ res = 0;
+ /* Loop calling some functions that do not modify the loop counter. */
+ for (int i = 0; i < 25; i++) {
+ incr_g();
+ int t = incr(i);
+ res = incr(res);
+ }
+ Frama_C_show_each_25(res);
+ res = 0;
+ /* Nested loops. */
+ res = 0;
+ for (int i = 0; i < 16; i++) {
+ for (int j = 0; j < i; j++) {
+ res++;
+ }
+ }
+ Frama_C_show_each_120(res);
+ res = 0;
+}
+
+/* Loops that cannot be unrolled. */
+void complex_loops () {
+ /* Loop counter modified through a pointer. */
+ int res = 0;
+ int i = 0;
+ int *p = &i;
+ while (i < 64) {
+ (*p)++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ /* Loop counter modified within a nested loop. */
+ res = 0;
+ i = 0;
+ while (i < 64) {
+ for (int j = 0; j < i; j++) {
+ i++;
+ }
+ res++;
+ i++;
+ }
+ Frama_C_show_each_imprecise(res);
+ /* Loop counter incremented under a condition. */
+ res = 0;
+ i = 0;
+ while (i < 10) {
+ if (undet)
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ i = 0;
+ while (i < 10) {
+ if (undet)
+ i++;
+ else
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ /* Loop counter modified by a function. */
+ res = 0;
+ g = 0;
+ while (g < 64) {
+ incr_g();
+ g++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* Too complex loop condition. */
+ int t[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+ i = 0;
+ while (t[i] < 6) {
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+ res = 0;
+ /* Random loop condition. */
+ i = 0;
+ while (i < 64 && undet) {
+ i++;
+ res++;
+ }
+ Frama_C_show_each_imprecise(res);
+}
+
+
+void main () {
+ simple_loops ();
+ various_loops ();
+ complex_loops ();
+}
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..359bdb60f2fc65fdc7521795c3637c8ef6d68cbd
--- /dev/null
+++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle
@@ -0,0 +1,297 @@
+[kernel] Parsing tests/value/auto_loop_unroll.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ undet ∈ [--..--]
+ g ∈ {0}
+[eva] computing for function simple_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:189.
+[eva] tests/value/auto_loop_unroll.c:24: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:25: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:30: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:33:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:38: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:41:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:46:
+ Trace partitioning superposing up to 100 states
+[eva] tests/value/auto_loop_unroll.c:49: Frama_C_show_each_singleton: {100}
+[eva] Recording results for simple_loops
+[eva] Done for function simple_loops
+[eva] computing for function various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:190.
+[eva] tests/value/auto_loop_unroll.c:57: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:58: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:62: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:63: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:67: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:69: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:75: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:76: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:82:
+ Frama_C_show_each_32_80: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:85: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:86: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:90:
+ Frama_C_show_each_11_111: [0..2147483647]
+[eva] computing for function Frama_C_interval <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:94.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/auto_loop_unroll.c:94:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/auto_loop_unroll.c:95: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:96: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:97:
+ Frama_C_show_each_40_50: [0..2147483647]
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:100: starting to merge loop iterations
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva:alarm] tests/value/auto_loop_unroll.c:14: Warning:
+ signed overflow. assert g + 1 ≤ 2147483647;
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:103.
+[eva:alarm] tests/value/auto_loop_unroll.c:18: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:109: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:110: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:111: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: [0..2147483647]
+[eva] Recording results for various_loops
+[eva] Done for function various_loops
+[eva] computing for function complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:191.
+[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:128:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:139:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:148:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:158:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:167:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:176:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:184:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] Recording results for complex_loops
+[eva] Done for function complex_loops
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function incr:
+ __retres ∈ [1..2147483647]
+[eva:final-states] Values at end of function incr_g:
+ g ∈ [1..2147483647]
+[eva:final-states] Values at end of function complex_loops:
+ g ∈ {64}
+ res ∈ [0..2147483647]
+ i ∈ [0..64]
+ p ∈ {{ &i }}
+ t[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {3}
+ [4] ∈ {4}
+ [5] ∈ {5}
+ [6] ∈ {6}
+ [7] ∈ {7}
+ [8] ∈ {8}
+ [9] ∈ {9}
+[eva:final-states] Values at end of function simple_loops:
+ res ∈ {100}
+[eva:final-states] Values at end of function various_loops:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ [0..2147483647]
+ res ∈ {0}
+ x ∈ {24}
+ k ∈ [0..10]
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ {64}
+[from] Computing for function incr
+[from] Done for function incr
+[from] Computing for function incr_g
+[from] Done for function incr_g
+[from] Computing for function complex_loops
+[from] Done for function complex_loops
+[from] Computing for function simple_loops
+[from] Done for function simple_loops
+[from] Computing for function various_loops
+[from] Computing for function Frama_C_interval <-various_loops
+[from] Done for function Frama_C_interval
+[from] Done for function various_loops
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function incr:
+ \result FROM i
+[from] Function incr_g:
+ g FROM g
+[from] Function complex_loops:
+ g FROM \nothing
+[from] Function simple_loops:
+ NO EFFECTS
+[from] Function various_loops:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM g (and SELF)
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function incr:
+ __retres
+[inout] Inputs for function incr:
+ \nothing
+[inout] Out (internal) for function incr_g:
+ g
+[inout] Inputs for function incr_g:
+ g
+[inout] Out (internal) for function complex_loops:
+ g; res; i; p; j; t[0..9]
+[inout] Inputs for function complex_loops:
+ undet; g
+[inout] Out (internal) for function simple_loops:
+ res; i; i_0; i_1; i_2
+[inout] Inputs for function simple_loops:
+ \nothing
+[inout] Out (internal) for function various_loops:
+ Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5;
+ t; i_6; j
+[inout] Inputs for function various_loops:
+ Frama_C_entropy_source; undet; g
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; g
+[inout] Inputs for function main:
+ Frama_C_entropy_source; undet; g
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..775a7323bf9b696e565c5de92ee3cf0bbbcbeda7
--- /dev/null
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -0,0 +1,431 @@
+[kernel] Parsing tests/value/auto_loop_unroll.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ undet ∈ [--..--]
+ g ∈ {0}
+[eva] computing for function simple_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:189.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:24: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:24:
+ Trace partitioning superposing up to 100 states
+[eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: {100}
+[eva] tests/value/auto_loop_unroll.c:30: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:33:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:38: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:41:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:49: Frama_C_show_each_singleton: {100}
+[eva] Recording results for simple_loops
+[eva] Done for function simple_loops
+[eva] computing for function various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:190.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:57: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:62: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: {40}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:67: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: {80}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:75: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:75:
+ Trace partitioning superposing up to 100 states
+[eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [32..80]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:85: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:90: Frama_C_show_each_11_111: [11..111]
+[eva] computing for function Frama_C_interval <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:94.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/auto_loop_unroll.c:94:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:95: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:97: Frama_C_show_each_40_50: [40..50]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:100: Automatic loop unrolling.
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] computing for function incr_g <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:101.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr <- various_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:102.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: {25}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:109: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: {120}
+[eva] Recording results for various_loops
+[eva] Done for function various_loops
+[eva] computing for function complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:191.
+[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:128:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning:
+ signed overflow. assert i + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:139:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:148:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:158:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] computing for function incr_g <- complex_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:163.
+[eva] Recording results for incr_g
+[eva] Done for function incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:167:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:176:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:184:
+ Frama_C_show_each_imprecise: [0..2147483647]
+[eva] Recording results for complex_loops
+[eva] Done for function complex_loops
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function incr:
+ __retres ∈ [1..25]
+[eva:final-states] Values at end of function incr_g:
+ g ∈ [1..63]
+[eva:final-states] Values at end of function complex_loops:
+ g ∈ {64}
+ res ∈ [0..2147483647]
+ i ∈ [0..64]
+ p ∈ {{ &i }}
+ t[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {3}
+ [4] ∈ {4}
+ [5] ∈ {5}
+ [6] ∈ {6}
+ [7] ∈ {7}
+ [8] ∈ {8}
+ [9] ∈ {9}
+[eva:final-states] Values at end of function simple_loops:
+ res ∈ {100}
+[eva:final-states] Values at end of function various_loops:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ {25}
+ res ∈ {0}
+ x ∈ {24}
+ k ∈ [0..10]
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ g ∈ {64}
+[from] Computing for function incr
+[from] Done for function incr
+[from] Computing for function incr_g
+[from] Done for function incr_g
+[from] Computing for function complex_loops
+[from] Done for function complex_loops
+[from] Computing for function simple_loops
+[from] Done for function simple_loops
+[from] Computing for function various_loops
+[from] Computing for function Frama_C_interval <-various_loops
+[from] Done for function Frama_C_interval
+[from] Done for function various_loops
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function incr:
+ \result FROM i
+[from] Function incr_g:
+ g FROM g
+[from] Function complex_loops:
+ g FROM \nothing
+[from] Function simple_loops:
+ NO EFFECTS
+[from] Function various_loops:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM g (and SELF)
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ g FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function incr:
+ __retres
+[inout] Inputs for function incr:
+ \nothing
+[inout] Out (internal) for function incr_g:
+ g
+[inout] Inputs for function incr_g:
+ g
+[inout] Out (internal) for function complex_loops:
+ g; res; i; p; j; t[0..9]
+[inout] Inputs for function complex_loops:
+ undet; g
+[inout] Out (internal) for function simple_loops:
+ res; i; i_0; i_1; i_2
+[inout] Inputs for function simple_loops:
+ \nothing
+[inout] Out (internal) for function various_loops:
+ Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5;
+ t; i_6; j
+[inout] Inputs for function various_loops:
+ Frama_C_entropy_source; undet; g
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; g
+[inout] Inputs for function main:
+ Frama_C_entropy_source; undet; g