diff --git a/Changelog b/Changelog
index 65f7db922aecdc1a77d11359a81e8627262b66f4..8c9a705d3c372b62fee986ca97d723c021c62eec 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,12 @@
Open Source Release <next-release>
##################################
+- 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
+ pairs of scalar variables occuring in a same instruction.
+ Intra-procedural by default; octagons can be propagated through
+ function calls with option -eva-octagon-through-calls.
- Eva [2019/10/04] Evaluates ACSL predicates \is_plus_infinity and
\is_minus_infinity.
- Kernel [2019/10/04] Supports macro INFINITY and NAN.
diff --git a/Makefile b/Makefile
index 476d1807b2c22731957fd4d801361f45cbd6671b..8b6f552a87882d2d156af1737917172b03ee522b 100644
--- a/Makefile
+++ b/Makefile
@@ -875,6 +875,7 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
domains/printer_domain \
domains/traces_domain \
domains/simple_memory \
+ domains/octagons \
domains/gauges/gauges_domain \
domains/hcexprs \
domains/equality/equality domains/equality/equality_domain \
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 8a8ef8917377f732c9ad306cc8a44e66b110f564..2cc8c362d514faeb329df932c57bb06fac788a5a 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3956,6 +3956,55 @@ while (--x > 0) {
cannot be analyzed precisely, because the relation between \texttt{x}
and \texttt{y} is not affine.
+
+\subsection{Octagons}
+\label{sec:octagons}
+
+Activating option \texttt{-eva-octagon-domain} instructs Eva to infer relations
+between variables as numerical constraints of the form $l \leq \pm X \pm Y \leq
+u$, where $X$ and $Y$ are program variables, and $l$ and $u$ are constants.
+
+These relations are then used to evaluate more precisely the possible values
+of an expression involving $X$ and $Y$, or to deduce a reduction of
+the possible values of $X$ from a reduction of the possible values of $Y$.
+
+The following code is a minimal working example that illustrates
+the precision improvement provided by the octagon domain.
+\begin{lstlisting}
+void main (int y) {
+ int k = Frama_C_interval(0, 10);
+ int x = y + k; // x - y $\in$ [0..10]
+ int r = x + 3 - y; // r $\in$ [-7..3]
+ int t;
+ if (y > 15)
+ t = x; // t $\in$ [6..$\infty$]
+}
+\end{lstlisting}
+
+
+Currently, the octagon domain is fast but has two strong limitations:
+\begin{itemize}
+\item
+ The domain only infers relations between scalar variables of integer types.
+ It ignores pointers, arrays and structure fields.
+\item
+ The domain only infers relations between pairs of variables occurring in the
+ same instruction, as \lstinline|x = y + k;| or \lstinline|if (x < y + k)|.
+ If an instruction involves 3 variables or more, relations are inferred for
+ each pair of variables.
+\end{itemize}
+
+The domain is intraprocedural by default: the inferred relations are local to
+the current function and are lost when entering a function call or returning
+to its caller.
+
+The option \verb+-eva-octagon-through-calls+ makes the octagon domain
+interprocedural, which is a more precise but slower mode where
+the inferred relations are propagated through function calls.
+The analysis of a function can then use the relations inferred in the callers,
+and at the end, the inferred relations are propagated back to the caller.
+
+
\subsection{Bitwise values}
\label{sec:bitwise}
@@ -5044,6 +5093,9 @@ of the domain, shown in Figure~\ref{fig:log-category}.
Gauges & \lstinline|d-gauges| & \ref{sec:gauges}
\tabularnewline
\midrule
+ Octagons & \lstinline|d-octagon| & \ref{sec:octagons}
+ \tabularnewline
+ \midrule
Bitwise & \lstinline|d-bitwise| & \ref{sec:bitwise}
\tabularnewline
\midrule
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 2a853e3bc043d0fd819edf2781f28103c9a441b2..e411e9b106f983a77f99baca0fcb6e8cbd697b85 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1189,6 +1189,8 @@ src/plugins/value/domains/hcexprs.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/hcexprs.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/inout_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/inout_domain.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/octagons.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/octagons.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/offsm_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/offsm_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/powerset.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
new file mode 100644
index 0000000000000000000000000000000000000000..48734821cf4f4e84353625637dc78310bdd4b867
--- /dev/null
+++ b/src/plugins/value/domains/octagons.ml
@@ -0,0 +1,1323 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Eval
+
+(* If [true], checks invariants of the states created by most functions. *)
+let debug = false
+
+(* Whether the domain infers non-relational intervals (ivals) to improve the
+ precision of the join operation: this avoids losing all relations that have
+ been inferred in only one side of the join. Enhances the domain accuracy
+ for a minimal drop in efficiency. *)
+let infer_intervals = true
+
+(* Whether the domain saturates the octagons: from a relation between (x, y)
+ and a relation between (y, z), infers the relation between (x, z).
+ The saturation is currently partial. Improves the domain accuracy for a
+ minimal drop in efficiency. *)
+let saturate_octagons = true
+
+(* Is the domain intraprocedural, according to the -eva-octagon-through-calls
+ option. In this case, the analysis of each function starts with an empty
+ state, and the relations inferred in a function are not propagated back to
+ the caller either. *)
+let intraprocedural () = not (Value_parameters.OctagonCall.get ())
+
+(* -------------------------------------------------------------------------- *)
+(* Basic types: pair of variables and Ival.t *)
+(* -------------------------------------------------------------------------- *)
+
+(* Variables of the octagons. Should be extended later to also include
+ symbolic lvalues. *)
+module Variable = struct
+ include Cil_datatype.Varinfo
+ let id v = v.vid
+end
+
+module VariableSet = struct
+ include Variable.Set
+ let pretty_debug = pretty
+end
+
+(* Pairs of related variables in an octagon.
+ This module imposes an order between the two variables X and Y in a pair
+ to avoid creating octagons about X±Y *and* about Y±X. *)
+module Pair = struct
+ module D = Datatype.Pair (Variable) (Variable)
+ module Info = struct
+ let name = "Octagons.Pair"
+ let dependencies = [ Ast.self ]
+ let initial_values = []
+ end
+
+ include State_builder.Hashcons (D) (Info)
+
+ (* Creates a pair, and also returns a boolean that is [true] if x, y are
+ swapped in the pair. *)
+ let make x y =
+ assert (x.vid <> y.vid);
+ let pair, swap = if x.vid < y.vid then (x, y), false else (y, x), true in
+ hashcons pair, swap
+
+ let fst t = fst (get t)
+end
+
+
+(* Kind of relation between two variables X and Y: X+Y or X-Y. *)
+type operation = Add | Sub
+
+(* Extended arithmetic operations over Ival.t. *)
+module Arith = struct
+ open Ival
+
+ let top_float = Ival.inject_float Fval.top
+
+ let narrow x y =
+ let r = narrow x y in
+ if is_bottom r then `Bottom else `Value r
+
+ let widen =
+ let hints = Integer.zero,
+ (Ival.Widen_Hints.default_widen_hints,
+ Fc_float.Widen_Hints.default_widen_hints)
+ in
+ Ival.widen hints
+
+ (* TODO: do not use Ival.top on floating-point value? *)
+ let project_float ival =
+ if Ival.(equal top ival) then Fval.top
+ else project_float ival
+
+ let neg = function
+ | Float f -> inject_float (Fval.neg f)
+ | ival -> neg_int ival
+
+ let int_or_float_operation i_op f_op = fun typ ->
+ match Cil.unrollType typ with
+ | TInt _ | TEnum _ -> i_op
+ | TFloat _ -> fun i1 i2 ->
+ inject_float (f_op Fval.Real (project_float i1) (project_float i2))
+ | _ -> assert false
+
+ let sub = int_or_float_operation Ival.sub_int Fval.sub
+ let add = int_or_float_operation Ival.add_int Fval.add
+
+ let apply = function
+ | Add -> add
+ | Sub -> sub
+
+ (* Creates the ival covering the integer range [range]. *)
+ let make_range range =
+ let min = Eval_typ.range_lower_bound range in
+ let max = Eval_typ.range_upper_bound range in
+ Ival.inject_range (Some min) (Some max)
+
+ (* Does an ival represent all values of a C type [typ]? *)
+ let is_top_for_typ typ ival =
+ let open Eval_typ in
+ Ival.(equal top ival) ||
+ match classify_as_scalar typ with
+ | None -> assert false
+ | Some (TSFloat _) -> Ival.equal top_float ival
+ | Some (TSInt range | TSPtr range) ->
+ (* TODO: this could be more efficient. *)
+ let range = make_range range in
+ Ival.is_included range ival || Ival.is_included range (neg_int ival)
+
+ (* Does an ival represent all possible values of a pair of variables? *)
+ let is_top_for_pair pair =
+ let x, y = Pair.get pair in
+ if Cil_datatype.Typ.equal x.vtype y.vtype
+ then is_top_for_typ x.vtype
+ else fun ival -> is_top_for_typ x.vtype ival && is_top_for_typ y.vtype ival
+end
+
+(* -------------------------------------------------------------------------- *)
+(* Rewriting Cil expressions into mathematical octagons *)
+(* -------------------------------------------------------------------------- *)
+
+(* An octagonal relation between two variables : b ≤ X±Y ≤ e *)
+type octagon =
+ { variables: Pair.t; (* The two related variables X and Y. *)
+ operation: operation; (* Whether the relation is about X+Y or X-Y. *)
+ value: Ival.t; (* The interval of X±Y. *)
+ }
+
+let _pretty_octagon fmt octagon =
+ let x, y = Pair.get octagon.variables in
+ let op = match octagon.operation with Add -> "+" | Sub -> "-" in
+ Format.fprintf fmt "%a %s %a %s %a"
+ Printer.pp_varinfo x op Printer.pp_varinfo y
+ (Unicode.inset_string ()) Ival.pretty octagon.value
+
+(* Transforms Cil expressions into mathematical octagons.
+ Use Ival.t to evaluate expressions. *)
+module Rewriting = struct
+
+ (* Checks if the interval [ival] fits in the C type [typ].
+ This is used to ensure that an expression cannot overflow: this module
+ uses the mathematical semantics of arithmetic operations, and cannot
+ soundly translate overflows in the C semantics. *)
+ let may_overflow typ ival =
+ let open Eval_typ in
+ match classify_as_scalar typ with
+ | None -> assert false (* This should not happen here. *)
+ | Some (TSFloat _) -> false
+ | Some (TSInt range | TSPtr range) ->
+ not
+ ((range.i_signed && Kernel.SignedOverflow.get ()) ||
+ (not range.i_signed && Kernel.UnsignedOverflow.get ()) ||
+ Ival.is_included ival (Arith.make_range range))
+
+ (* Simplified form [±X-coeff] for expressions,
+ where X is a variable and coeff an interval. *)
+ type var_coeff = { varinfo: varinfo; sign: bool; coeff: Ival.t; }
+
+ (* Negates a simplified form. *)
+ let neg { varinfo; sign; coeff } =
+ { varinfo; sign = not sign; coeff = Arith.neg coeff }
+
+ (* Is the interval computed for a variable a singleton? *)
+ let is_singleton = function
+ | `Top -> false
+ | `Value ival -> Ival.cardinal_zero_or_one ival
+
+ (* If a needed interval is unknown, stop the current computation and return
+ an empty list. *)
+ let (>>) value f = match value with
+ | `Top -> []
+ | `Value ival -> f ival
+
+ (* Apply [f typ v1 v2] if the operation [e1 op e2] does not overflow,
+ where [v1] and [v2] are the intervals for [e1] and [e2], and [typ] is
+ the type of [e1]. Returns the empty list otherwise. *)
+ let apply_binop f evaluate typ e1 op e2 =
+ evaluate e1 >> fun v1 ->
+ evaluate e2 >> fun v2 ->
+ let typ_e1 = Cil.typeOf e1 in
+ let result = Arith.apply op typ_e1 v1 v2 in
+ if may_overflow typ result
+ then []
+ else f typ_e1 v1 v2
+
+ (* Rewrites the Cil expression [expr] into the simplified form [±x-coeff],
+ where [x] is a non-singleton variable and [coeff] is an interval. The
+ result follows the mathematical semantics.
+ If such a simplified form cannot be found, the function returns an empty
+ list. If multiple variables occur in the expression, the function tries to
+ compute a list of equivalent forms [±x-coeff], one for each variable. The
+ function relies on an evaluation function linking each sub-expression into
+ an interval, used for computing sound coefficients. The evaluation may
+ return Top for some sub-expression, thus preventing the computation. *)
+ let rec rewrite evaluate expr =
+ match expr.enode with
+ | Lval (Var varinfo, NoOffset) ->
+ if Cil.isIntegralType varinfo.vtype
+ && not (Cil.typeHasQualifier "volatile" varinfo.vtype)
+ && not (is_singleton (evaluate expr))
+ then [ { varinfo; sign = true; coeff = Ival.zero } ]
+ else []
+
+ | UnOp (Neg, e, typ) ->
+ evaluate e >> fun v ->
+ if may_overflow typ (Arith.neg v)
+ then [] else List.map neg (rewrite evaluate e)
+
+ | BinOp ((PlusA | MinusA as binop), e1, e2, typ) ->
+ let op = if binop = PlusA then Add else Sub in
+ let rewrite_binop typ v1 v2 =
+ let inverse_op = if binop = PlusA then Arith.sub else Arith.add in
+ let add_v2 var =
+ { var with coeff = inverse_op typ var.coeff v2 }
+ in
+ let add_v1 var =
+ let var = if binop = MinusA then neg var else var in
+ { var with coeff = Arith.sub typ var.coeff v1 }
+ in
+ List.map add_v2 (rewrite evaluate e1) @
+ List.map add_v1 (rewrite evaluate e2)
+ in
+ apply_binop rewrite_binop evaluate typ e1 op e2
+
+ | CastE (typ, e) ->
+ if Cil.(isIntegralType typ && isIntegralType (typeOf e)) then
+ evaluate e >> fun v ->
+ if may_overflow typ v then [] else rewrite evaluate e
+ else []
+
+ | Info (e, _) -> rewrite evaluate e
+
+ | _ -> []
+
+ (* Rewrites the operation [e1 ± e2] into equivalent octagons ±(X±Y-value). *)
+ let rewrite_binop evaluate e1 binop e2 =
+ let vars1 = rewrite evaluate e1 in
+ let vars2 = rewrite evaluate e2 in
+ let vars2 = if binop = Sub then List.map neg vars2 else vars2 in
+ let aux acc var1 var2 =
+ if Cil_datatype.Varinfo.equal var1.varinfo var2.varinfo
+ then acc
+ else
+ let variables, swap = Pair.make var1.varinfo var2.varinfo in
+ let operation = if var1.sign = var2.sign then Add else Sub in
+ let sign = match operation with
+ | Add -> var1.sign
+ | Sub -> if swap then var2.sign else var1.sign
+ in
+ let value = Arith.add (Cil.typeOf e1) var1.coeff var2.coeff in
+ let value = if sign then value else Arith.neg value in
+ (* Do not include this rewriting if the [value] exceeds all possible
+ values for the type of [var1] and [var2]. *)
+ if Arith.is_top_for_pair variables value
+ then acc
+ else (sign, { variables; operation; value }) :: acc
+ in
+ Extlib.product_fold aux [] vars1 vars2
+
+ (* Returns the range of the expression X-Y when the comparison X#Y holds. *)
+ let comparison_range =
+ let open Abstract_interp.Comp in
+ function
+ | Lt -> Ival.inject_range None (Some Integer.minus_one)
+ | Gt -> Ival.inject_range (Some Integer.one) None
+ | Le -> Ival.inject_range None (Some Integer.zero)
+ | Ge -> Ival.inject_range (Some Integer.zero) None
+ | Eq -> Ival.zero
+ | Ne -> Ival.top
+
+ (* Transforms the constraint [expr] ∈ [ival] into a list of octagonal
+ constraints. *)
+ let make_octagons evaluate expr ival =
+ let make_octagons_from_binop typ e1 op e2 ival =
+ (* equivalent octagonal forms ±(X±Y-v) for [e1 op e2]. *)
+ let rewritings = rewrite_binop evaluate e1 op e2 in
+ (* create the final octagon, knowning that [e1 op e2] ∈ [ival]. *)
+ let make_octagon (sign, octagon) =
+ let ival = if sign then ival else Arith.neg ival in
+ let value = Arith.add typ ival octagon.value in
+ { octagon with value }
+ in
+ List.map make_octagon rewritings
+ in
+ match expr.enode with
+ | BinOp ((PlusA | MinusA as binop), e1, e2, typ) ->
+ let op = if binop = PlusA then Add else Sub in
+ let make_octagons typ _ _ = make_octagons_from_binop typ e1 op e2 ival in
+ apply_binop make_octagons evaluate typ e1 op e2
+ | BinOp ((Lt | Gt | Le | Ge | Eq | Ne as binop), e1, e2, _typ) ->
+ let typ = Cil.typeOf e1 in
+ if not (Cil.isIntegralType typ)
+ || (Ival.contains_zero ival && Ival.contains_non_zero ival)
+ then []
+ else
+ let comp = Value_util.conv_comp binop in
+ let comp =
+ if Ival.is_zero ival then Abstract_interp.Comp.inv comp else comp
+ in
+ let range = comparison_range comp in
+ make_octagons_from_binop typ e1 Sub e2 range
+ | _ -> []
+
+ let overflow_alarms typ expr ival =
+ match Eval_typ.classify_as_scalar typ with
+ | Some (Eval_typ.TSInt range) ->
+ let signed = range.Eval_typ.i_signed in
+ let overflow = if signed then Alarms.Signed else Alarms.Unsigned in
+ let max_bound = Eval_typ.range_upper_bound range in
+ let min_bound = Eval_typ.range_lower_bound range in
+ let ival_range = Ival.inject_range (Some min_bound) (Some max_bound) in
+ let aux has_better_bound bound bound_kind alarms =
+ if has_better_bound ival ival_range >= 0
+ then
+ let alarm = Alarms.Overflow (overflow, expr, bound, bound_kind) in
+ Alarmset.set alarm Alarmset.True alarms
+ else alarms
+ in
+ let alarms = Alarmset.all in
+ let alarms =
+ aux Ival.has_greater_min_bound min_bound Alarms.Lower_bound alarms
+ in
+ aux Ival.has_smaller_max_bound max_bound Alarms.Upper_bound alarms
+ | _ -> Alarmset.all
+
+ (* Evaluates the Cil expression [expr], by rewriting it into octagonal
+ constraints using [evaluate_expr] to evaluate sub-expressions, and
+ then using [evaluate_octagon] to evaluate the octagons. *)
+ let evaluate_through_octagons evaluate_expr evaluate_octagon expr =
+ let evaluate_octagon acc (sign, octagon) =
+ match evaluate_octagon octagon with
+ | None -> acc
+ | Some ival ->
+ let ival = if sign then ival else Arith.neg ival in
+ Ival.narrow acc ival
+ in
+ let evaluate_octagons octagons =
+ List.fold_left evaluate_octagon Ival.top octagons
+ in
+ let default = Ival.top, Alarmset.all in
+ match expr.enode with
+ | BinOp ((PlusA | MinusA as binop), e1, e2, typ) ->
+ let op = if binop = PlusA then Add else Sub in
+ let octagons = rewrite_binop evaluate_expr e1 op e2 in
+ let ival = evaluate_octagons octagons in
+ if Ival.(equal top ival) then default else
+ let typ_e1 = Cil.typeOf e1 in
+ let ival2 =
+ match evaluate_expr e1, evaluate_expr e2 with
+ | `Value v1, `Value v2 -> Arith.apply op typ_e1 v1 v2
+ | _, _ -> Ival.top
+ in
+ let ival = Ival.narrow ival ival2 in
+ if may_overflow typ ival
+ then default
+ else ival, overflow_alarms typ expr ival
+ | BinOp ((Lt | Gt | Le | Ge | Eq as binop), e1, e2, _typ)
+ when Cil.isIntegralType (Cil.typeOf e1) ->
+ let comp = Value_util.conv_comp binop in
+ (* Evaluate [e1 - e2] and compare the resulting interval to the interval
+ for which the comparison [e1 # e2] holds. *)
+ let range = comparison_range comp in
+ let octagons = rewrite_binop evaluate_expr e1 Sub e2 in
+ let ival = evaluate_octagons octagons in
+ if Ival.is_included ival range then Ival.one, Alarmset.all
+ else if not (Ival.intersects ival range)
+ then Ival.zero, Alarmset.all else default
+ | _ -> default
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* Diamonds and octagons: relations between two variables *)
+(* -------------------------------------------------------------------------- *)
+
+(* This domain infers relations between pairs of variables (X, Y), by inferring
+ intervals for the mathematical operations X+Y and X-Y.
+ It also infers non-relational intervals for the separate variables X and Y
+ (they could be seen as intervals for X+X and Y+Y, but we chose to store them
+ in another way). These intervals are used to make the join more precise.
+ Geometrically, in a plan, intervals for X and Y shape a straight rectangle,
+ while intervals for X+Y and X-Y shape a "leaning" rectangle; the intersection
+ of these rectangles shapes an octagon.
+ Using a misnomer, we call diamonds the intervals for X+Y and X-Y, and
+ octagons the maps from variables to diamonds, even if they do not exactly
+ shape octagons. *)
+
+(* Relation between a pair of variables (X, Y).
+ [add] is an interval for X+Y, and [sub] is an interval for [X-Y]. *)
+type diamond = { add: Ival.t; sub: Ival.t }
+
+module DiamondDatatype = struct
+ type t = diamond
+ include Datatype.Serializable_undefined
+
+ let name = "Octagons.Diamond"
+ let structural_descr =
+ Structural_descr.t_record [| Ival.packed_descr; Ival.packed_descr |]
+ let reprs = [ { add = Ival.top; sub = Ival.top } ]
+
+ let compare x y =
+ let c = Ival.compare x.add y.add in
+ if c <> 0 then c else Ival.compare x.sub y.sub
+
+ let equal = Datatype.from_compare
+
+ let hash { add; sub } = Hashtbl.hash (Ival.hash add, Ival.hash sub)
+
+ let pretty fmt { add; sub } =
+ Format.fprintf fmt "@[<hov>ADD: @[%a@] ; SUB: @[%a@]@]"
+ Ival.pretty add Ival.pretty sub
+end
+
+module Diamond = struct
+ include Datatype.Make (DiamondDatatype)
+ let pretty_debug = pretty
+
+ let top = { add = Ival.top; sub = Ival.top }
+
+ let is_included x y =
+ Ival.is_included x.add y.add && Ival.is_included x.sub y.sub
+
+ let join x y =
+ { add = Ival.join x.add y.add; sub = Ival.join x.sub y.sub }
+
+ let widen x y =
+ { add = Arith.widen x.add y.add; sub = Arith.widen x.sub y.sub }
+
+ let narrow x y =
+ Arith.narrow x.add y.add >>- fun add ->
+ Arith.narrow x.sub y.sub >>-: fun sub -> {add; sub}
+
+ (* If [swap] is true, makes a diamond about (X, Y) from a diamond
+ about (Y, X). *)
+ let reverse_variables swap t =
+ if swap then { t with sub = Arith.neg t.sub } else t
+
+ (* Normalizes a diamond for the pair of variables [pair]: replaces too large
+ ivals by Ival.top. Returns None if both ivals are meaningless. *)
+ let trim pair t =
+ let is_top = Arith.is_top_for_pair pair in
+ match is_top t.add, is_top t.sub with
+ | true, true -> None
+ | true, false -> Some { t with add = Ival.top }
+ | false, true -> Some { t with sub = Ival.top }
+ | false, false -> Some t
+end
+
+
+(* Maps linking pairs of variables (X, Y) to intervals for X+Y and X-Y. *)
+module Octagons = struct
+ module Initial_Values = struct let v = [[]] end
+ module Dependencies = struct let l = [ Ast.self ] end
+
+ include Hptmap.Make (Pair) (Diamond)
+ (Hptmap.Comp_unused) (Initial_Values) (Dependencies)
+
+ let internal_join = join
+
+ let pretty fmt t =
+ let iter f = iter (fun k v -> f (k, v)) in
+ let pretty fmt (pair, diamond) =
+ let x, y = Pair.get pair in
+ let pretty_one op ival =
+ if not Ival.(equal top ival)
+ then
+ Format.fprintf fmt "@[@[%a %s %a@] %s @[%a@]@]@,"
+ Variable.pretty x op Variable.pretty y
+ (Unicode.inset_string ()) Ival.pretty ival
+ in
+ pretty_one "+" diamond.add;
+ pretty_one "-" diamond.sub
+ in
+ Pretty_utils.pp_iter
+ ~pre:"@[<v 3>{[ " ~suf:" ]}@]" ~sep:""
+ iter pretty fmt t
+
+ let top = empty
+
+ let is_included =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Octagons.is_included" in
+ let decide_fst _ _ = true in
+ let decide_snd _ _ = false in
+ let decide_both _ x y = Diamond.is_included x y in
+ let decide_fast t1 t2 = decide_fast_inclusion t2 t1 in
+ binary_predicate cache UniversalPredicate
+ ~decide_fast ~decide_fst ~decide_snd ~decide_both
+
+ exception EBottom
+
+ let narrow_exc =
+ let cache = Hptmap_sig.NoCache in
+ let decide _pair x y =
+ match Diamond.narrow x y with
+ | `Value v -> v
+ | `Bottom -> raise EBottom
+ in
+ join ~cache ~symmetric:true ~idempotent:true ~decide
+
+ let narrow x y = try `Value (narrow_exc x y) with EBottom -> `Bottom
+
+ let simple_join =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Octagons.join" in
+ let decide pair x y = Diamond.trim pair (Diamond.join x y) in
+ inter ~cache ~symmetric:true ~idempotent:true ~decide
+
+ let join ~decide_left ~decide_right =
+ let cache = Hptmap_sig.NoCache in
+ let decide_left = Traversing decide_left
+ and decide_right = Traversing decide_right in
+ let decide_both pair x y = Diamond.trim pair (Diamond.join x y) in
+ merge ~cache ~symmetric:false ~idempotent:true
+ ~decide_left ~decide_right ~decide_both
+
+ let simple_widen =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Octagons.widen" in
+ let decide pair x y = Diamond.trim pair (Diamond.widen x y) in
+ inter ~cache ~symmetric:false ~idempotent:true ~decide
+
+ let widen ~decide_left ~decide_right =
+ let cache = Hptmap_sig.NoCache in
+ let decide_left = Traversing decide_left
+ and decide_right = Traversing decide_right in
+ let decide_both pair x y = Diamond.trim pair (Diamond.widen x y) in
+ merge ~cache ~symmetric:false ~idempotent:true
+ ~decide_left ~decide_right ~decide_both
+
+ let unsafe_add = add
+
+ let add variables diamond t =
+ try
+ Diamond.narrow diamond (find variables t) >>-: fun diamond ->
+ add variables diamond t
+ with Not_found -> `Value (add variables diamond t)
+
+ let add_octagon { variables; operation; value; } t =
+ let diamond =
+ try find variables t
+ with Not_found -> Diamond.top
+ in
+ let diamond =
+ match operation with
+ | Add ->
+ Arith.narrow diamond.add value >>-: fun add ->
+ { diamond with add }
+ | Sub ->
+ Arith.narrow diamond.sub value >>-: fun sub ->
+ { diamond with sub }
+ in
+ diamond >>-: fun diamond -> unsafe_add variables diamond t
+
+ let evaluate octagon t =
+ try
+ let diamond = find octagon.variables t in
+ let ival = match octagon.operation with
+ | Add -> diamond.add
+ | Sub -> diamond.sub
+ in
+ if Ival.(equal top ival)
+ then None
+ else
+ let typ = (Pair.fst octagon.variables).vtype in
+ let ival = Arith.sub typ ival octagon.value in
+ Some ival
+ with Not_found -> None
+end
+
+(* -------------------------------------------------------------------------- *)
+(* Relations *)
+(* -------------------------------------------------------------------------- *)
+
+(* Keep track of related variables in an octagon state. *)
+module Relations = struct
+ module Initial_Values = struct let v = [[]] end
+ module Dependencies = struct let l = [ Ast.self ] end
+
+ include Hptmap.Make (Variable) (VariableSet)
+ (Hptmap.Comp_unused) (Initial_Values) (Dependencies)
+
+ let inter =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Relations.inter" in
+ let decide _pair x y =
+ let r = Variable.Set.inter x y in
+ if Variable.Set.is_empty r then None else Some r
+ in
+ inter ~cache ~symmetric:true ~idempotent:true ~decide
+
+ let union =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Relations.union" in
+ let decide _pair x y = Variable.Set.union x y in
+ join ~cache ~symmetric:true ~idempotent:true ~decide
+
+ (* Marks y as related to x. *)
+ let relate_aux x y t =
+ let related =
+ try find x t
+ with Not_found -> VariableSet.empty
+ in
+ let updated = VariableSet.add y related in
+ add x updated t
+
+ (* Marks x and y as mutually related. *)
+ let relate pair t =
+ let x, y = Pair.get pair in
+ relate_aux y x (relate_aux x y t)
+
+ let add variable set t =
+ if VariableSet.is_empty set
+ then remove variable t
+ else add variable set t
+end
+
+(* -------------------------------------------------------------------------- *)
+(* Non-relational intervals *)
+(* -------------------------------------------------------------------------- *)
+
+module Intervals = struct
+ module Initial_Values = struct let v = [[]] end
+ module Dependencies = struct let l = [ Ast.self ] end
+
+ include Hptmap.Make (Variable) (Ival)
+ (Hptmap.Comp_unused) (Initial_Values) (Dependencies)
+
+ let internal_join = join
+
+ let top = empty
+
+ let is_included =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Intervals.is_included" in
+ let decide_fst _ _ = true in
+ let decide_snd _ _ = false in
+ let decide_both _ x y = Ival.is_included x y in
+ let decide_fast t1 t2 = decide_fast_inclusion t2 t1 in
+ binary_predicate cache UniversalPredicate
+ ~decide_fast ~decide_fst ~decide_snd ~decide_both
+
+ exception EBottom
+
+ let narrow_exc =
+ let cache = Hptmap_sig.NoCache in
+ let decide _varinfo x y =
+ let ival = Ival.narrow x y in
+ if Ival.is_bottom ival then raise EBottom else ival
+ in
+ join ~cache ~symmetric:true ~idempotent:true ~decide
+
+ let narrow x y = try `Value (narrow_exc x y) with EBottom -> `Bottom
+
+ let join =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Intervals.join" in
+ let decide _varinfo x y =
+ let r = Ival.join x y in
+ if Ival.(equal top r) then None else Some r
+ in
+ inter ~cache ~symmetric:true ~idempotent:true ~decide
+
+ let widen =
+ let cache = Hptmap_sig.PersistentCache "Octagons.Intervals.widen" in
+ let decide _varinfo x y =
+ let r = Arith.widen x y in
+ if Ival.(equal top r) then None else Some r
+ in
+ inter ~cache ~symmetric:false ~idempotent:true ~decide
+end
+
+(* -------------------------------------------------------------------------- *)
+(* Octagon states *)
+(* -------------------------------------------------------------------------- *)
+
+module Zone = Locations.Zone
+
+module State = struct
+
+ type state =
+ { octagons: Octagons.t; (* The intervals for X±Y. *)
+ intervals: Intervals.t; (* The intervals for the variables X,Y… *)
+ relations: Relations.t; (* The related variables in [octagons]. *)
+ modified: Locations.Zone.t; (* The memory zone modified by a function. *)
+ }
+
+ include Datatype.Make_with_collections
+ (struct
+ type t = state
+ include Datatype.Serializable_undefined
+
+ let name = "Octagons.State"
+ let structural_descr =
+ Structural_descr.t_record
+ [| Octagons.packed_descr;
+ Intervals.packed_descr;
+ Relations.packed_descr;
+ Zone.packed_descr |]
+ let reprs =
+ [ { octagons = Octagons.top;
+ intervals = Intervals.empty;
+ relations = Relations.empty;
+ modified = Zone.bottom } ]
+
+ let compare s1 s2 =
+ let c = Octagons.compare s1.octagons s2.octagons in
+ if c <> 0 then c else
+ let c = Intervals.compare s1.intervals s2.intervals in
+ if c <> 0 then c else
+ Zone.compare s1.modified s2.modified
+
+ let equal = Datatype.from_compare
+
+ let hash t =
+ Hashtbl.hash (Octagons.hash t.octagons,
+ Relations.hash t.relations,
+ Zone.hash t.modified)
+
+ let pretty fmt { octagons } =
+ Format.fprintf fmt "@[%a@]" Octagons.pretty octagons
+ end)
+
+ let pretty_debug fmt { octagons; intervals; relations } =
+ Format.fprintf fmt "@[<v> Octagons: %a@; Intervals: %a@; Relations: %a@]"
+ Octagons.pretty octagons Intervals.pretty intervals
+ Relations.pretty relations
+
+ (* Verify the internal structure of a state [t], depending on the boolean
+ variable [debug]. *)
+ let check =
+ if not debug
+ then fun _ t -> t
+ else fun msg t ->
+ (* Checks that an octagon is properly registered in [t.relations]. This is
+ mandatory for the soundness of the domain. On the other hand, two
+ variables can be related in [t.relations] without an actual octagon
+ between them. *)
+ let check_octagon pair _ =
+ let x, y = Pair.get pair in
+ try VariableSet.mem x (Relations.find y t.relations)
+ && VariableSet.mem y (Relations.find x t.relations)
+ with Not_found -> false
+ in
+ if Octagons.for_all check_octagon t.octagons
+ then t
+ else
+ Value_parameters.abort
+ "Incorrect octagon state computed by function %s:@ %a"
+ msg pretty_debug t
+
+ (* ------------------------------ Lattice --------------------------------- *)
+
+ let top =
+ { octagons = Octagons.top;
+ intervals = Intervals.top;
+ relations = Relations.empty;
+ modified = Zone.top; }
+
+ let empty () =
+ { octagons = Octagons.top;
+ intervals = Intervals.top;
+ relations = Relations.empty;
+ modified = Zone.bottom; }
+
+ let is_included t1 t2 =
+ Octagons.is_included t1.octagons t2.octagons
+ && Intervals.is_included t1.intervals t2.intervals
+ && Zone.is_included t1.modified t2.modified
+
+ let join t1 t2 =
+ let octagons =
+ if not infer_intervals
+ then Octagons.simple_join t1.octagons t2.octagons
+ else
+ let decide_empty intervals pair diamond =
+ let v1, v2 = Pair.get pair in
+ try
+ let i1 = Intervals.find v1 intervals
+ and i2 = Intervals.find v2 intervals in
+ let add = Arith.add v1.vtype i1 i2
+ and sub = Arith.sub v1.vtype i1 i2 in
+ let diamond = Diamond.join diamond { add; sub } in
+ Diamond.trim pair diamond
+ with Not_found -> None
+ in
+ let decide_left = decide_empty t2.intervals
+ and decide_right = decide_empty t1.intervals in
+ Octagons.join ~decide_left ~decide_right t1.octagons t2.octagons
+ in
+ let relations =
+ if infer_intervals
+ then Relations.union t1.relations t2.relations
+ else Relations.inter t1.relations t2.relations
+ in
+ let state =
+ { octagons; relations;
+ intervals = Intervals.join t1.intervals t2.intervals;
+ modified = Zone.join t1.modified t2.modified; }
+ in
+ check "join" state
+
+ let widen _kf _hints t1 t2 =
+ let octagons =
+ if not infer_intervals
+ then Octagons.simple_widen t1.octagons t2.octagons
+ else
+ let decide_empty b intervals pair diamond =
+ let v1, v2 = Pair.get pair in
+ try
+ let i1 = Intervals.find v1 intervals
+ and i2 = Intervals.find v2 intervals in
+ let add = Arith.add v1.vtype i1 i2
+ and sub = Arith.sub v1.vtype i1 i2 in
+ let diamond =
+ if b
+ then Diamond.widen { add; sub } diamond
+ else Diamond.widen diamond { add; sub }
+ in
+ Diamond.trim pair diamond
+ with Not_found -> None
+ in
+ let decide_left = decide_empty false t2.intervals
+ and decide_right = decide_empty true t1.intervals in
+ Octagons.widen ~decide_left ~decide_right t1.octagons t2.octagons
+ in
+ let relations =
+ if infer_intervals
+ then Relations.union t1.relations t2.relations
+ else Relations.inter t1.relations t2.relations
+ in
+ let state =
+ { octagons; relations;
+ intervals = Intervals.widen t1.intervals t2.intervals;
+ modified = Zone.join t1.modified t2.modified; }
+ in
+ check "widen" state
+
+ let narrow t1 t2 =
+ Octagons.narrow t1.octagons t2.octagons >>- fun octagons ->
+ Intervals.narrow t1.intervals t2.intervals >>- fun intervals ->
+ let relations = Relations.union t1.relations t2.relations in
+ let modified = Zone.narrow t1.modified t2.modified in
+ `Value { octagons; intervals; relations; modified; }
+
+ (* -------------- Transitive closure when adding an octagon --------------- *)
+
+ type relation =
+ { vars: varinfo * varinfo;
+ diamond: diamond; }
+
+ let add_diamond state pair diamond =
+ match Diamond.trim pair diamond with
+ | None -> `Value state
+ | Some diamond ->
+ Octagons.add pair diamond state.octagons >>-: fun octagons ->
+ let relations = Relations.relate pair state.relations in
+ { state with octagons; relations }
+
+ let inverse { vars; diamond } =
+ let var1, var2 = vars in
+ { vars = var2, var1; diamond = Diamond.reverse_variables true diamond }
+
+ let transitive_relation y rel1 rel2 =
+ let rel1 =
+ if Variable.equal y (snd rel1.vars) then rel1 else inverse rel1
+ and rel2 =
+ if Variable.equal y (fst rel2.vars) then rel2 else inverse rel2
+ in
+ (* rel1 is about X±Y, rel2 is about Y±Z. *)
+ let typ = y.vtype in
+ (* X+Z = (X+Y) - (Y-Z) and X+Y = (X-Y) + (Y+Z) *)
+ let add =
+ Ival.narrow
+ (Arith.sub typ rel1.diamond.add rel2.diamond.sub)
+ (Arith.add typ rel1.diamond.sub rel2.diamond.add)
+ (* X-Z = (X+Y) - (Y+Z) and X-Z = (X-Y) + (Y-Z) *)
+ and sub =
+ Ival.narrow
+ (Arith.sub typ rel1.diamond.add rel2.diamond.add)
+ (Arith.add typ rel1.diamond.sub rel2.diamond.sub)
+ in
+ let diamond = {add; sub} in
+ let pair, swap = Pair.make (fst rel1.vars) (snd rel2.vars) in
+ let diamond = Diamond.reverse_variables swap diamond in
+ pair, diamond
+
+ let saturate state x y rel1 =
+ try
+ let y_related = Relations.find y state.relations in
+ let y_related = VariableSet.remove x y_related in
+ let aux z state =
+ state >>- fun state ->
+ try
+ let pair, _ = Pair.make y z in
+ let diamond = Octagons.find pair state.octagons in
+ let vars = Pair.get pair in
+ let rel2 = { vars; diamond } in
+ let pair, diamond = transitive_relation y rel1 rel2 in
+ add_diamond state pair diamond
+ with Not_found -> `Value state
+ in
+ VariableSet.fold aux y_related (`Value state)
+ with Not_found -> `Value state
+
+ let add_octagon state octagon =
+ if Arith.is_top_for_pair octagon.variables octagon.value
+ then `Value state
+ else
+ let state =
+ if saturate_octagons
+ then
+ let x, y = Pair.get octagon.variables in
+ let diamond = match octagon.operation with
+ | Add -> { add = octagon.value; sub = Ival.top }
+ | Sub -> { add = Ival.top; sub = octagon.value }
+ in
+ let relation = { vars = x, y; diamond } in
+ saturate state y x relation >>- fun state ->
+ saturate state x y relation
+ else `Value state
+ in
+ state >>- fun state ->
+ Octagons.add_octagon octagon state.octagons >>-: fun octagons ->
+ let relations = Relations.relate octagon.variables state.relations in
+ { state with octagons; relations }
+
+ let remove state x =
+ let intervals = Intervals.remove x state.intervals in
+ let state = { state with intervals } in
+ try
+ let relations = Relations.find x state.relations in
+ let remove_one y state =
+ try
+ let yrelations = Relations.find y state.relations in
+ let yrelations = VariableSet.remove x yrelations in
+ let relations = Relations.add y yrelations state.relations in
+ let pair, _ = Pair.make x y in
+ let octagons = Octagons.remove pair state.octagons in
+ { state with octagons; relations }
+ with Not_found -> state
+ in
+ let state = VariableSet.fold remove_one relations state in
+ let relations = Relations.remove x state.relations in
+ { state with relations }
+ with Not_found -> state
+
+ let related_octagons state x =
+ try
+ let related = Relations.find x state.relations in
+ let aux y acc =
+ let pair, swap = Pair.make x y in
+ try
+ let diamond = Octagons.find pair state.octagons in
+ let diamond = Diamond.reverse_variables swap diamond in
+ (y, diamond) :: acc
+ with Not_found -> acc
+ in
+ VariableSet.fold aux related []
+ with Not_found -> []
+
+ (* x' = ±x - delta *)
+ let sub_delta ~inverse state x delta =
+ let intervals = Intervals.remove x state.intervals in
+ let state = { state with intervals } in
+ let x_related = Relations.find x state.relations in
+ let aux y state =
+ let pair, swap = Pair.make x y in
+ try
+ let diamond = Octagons.find pair state.octagons in
+ let diamond =
+ if inverse
+ then
+ let op = if swap then fun x -> x else Arith.neg in
+ { add = op diamond.sub;
+ sub = op diamond.add }
+ else diamond
+ in
+ let typ = x.vtype in
+ let op = if swap then Arith.add else Arith.sub in
+ let add =
+ if Ival.(equal top diamond.add)
+ then diamond.add
+ else Arith.sub typ diamond.add delta
+ and sub =
+ if Ival.(equal top diamond.sub)
+ then diamond.sub
+ else op typ diamond.sub delta
+ in
+ let diamond' = { add; sub } in
+ let octagons = Octagons.unsafe_add pair diamond' state.octagons in
+ { state with octagons }
+ with Not_found -> state
+ in
+ VariableSet.fold aux x_related state
+end
+
+(* -------------------------------------------------------------------------- *)
+(* Octagon domain *)
+(* -------------------------------------------------------------------------- *)
+
+module Domain = struct
+
+ include State
+
+ type value = Cvalue.V.t
+ type location = Precise_locs.precise_location
+
+ type origin = unit
+ let top_value = `Value (Cvalue.V.top, ()), Alarmset.all
+
+ let extract_expr oracle state expr =
+ let evaluate_expr expr =
+ match fst (oracle expr) with
+ | `Bottom -> `Top (* should not happen *)
+ | `Value cvalue ->
+ try `Value (Cvalue.V.project_ival cvalue)
+ with Cvalue.V.Not_based_on_null -> `Top
+ in
+ let evaluate_octagon octagon = Octagons.evaluate octagon state.octagons in
+ let ival, alarms =
+ Rewriting.evaluate_through_octagons evaluate_expr evaluate_octagon expr
+ in
+ if Ival.(equal ival top)
+ then top_value
+ else if Ival.is_bottom ival
+ then `Bottom, Alarmset.all
+ else `Value (Cvalue.V.inject_ival ival, ()), alarms
+
+ let extract_lval _oracle _t _lval _typ _loc = top_value
+
+ let backward_location _t _lval _typ loc value = `Value (loc, value)
+
+ let reduce_further state expr value =
+ match expr.enode with
+ | Lval (Var x, NoOffset) when Cil.isIntegralType x.vtype ->
+ begin
+ try
+ let x_ival = Cvalue.V.project_ival value in
+ let octagons = State.related_octagons state x in
+ let reduce acc (y, octagons) =
+ let y_ival1 =
+ if Ival.(equal top octagons.add)
+ then Ival.top
+ else Arith.sub x.vtype octagons.add x_ival
+ in
+ let y_ival2 =
+ if Ival.(equal top octagons.sub)
+ then Ival.top
+ else Arith.sub x.vtype x_ival octagons.sub
+ in
+ let y_ival = Ival.narrow y_ival1 y_ival2 in
+ if Ival.(equal top y_ival) then acc else
+ let y_enode = Lval (Var y, NoOffset) in
+ let y_expr = Cil.new_exp ~loc:expr.eloc y_enode in
+ let y_cvalue = Cvalue.V.inject_ival y_ival in
+ (y_expr, y_cvalue) :: acc
+ in
+ List.fold_left reduce [] octagons
+ with Cvalue.V.Not_based_on_null -> []
+ end
+ | _ -> []
+
+
+ let kill_base base state =
+ try
+ let varinfo = Base.to_varinfo base in
+ State.remove state varinfo
+ with Base.Not_a_C_variable -> state
+
+ let kill zone state =
+ if Locations.Zone.(equal zone top)
+ then top
+ else
+ let modified = Locations.Zone.join state.modified zone in
+ let state = Zone.fold_bases kill_base zone state in
+ { state with modified }
+
+ module Transfer
+ (Valuation: Abstract_domain.Valuation with type value = value
+ and type loc = location)
+ = struct
+
+ (* Evaluation function of expressions to ival, from a [valuation]. *)
+ let evaluation_function valuation = fun expr ->
+ match Valuation.find valuation expr with
+ | `Top -> `Top
+ | `Value record ->
+ match record.Eval.value.v with
+ | `Bottom -> `Top (* TODO: why this keeps happening? *)
+ | `Value cvalue ->
+ try `Value (Cvalue.V.project_ival cvalue)
+ with Cvalue.V.Not_based_on_null -> `Top
+
+ exception EBottom
+
+ let infer_octagons evaluate expr ival state =
+ let octagons = Rewriting.make_octagons evaluate expr ival in
+ let add_octagon state octagon =
+ match State.add_octagon state octagon with
+ | `Bottom -> raise EBottom
+ | `Value state -> state
+ in
+ List.fold_left add_octagon state octagons
+
+ let infer_interval expr ival state =
+ if not infer_intervals
+ then state
+ else
+ match expr.enode with
+ | Lval (Var varinfo, NoOffset)
+ when Cil.isIntegralType varinfo.vtype ->
+ let intervals = Intervals.add varinfo ival state.intervals in
+ { state with intervals }
+ | _ -> state
+
+ let update valuation state =
+ let evaluate = evaluation_function valuation in
+ let aux expr record state =
+ let value = record.Eval.value in
+ match record.reductness, value.v, value.initialized, value.escaping with
+ | (Created | Reduced), `Value cvalue, true, false ->
+ begin
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ let state = infer_octagons evaluate expr ival state in
+ infer_interval expr ival state
+ with Cvalue.V.Not_based_on_null -> state
+ end
+ | _ -> state
+ in
+ try `Value (check "update" (Valuation.fold aux valuation state))
+ with EBottom -> `Bottom
+
+ let assign_interval varinfo assigned state =
+ if not infer_intervals
+ then state
+ else
+ match assigned with
+ | Assign v
+ | Copy (_, { v = `Value v; initialized = true; escaping = false }) ->
+ begin
+ try
+ let ival = Cvalue.V.project_ival v in
+ let intervals = Intervals.add varinfo ival state.intervals in
+ { state with intervals }
+ with Cvalue.V.Not_based_on_null -> state
+ end
+ | _ -> state
+
+ let assign_variable varinfo expr assigned valuation state =
+ let evaluate = evaluation_function valuation in
+ (* TODO: redundant with rewrite_binop below. *)
+ let vars = Rewriting.rewrite evaluate expr in
+ let equal_varinfo v = Variable.equal varinfo v.Rewriting.varinfo in
+ let state =
+ try
+ let var = List.find equal_varinfo vars in
+ let inverse = not var.Rewriting.sign in
+ State.sub_delta ~inverse state varinfo var.Rewriting.coeff
+ with Not_found -> State.remove state varinfo
+ in
+ let state = assign_interval varinfo assigned state in
+ let enode = Lval (Var varinfo, NoOffset) in
+ let left_expr = Cil.new_exp ~loc:expr.eloc enode in
+ (* On the assignment X = E; if X-E can be rewritten as ±(X±Y-v),
+ then the octagonal constraint [X±Y ∈ v] holds. *)
+ let octagons = Rewriting.rewrite_binop evaluate left_expr Sub expr in
+ let state =
+ List.fold_left
+ (fun acc (_sign, octagon) ->
+ acc >>- fun state -> State.add_octagon state octagon)
+ (`Value state) octagons
+ in
+ state >>-: check "precise assign"
+
+ let assign _kinstr left_value expr assigned valuation state =
+ update valuation state >>- fun state ->
+ match left_value.lval with
+ | Var varinfo, NoOffset when Cil.isIntegralType varinfo.vtype ->
+ assign_variable varinfo expr assigned valuation state
+ | _ ->
+ let written_loc = Precise_locs.imprecise_location left_value.lloc in
+ let written_zone =
+ Locations.(enumerate_valid_bits Write written_loc)
+ in
+ let state = kill written_zone state in
+ `Value (check "imprecise assign" state)
+
+ let assume _stmt _exp _bool = update
+
+ let start_call _stmt call valuation state =
+ if intraprocedural ()
+ then `Value (empty ())
+ else
+ let state = { state with modified = Locations.Zone.bottom } in
+ let assign_formal state { formal; concrete; avalue } =
+ state >>- assign_variable formal concrete avalue valuation
+ in
+ List.fold_left assign_formal (`Value state) call.arguments
+
+ let finalize_call _stmt _call ~pre ~post =
+ if intraprocedural ()
+ then `Value (kill post.modified pre)
+ else
+ let modified = Locations.Zone.join post.modified pre.modified in
+ `Value { post with modified }
+
+ let show_expr _valuation _state _fmt _expr = ()
+ end
+
+ let logic_assign _logic_assign location ~pre:_ state =
+ let loc = Precise_locs.imprecise_location location in
+ let zone = Locations.(enumerate_valid_bits Write loc) in
+ let state = kill zone state in
+ check "logic_assign" state
+
+ let evaluate_predicate _env _state _pred = Alarmset.Unknown
+ let reduce_by_predicate _env state _pred _positive = `Value state
+
+ let enter_scope _kf _varinfos state = state
+ let leave_scope _kf varinfos state =
+ let state = List.fold_left State.remove state varinfos in
+ check "leave_scope" state
+
+ let enter_loop _stmt state = state
+ let incr_loop_counter _stmt state = state
+ let leave_loop _stmt state = state
+
+ let introduce_globals _varinfos state = state
+ let initialize_variable _lval _location ~initialized:_ _value state = state
+ let initialize_variable_using_type _kind _varinfo state = state
+
+ let relate _kf bases state =
+ if intraprocedural ()
+ then Base.SetLattice.empty
+ else
+ let aux base acc =
+ try
+ let varinfo = Base.to_varinfo base in
+ let varset = Relations.find varinfo state.relations in
+ let baseset =
+ VariableSet.fold
+ (fun vi acc -> Base.Hptset.add (Base.of_varinfo vi) acc)
+ varset Base.Hptset.empty
+ in
+ Base.SetLattice.(join (inject baseset) acc)
+ with Base.Not_a_C_variable | Not_found -> acc
+ in
+ Base.Hptset.fold aux bases Base.SetLattice.empty
+
+ let filter _kf _kind bases state =
+ if intraprocedural ()
+ then state
+ else
+ let mem_vi varinfo = Base.Hptset.mem (Base.of_varinfo varinfo) bases in
+ let mem_pair pair =
+ let x, y = Pair.get pair in
+ mem_vi x && mem_vi y
+ in
+ let octagons = Octagons.filter mem_pair state.octagons in
+ let intervals = Intervals.filter mem_vi state.intervals in
+ let relations = Relations.filter mem_vi state.relations in
+ { state with octagons; intervals; relations; }
+
+ let reuse =
+ let cache = Hptmap_sig.PersistentCache "Octagons.reuse"
+ and symmetric = false
+ and idempotent = true
+ and decide _key left _right = left in
+ let join_oct = Octagons.internal_join ~cache ~symmetric ~idempotent ~decide
+ and join_itv = Intervals.internal_join ~cache ~symmetric ~idempotent ~decide
+ and join_rel = Relations.union in
+ fun _kf _bases ~current_input ~previous_output ->
+ if intraprocedural ()
+ then previous_output
+ else
+ let current_input = kill previous_output.modified current_input in
+ let prev_output = previous_output in
+ check "reuse result"
+ { octagons = join_oct prev_output.octagons current_input.octagons;
+ intervals = join_itv prev_output.intervals current_input.intervals;
+ relations = join_rel prev_output.relations current_input.relations;
+ modified = current_input.modified }
+
+ let name = "Octagon domain"
+ let log_category = Value_parameters.register_category "d-octagon"
+
+ let storage () = true
+end
+
+include Domain_builder.Complete (Domain)
diff --git a/src/plugins/value/domains/octagons.mli b/src/plugins/value/domains/octagons.mli
new file mode 100644
index 0000000000000000000000000000000000000000..88ba3269a6afbba3a7785bf5e4b4dc903a1969b9
--- /dev/null
+++ b/src/plugins/value/domains/octagons.mli
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Abstract_domain.Leaf
+ with type value = Cvalue.V.t
+ and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 5781d60bf7672faf0129790ab98f89cde419dd68..4261513ad85956b5344086030abbb39c7cef4759 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -98,6 +98,7 @@ module Config = struct
let cvalue = make 9 "cvalue" CvalueDomain.get (module Cvalue_domain.State)
let gauges = make 6 "gauges" GaugesDomain.get (module Gauges_domain.D)
+ let octagon = make 6 "octagon" OctagonDomain.get (module Octagons)
let inout = make 5 "inout" InoutDomain.get (module Inout_domain.D)
let traces = make 2 "traces" TracesDomain.get (module Traces_domain.D)
let printer = make 2 "printer" PrinterDomain.get (module Printer_domain)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 4c2909dbb757e52966e0dab66ec42e86473b87b2..3d4ebe9e437fdf5e913e368f9a5a9a0976ac5d69 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -132,6 +132,7 @@ module Config : sig
val equality: flag
val symbolic_locations: flag
val gauges: flag
+ val octagon: flag
val bitwise: flag
val inout: flag
val sign: flag
diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index 17adb02719337ef16ce67e9b106b1ac74647c4e8..83629ab5fc926f6d2d59ee2a77e93208b3df5d6a 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -240,18 +240,22 @@ module Make
raise [Result_found] when this execution exists, or do nothing. *)
let find_match_in_previous kf (map_inputs: InputBasesToCallEffect.t) state =
let aux_previous_call binputs hstates =
- (* restrict [state] to the inputs of this call *)
- let st_filtered = Domain.filter kf `Pre binputs state in
- try
- let bases, outputs, i = Domain.Hashtbl.find hstates st_filtered in
- (* We have found a previous execution, in which the outputs are
- [outputs]. Copy them in [state] and return this result. *)
- let process output =
- Domain.reuse kf bases ~current_input:state ~previous_output:output
- in
- let outputs = List.map process outputs in
- raise (Result_found (outputs, i))
- with Not_found -> ()
+ let brelated = Domain.relate kf binputs state in
+ if not Base.SetLattice.(is_included brelated (inject binputs))
+ then ()
+ else
+ (* restrict [state] to the inputs of this call *)
+ let st_filtered = Domain.filter kf `Pre binputs state in
+ try
+ let bases, outputs, i = Domain.Hashtbl.find hstates st_filtered in
+ (* We have found a previous execution, in which the outputs are
+ [outputs]. Copy them in [state] and return this result. *)
+ let process output =
+ Domain.reuse kf bases ~current_input:state ~previous_output:output
+ in
+ let outputs = List.map process outputs in
+ raise (Result_found (outputs, i))
+ with Not_found -> ()
in
Base.Hptset.Hashtbl.iter aux_previous_call map_inputs
diff --git a/src/plugins/value/utests b/src/plugins/value/utests
index bce097c3b1cfcea2ffac3282c750f757bd950bae..0b2cfea613cd1024532c5bbff89cae377bc921b5 100755
--- a/src/plugins/value/utests
+++ b/src/plugins/value/utests
@@ -12,7 +12,7 @@ if [ $res -ne 0 ]; then
fi
TESTS=(float value idct builtins)
-CONFIGS=(apron equalities bitwise symblocs gauges)
+CONFIGS=(apron equalities bitwise symblocs gauges octagons)
for C in ${CONFIGS[@]}
do
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 1de1430a7c101b4894bd7aa0176476f575738ee8..0f972433fe475cecf2c6f1a3981bafea11ed233f 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -167,6 +167,13 @@ module SymbolicLocsDomain = Domain_Parameter
let default = false
end)
+module OctagonDomain = Domain_Parameter
+ (struct
+ let option_name = "-eva-octagon-domain"
+ let help = "Use the octagon domain of Eva."
+ let default = false
+ end)
+
module BitwiseOffsmDomain = Domain_Parameter
(struct
let option_name = "-eva-bitwise-domain"
@@ -312,6 +319,21 @@ module EqualityCallFunction =
end)
let () = add_precision_dep EqualityCallFunction.parameter
+let () = Parameter_customize.set_group domains
+module OctagonCall =
+ Bool
+ (struct
+ let option_name = "-eva-octagon-through-calls"
+ let help = "Whether the relations inferred by the octagon domain are \
+ propagated through function calls. Disabled by default: \
+ the octagon analysis is intra-procedural, starting \
+ each function with an empty octagon state, \
+ and losing the octagons inferred at the end. \
+ The interprocedural analysis is more precise but slower."
+ let default = false
+ end)
+let () = add_precision_dep OctagonCall.parameter
+
let () = Parameter_customize.set_group domains
module Numerors_Real_Size =
Int
@@ -1520,7 +1542,9 @@ let () =
bind (module EqualityDomain) (fun n -> n > 1);
bind (module EqualityCall) (fun n -> if n > 2 then "formals" else "none");
bind (module GaugesDomain) (fun n -> n > 3);
- bind (module SplitReturn) (fun n -> if n > 4 then "auto" else "");
+ bind (module OctagonDomain) (fun n -> n > 4);
+ bind (module OctagonCall) (fun n -> n > 5);
+ bind (module SplitReturn) (fun n -> if n > 6 then "auto" else "");
()
let set_analysis n =
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 3e0fb860496b052159093bf18d4239e97379081a..8cda781691b11799c8f0277f35bab8803cc53206 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -32,6 +32,7 @@ module CvalueDomain: Parameter_sig.Bool
module EqualityDomain: Parameter_sig.Bool
module GaugesDomain: Parameter_sig.Bool
module SymbolicLocsDomain: Parameter_sig.Bool
+module OctagonDomain: Parameter_sig.Bool
module BitwiseOffsmDomain: Parameter_sig.Bool
module InoutDomain: Parameter_sig.Bool
module SignDomain: Parameter_sig.Bool
@@ -50,6 +51,8 @@ module EqualityCallFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
+module OctagonCall: Parameter_sig.Bool
+
module TracesUnrollLoop: Parameter_sig.Bool
module TracesUnifyLoop: Parameter_sig.Bool
module TracesDot: Parameter_sig.String
diff --git a/src/plugins/value/vtests b/src/plugins/value/vtests
index f03eac0072fb247668a1005922ae6f62319a7af6..2962dae8d845919d715d58362f08e97b0fd984d0 100755
--- a/src/plugins/value/vtests
+++ b/src/plugins/value/vtests
@@ -1,7 +1,7 @@
#!/bin/bash -eu
DEFAULT_TESTS=(float value idct builtins)
-CONFIGS=( apron equalities bitwise symblocs gauges)
+CONFIGS=( apron equalities bitwise symblocs gauges octagons)
ARGS=("${@-}")
diff --git a/tests/builtins/diff_octagons b/tests/builtins/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..0054c1a3abad131720e7bd2fa952732a6567d75c
--- /dev/null
+++ b/tests/builtins/diff_octagons
@@ -0,0 +1,335 @@
+diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_octagons/Longinit_sequencer.res.oracle
+327c327
+< tests/builtins/result/Longinit_sequencer.sav
+---
+> tests/builtins/result_octagons/Longinit_sequencer.sav
+568c568
+< tests/builtins/result/Longinit_sequencer.sav
+---
+> tests/builtins/result_octagons/Longinit_sequencer.sav
+diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_octagons/allocated.0.res.oracle
+273c273
+< j ∈ [1..2147483647]
+---
+> j ∈ {10}
+diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons/allocated.1.res.oracle
+191a192,194
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+208a212,214
+> strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+223a230,232
+> strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+238a248,250
+> strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+252,254c264,266
+< [eva] tests/builtins/allocated.c:82:
+< Call to builtin Frama_C_malloc_fresh for function malloc
+< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+---
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_7}
+323a336,356
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_31
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_32
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_33
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_34
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_35
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_36
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_37
+329,330d361
+< Trace partitioning superposing up to 300 states
+< [eva] tests/builtins/allocated.c:84:
+333a365,385
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+403c455,473
+< strong free on bases: {__malloc_main_l82_7}
+---
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+475c545,563
+< strong free on bases: {__malloc_main_l82_7}
+---
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+547c635,653
+< strong free on bases: {__malloc_main_l82_7}
+---
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+619c725,743
+< strong free on bases: {__malloc_main_l82_7}
+---
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+691c815,833
+< strong free on bases: {__malloc_main_l82_7}
+---
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+763c905,923
+< strong free on bases: {__malloc_main_l82_7}
+---
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+835c995,1013
+< strong free on bases: {__malloc_main_l82_7}
+---
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_31}
+905,907c1083,1084
+< [eva] tests/builtins/allocated.c:87: Call to builtin free
+< [eva:malloc] tests/builtins/allocated.c:87:
+< strong free on bases: {__malloc_main_l82_7}
+---
+> [eva] tests/builtins/allocated.c:81:
+> Trace partitioning superposing up to 500 states
+1069,1071c1246,1247
+< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
+< [1] ∈ {24} or UNINITIALIZED
+< [2] ∈ {27} or UNINITIALIZED
+---
+> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
+> [1] ∈ {17} or UNINITIALIZED
+1140a1317,1337
+> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_32[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_33[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_34[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_35[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_36[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+1184c1381
+< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
+---
+> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
+1207a1405,1411
+> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_34[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
+1231c1435
+< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
+---
+> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
+1243,1244c1447,1452
+< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
+< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
+---
+> __malloc_main_l82_30[0..2]; __malloc_main_l82_31[0..2];
+> __malloc_main_l82_32[0..2]; __malloc_main_l82_33[0..2];
+> __malloc_main_l82_34[0..2]; __malloc_main_l82_35[0..2];
+> __malloc_main_l82_36[0..2]; __malloc_main_l82_37[0..2];
+> __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
+> __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
+diff tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_octagons/imprecise.res.oracle
+224a225,226
+> [kernel] tests/builtins/imprecise.c:111:
+> more than 200(300) elements to enumerate. Approximating.
+233a236,237
+> [kernel] tests/builtins/imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d240
+< [kernel] tests/builtins/imprecise.c:111:
+< more than 200(300) elements to enumerate. Approximating.
+< [kernel] tests/builtins/imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
+diff tests/builtins/oracle/linked_list.1.res.oracle tests/builtins/oracle_octagons/linked_list.1.res.oracle
+506a507,508
+> [kernel] tests/builtins/linked_list.c:43:
+> more than 100(128) elements to enumerate. Approximating.
+508a511,512
+> [kernel] tests/builtins/linked_list.c:44:
+> more than 100(128) elements to enumerate. Approximating.
+600,603d603
+< [kernel] tests/builtins/linked_list.c:43:
+< more than 100(128) elements to enumerate. Approximating.
+< [kernel] tests/builtins/linked_list.c:44:
+< more than 100(128) elements to enumerate. Approximating.
+diff tests/builtins/oracle/malloc-optimistic.res.oracle tests/builtins/oracle_octagons/malloc-optimistic.res.oracle
+3520c3520
+< i ∈ [14..100]
+---
+> i ∈ {98; 99; 100}
+3524c3524
+< i ∈ [14..100]
+---
+> i ∈ {98; 99; 100}
diff --git a/tests/builtins/test_config_octagons b/tests/builtins/test_config_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..848a1c5fa4142125e0dc80808d0a8027d9760a2a
--- /dev/null
+++ b/tests/builtins/test_config_octagons
@@ -0,0 +1,3 @@
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-octagon-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/float/diff_octagons b/tests/float/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..806b63f0fdd00d77aa58baea79238e5893426733
--- /dev/null
+++ b/tests/float/diff_octagons
@@ -0,0 +1,18 @@
+Only in tests/float/oracle: absorb.res.oracle
+Only in tests/float/oracle: absorb_sav.err
+Only in tests/float/oracle: absorb_sav.res
+Only in tests/float/oracle: absorb_sav2.err
+Only in tests/float/oracle: absorb_sav2.res
+Only in tests/float/oracle: fval_test.res.oracle
+diff tests/float/oracle/nonlin.1.res.oracle tests/float/oracle_octagons/nonlin.1.res.oracle
+253a254,255
+> [eva:nonlin] tests/float/nonlin.c:101: non-linear 'f + f', lv 'f'
+> [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
+257d258
+< [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
+diff tests/float/oracle/nonlin.3.res.oracle tests/float/oracle_octagons/nonlin.3.res.oracle
+253a254,255
+> [eva:nonlin] tests/float/nonlin.c:101: non-linear 'f + f', lv 'f'
+> [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
+257d258
+< [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
diff --git a/tests/idct/diff_octagons b/tests/idct/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..46e477e3f73c2fc3d4aa05888afdfc1d43d7b003
--- /dev/null
+++ b/tests/idct/diff_octagons
@@ -0,0 +1,78 @@
+diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_octagons/ieee_1180_1990.res.oracle
+424a425,432
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+498a507,514
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+571a588,595
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+579a604,617
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+581a620,621
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+583a624,629
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+605a652,661
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+607a664,665
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+609a668,677
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
diff --git a/tests/test_config_octagons b/tests/test_config_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..701bc8421e733eb40844d0b62ab65400925c498e
--- /dev/null
+++ b/tests/test_config_octagons
@@ -0,0 +1,3 @@
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-octagon-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/diff_apron b/tests/value/diff_apron
index 2ead3a445bbc76a876c5e89fb0e57325a79f52a0..e43d97743cb15e14e2c12e5d5ca200006be5b5a1 100644
--- a/tests/value/diff_apron
+++ b/tests/value/diff_apron
@@ -670,6 +670,17 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.or
60a109,110
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
+diff tests/value/oracle/octagons.res.oracle tests/value/oracle_apron/octagons.res.oracle
+270,273c270,273
+< a ∈ [-1024..2147483647]
+< b ∈ [-1023..2147483647]
+< c ∈ [-1023..2147483647]
+< d ∈ [-1032..2147483647]
+---
+> a ∈ [-603..2147483646]
+> b ∈ [-602..2147483647]
+> c ∈ [-602..1446]
+> d ∈ [-611..2147483647]
diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_apron/offsetmap.0.res.oracle
62,63c62
< a[bits 0 to 7] ∈ {1; 6}
diff --git a/tests/value/diff_equalities b/tests/value/diff_equalities
index 821b7e3c2fc6803fa2584c2b2deedc7692ba8b60..83d093f00364f8bd80e50ed2ff37c260660b6c70 100644
--- a/tests/value/diff_equalities
+++ b/tests/value/diff_equalities
@@ -610,6 +610,15 @@ diff tests/value/oracle/nonlin.res.oracle tests/value/oracle_equalities/nonlin.r
< q ∈ {{ &x + [-400..400],0%4 }}
---
> q ∈ {{ &x }}
+diff tests/value/oracle/octagons.res.oracle tests/value/oracle_equalities/octagons.res.oracle
+29c29
+< Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+---
+> Frama_C_show_each_unreduced_unsigned: [0..4294967295], [6..4294967295]
+255c255
+< t ∈ [--..--] or UNINITIALIZED
+---
+> t ∈ [6..4294967295] or UNINITIALIZED
diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_equalities/offsetmap.0.res.oracle
38d37
< [eva] Recording results for g
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index e0312fea2b92804faca6c4ccae3d2e2afc83fda6..ab9ecdc28fc62ed33d66256204e38c85a05476ed 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -889,6 +889,34 @@ diff tests/value/oracle/noreturn.res.oracle tests/value/oracle_gauges/noreturn.r
> [eva] tests/value/noreturn.i:7: starting to merge loop iterations
36a40
> [eva] tests/value/noreturn.i:13: starting to merge loop iterations
+diff tests/value/oracle/octagons.res.oracle tests/value/oracle_gauges/octagons.res.oracle
+121,128d120
+< [eva:alarm] tests/value/octagons.c:107: Warning:
+< signed overflow. assert a + 2 ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:108: Warning:
+< signed overflow. assert b + 2 ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:110: Warning:
+< signed overflow. assert a + k ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:113: Warning:
+< signed overflow. assert -2147483648 ≤ c - a;
+130c122
+< [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
+---
+> [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2468..1]
+270,273c262,265
+< a ∈ [-1024..2147483647]
+< b ∈ [-1023..2147483647]
+< c ∈ [-1023..2147483647]
+< d ∈ [-1032..2147483647]
+---
+> a ∈ [-182..1866]
+> b ∈ [-181..1867]
+> c ∈ [-602..1446]
+> d ∈ [-190..1874]
+275c267
+< d2 ∈ [-2147483648..1]
+---
+> d2 ∈ [-2468..1]
diff tests/value/oracle/reduce_formals.res.oracle tests/value/oracle_gauges/reduce_formals.res.oracle
10a11
> [eva] tests/value/reduce_formals.i:5: starting to merge loop iterations
diff --git a/tests/value/diff_octagons b/tests/value/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..2b5ae606dfe09be4f1aa091b2742ab58c421eb1f
--- /dev/null
+++ b/tests/value/diff_octagons
@@ -0,0 +1,399 @@
+diff tests/value/oracle/alias.1.res.oracle tests/value/oracle_octagons/alias.1.res.oracle
+85c85
+< z ∈ {0; 1; 2}
+---
+> z ∈ {0; 2}
+diff tests/value/oracle/alias.2.res.oracle tests/value/oracle_octagons/alias.2.res.oracle
+76c76
+< z ∈ {-5; -4; -3; -2; -1; 0; 1; 1000}
+---
+> z ∈ {-2; -1; 0; 1000}
+diff tests/value/oracle/alias.3.res.oracle tests/value/oracle_octagons/alias.3.res.oracle
+67c67
+< z ∈ {0; 1; 2}
+---
+> z ∈ {0; 2}
+diff tests/value/oracle/alias.5.res.oracle tests/value/oracle_octagons/alias.5.res.oracle
+59a60
+> [eva] tests/value/alias.i:260: starting to merge loop iterations
+diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_octagons/alias.6.res.oracle
+82c82
+< t ∈ {4; 5; 6}
+---
+> t ∈ {5}
+87c87
+< y ∈ {0; 1}
+---
+> y ∈ {1}
+94,96c94,96
+< tz1 ∈ {0; 1}
+< tz2 ∈ {0; 1}
+< tz3 ∈ {0; 1}
+---
+> tz1 ∈ {1}
+> tz2 ∈ {1}
+> tz3 ∈ {1}
+diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_octagons/bitfield.res.oracle
+132a133,135
+> [eva] tests/value/bitfield.i:71:
+> Frama_C_show_each:
+> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
+diff tests/value/oracle/builtins_split.res.oracle tests/value/oracle_octagons/builtins_split.res.oracle
+70a71,84
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+81a96,109
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+diff tests/value/oracle/call_simple.res.oracle tests/value/oracle_octagons/call_simple.res.oracle
+28c28
+< c ∈ [--..--]
+---
+> c ∈ [-2147483648..2147483646]
+diff tests/value/oracle/descending.res.oracle tests/value/oracle_octagons/descending.res.oracle
+42c42
+< i ∈ {31; 32}
+---
+> i ∈ {31}
+diff tests/value/oracle/downcast.res.oracle tests/value/oracle_octagons/downcast.res.oracle
+61c61
+< [100000..2147483647], [100145..2147483647], [100145..2147483647]
+---
+> [100000..2147483502], [100145..2147483647], [100145..2147483647]
+167c167
+< x_0 ∈ [100000..2147483647]
+---
+> x_0 ∈ [100000..2147483502]
+diff tests/value/oracle/equality.res.oracle tests/value/oracle_octagons/equality.res.oracle
+29,30c29,30
+< y ∈ [0..42] or UNINITIALIZED
+< w ∈ [0..42] or UNINITIALIZED
+---
+> y ∈ [0..42]
+> w ∈ [0..42]
+diff tests/value/oracle/find_ivaltop.res.oracle tests/value/oracle_octagons/find_ivaltop.res.oracle
+32,33c32,33
+< j ∈ {0; 1; 2; 3; 4; 5; 6; 7}
+< X ∈ {1; 2; 3; 4; 5; 6; 7; 8}
+---
+> j ∈ {7}
+> X ∈ {8}
+39c39
+< \result FROM t[0..7]
+---
+> \result FROM t[7]
+44c44
+< t[0..7]
+---
+> t[7]
+diff tests/value/oracle/for_loops.3.res.oracle tests/value/oracle_octagons/for_loops.3.res.oracle
+20c20
+< v ∈ [0..2147483647]
+---
+> v ∈ [5..2147483647]
+diff tests/value/oracle/gauges.res.oracle tests/value/oracle_octagons/gauges.res.oracle
+209,210d208
+< [eva:alarm] tests/value/gauges.c:156: Warning:
+< signed overflow. assert -2147483648 ≤ toCopy - 1;
+272,273d269
+< [eva:alarm] tests/value/gauges.c:201: Warning:
+< signed overflow. assert -2147483648 ≤ numNonZero - 1;
+296,300d291
+< [eva] tests/value/gauges.c:218: Frama_C_show_each:
+< [eva] tests/value/gauges.c:218: Frama_C_show_each:
+< [eva] tests/value/gauges.c:218: Frama_C_show_each:
+< [eva:alarm] tests/value/gauges.c:220: Warning:
+< signed overflow. assert -2147483648 ≤ n - 1;
+787c778
+< numNonZero ∈ [-2147483648..8]
+---
+> numNonZero ∈ {-1}
+798c789
+< n ∈ [-2147483648..99]
+---
+> n ∈ {-1}
+859c850
+< toCopy ∈ [-2147483648..99]
+---
+> toCopy ∈ {-1}
+diff tests/value/oracle/loop.res.oracle tests/value/oracle_octagons/loop.res.oracle
+26c26
+< r ∈ [0..2147483646],0%2
+---
+> r ∈ [46..2147483646],0%2
+diff tests/value/oracle/loop_wvar.1.res.oracle tests/value/oracle_octagons/loop_wvar.1.res.oracle
+12,13d11
+< [eva:alarm] tests/value/loop_wvar.i:57: Warning:
+< signed overflow. assert next + 1 ≤ 2147483647;
+41c39
+< next ∈ [0..2147483647]
+---
+> next ∈ [0..25]
+diff tests/value/oracle/modulo.res.oracle tests/value/oracle_octagons/modulo.res.oracle
+40a41,56
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
+50a67,82
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+60a93,94
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
+diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_octagons/non_natural.res.oracle
+58a59,60
+> [kernel] tests/value/non_natural.i:30:
+> more than 200(12500) elements to enumerate. Approximating.
+65a68,69
+> [kernel] tests/value/non_natural.i:23:
+> more than 200(12500) elements to enumerate. Approximating.
+70a75,76
+> [kernel] tests/value/non_natural.i:24:
+> more than 200(12500) elements to enumerate. Approximating.
+78a85,86
+> [kernel] tests/value/non_natural.i:25:
+> more than 200(12500) elements to enumerate. Approximating.
+86a95,96
+> [kernel] tests/value/non_natural.i:26:
+> more than 200(12500) elements to enumerate. Approximating.
+94a105,106
+> [kernel] tests/value/non_natural.i:27:
+> more than 200(12500) elements to enumerate. Approximating.
+102a115,116
+> [kernel] tests/value/non_natural.i:28:
+> more than 200(12500) elements to enumerate. Approximating.
+110a125,126
+> [kernel] tests/value/non_natural.i:29:
+> more than 200(12500) elements to enumerate. Approximating.
+129,130d144
+< [kernel] tests/value/non_natural.i:23:
+< more than 200(12500) elements to enumerate. Approximating.
+133,146d146
+< [kernel] tests/value/non_natural.i:24:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:25:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:26:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:27:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:28:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:29:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:30:
+< more than 200(12500) elements to enumerate. Approximating.
+199a200,201
+> [kernel] tests/value/non_natural.i:39:
+> more than 200(12500) elements to enumerate. Approximating.
+diff tests/value/oracle/nonlin.res.oracle tests/value/oracle_octagons/nonlin.res.oracle
+105a106,107
+> [eva:nonlin] tests/value/nonlin.c:67: non-linear 'x * x', lv 'x'
+> [eva:nonlin] tests/value/nonlin.c:67: subdividing on x
+108a111,113
+> [eva:nonlin] tests/value/nonlin.c:68: subdividing on x
+> [eva:nonlin] tests/value/nonlin.c:68: non-linear 'y * y', lv 'y'
+> [eva:nonlin] tests/value/nonlin.c:68: subdividing on y
+111a117,118
+> [eva:nonlin] tests/value/nonlin.c:70: non-linear 'z * x + x * y', lv 'x'
+> [eva:nonlin] tests/value/nonlin.c:70: subdividing on x
+176,178c183,185
+< square ∈ [-48..400]
+< square2 ∈ [-48..400]
+< res ∈ [-144..400]
+---
+> square ∈ [-200..400]
+> square2 ∈ [-200..400]
+> res ∈ [-200..400]
+diff tests/value/oracle/plevel.res.oracle tests/value/oracle_octagons/plevel.res.oracle
+12d11
+< [eva] Recording results for main
+14a14
+> [eva] Recording results for main
+diff tests/value/oracle/ptr_relation.1.res.oracle tests/value/oracle_octagons/ptr_relation.1.res.oracle
+24c24
+< j ∈ {-1; 0; 1}
+---
+> j ∈ {0}
+diff tests/value/oracle/relation_reduction.res.oracle tests/value/oracle_octagons/relation_reduction.res.oracle
+24,27d23
+< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
+< accessing out of bounds index. assert 0 ≤ y;
+< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
+< accessing out of bounds index. assert y < 9;
+34,37c30,33
+< R1 ∈ [-2147483648..2147483637]
+< R2 ∈ [-2147483638..2147483647]
+< R3 ∈ [--..--]
+< R4 ∈ {0; 1; 2; 3; 4; 5}
+---
+> R1 ∈ {0; 2}
+> R2 ∈ {0; 12}
+> R3 ∈ {0; 7}
+> R4 ∈ {0; 2}
+48c44
+< R4 FROM tab[0..8]; x (and SELF)
+---
+> R4 FROM tab[0..5]; x (and SELF)
+53c49
+< y; t; tab[0..8]
+---
+> y; t; tab[0..5]
+diff tests/value/oracle/relation_shift.res.oracle tests/value/oracle_octagons/relation_shift.res.oracle
+18,25d17
+< [eva:alarm] tests/value/relation_shift.i:15: Warning:
+< signed overflow. assert -2147483648 ≤ x - y;
+< [eva:alarm] tests/value/relation_shift.i:15: Warning:
+< signed overflow. assert x - y ≤ 2147483647;
+< [eva:alarm] tests/value/relation_shift.i:16: Warning:
+< signed overflow. assert -2147483648 ≤ z - y;
+< [eva:alarm] tests/value/relation_shift.i:16: Warning:
+< signed overflow. assert z - y ≤ 2147483647;
+31,32c23,24
+< r1 ∈ [--..--]
+< r2 ∈ [--..--]
+---
+> r1 ∈ {2}
+> r2 ∈ {7}
+35,37c27,29
+< x ∈ [-2147483647..2147483647]
+< y ∈ [-2147483648..2147483646]
+< z ∈ [-2147483642..2147483647]
+---
+> x ∈ [-2147483646..2147483642]
+> y ∈ [-2147483648..2147483640]
+> z ∈ [-2147483641..2147483647]
+49,50c41,42
+< r1 ∈ [--..--]
+< r2 ∈ [--..--]
+---
+> r1 ∈ {2}
+> r2 ∈ {7}
+53,55c45,47
+< x ∈ [-2147483647..2147483647]
+< y ∈ [-2147483648..2147483646]
+< z ∈ [-2147483642..2147483647]
+---
+> x ∈ [-2147483646..2147483642]
+> y ∈ [-2147483648..2147483640]
+> z ∈ [-2147483641..2147483647]
+diff tests/value/oracle/relations.res.oracle tests/value/oracle_octagons/relations.res.oracle
+80,81c80,82
+< e ∈ [--..--]
+< f ∈ [--..--]
+---
+> e ∈ {1}
+> f[bits 0 to 7] ∈ {1; 4}
+> [bits 8 to 31] ∈ [--..--]
+diff tests/value/oracle/relations2.res.oracle tests/value/oracle_octagons/relations2.res.oracle
+25c25
+< len ∈ [--..--]
+---
+> len ∈ [0..1023]
+36,37c36
+< [eva] tests/value/relations2.i:17:
+< Frama_C_show_each_end: [0..4294967295], [0..64]
+---
+> [eva] tests/value/relations2.i:17: Frama_C_show_each_end: [0..1023], [0..64]
+59c58
+< n ∈ [0..512]
+---
+> n ∈ [1..512]
+69,71d67
+< [eva:alarm] tests/value/relations2.i:34: Warning:
+< accessing out of bounds index.
+< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
+80c76
+< n ∈ [0..512]
+---
+> n ∈ [1..512]
+97c93
+< n ∈ [0..512]
+---
+> n ∈ [1..512]
+140c136
+< len ∈ [--..--]
+---
+> len ∈ [0..1023]
+diff tests/value/oracle/semaphore.res.oracle tests/value/oracle_octagons/semaphore.res.oracle
+65c65
+< c ∈ {-26; -1}
+---
+> c ∈ {-1}
+diff tests/value/oracle/struct2.res.oracle tests/value/oracle_octagons/struct2.res.oracle
+81,84d80
+< accessing out of bounds index. assert 0 ≤ (int)(i + j);
+< [eva:alarm] tests/value/struct2.i:185: Warning:
+< accessing out of bounds index. assert (int)(i + j) < 2;
+< [eva:alarm] tests/value/struct2.i:185: Warning:
+106d101
+< [scope:rm_asserts] removing 2 assertion(s)
+diff tests/value/oracle/test.0.res.oracle tests/value/oracle_octagons/test.0.res.oracle
+17,18d16
+< [eva:alarm] tests/value/test.i:11: Warning:
+< signed overflow. assert j + ecart ≤ 2147483647;
+29c27
+< j ∈ [-1073741822..1]
+---
+> j ∈ {-1; 0; 1}
+diff tests/value/oracle/unroll.res.oracle tests/value/oracle_octagons/unroll.res.oracle
+22c22
+< G ∈ [17739..2147483647]
+---
+> G ∈ [17854..2147483647]
+diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_octagons/unroll_simple.res.oracle
+17c17
+< G ∈ [8772..2147483647]
+---
+> G ∈ [8896..2147483647]
diff --git a/tests/value/octagons.c b/tests/value/octagons.c
new file mode 100644
index 0000000000000000000000000000000000000000..6d98523df71429efead57e87dd17633ea4ca4560
--- /dev/null
+++ b/tests/value/octagons.c
@@ -0,0 +1,196 @@
+/* run.config*
+ STDOPT: +" -eva-octagon-domain -eva-octagon-through-calls -eva-msg-key=d-octagon,-d-cvalue"
+*/
+
+#include <__fc_builtin.h>
+
+volatile int undet;
+
+/* Minimal example from the Eva user manual. */
+void demo () {
+ int y = undet;
+ int k = Frama_C_interval(0, 10);
+ int x = y - k;
+ int r = x + 3 - y; // r \in [-7..3]
+ int t;
+ if (y > 15)
+ t = x; // t \in [6..]
+}
+
+/* Same example as [demo] but with other integer types. */
+void integer_types () {
+ unsigned int k, x, y, r, t;
+ y = undet;
+ k = Frama_C_interval(0, 10);
+ x = y - k; // No octagon inferred as [y - k] may overflow.
+ r = x + 3 - y;
+ if (y > 15)
+ t = x;
+ Frama_C_show_each_unreduced_unsigned(r, t);
+ char ck, cx, cy, cr, ct;
+ cy = undet;
+ ck = Frama_C_interval(0, 10);
+ cx = cy - ck; // An octagon should be inferred despite the casts to int.
+ cr = cx + 3 - cy;
+ if (cy > 15)
+ ct = cx;
+ Frama_C_show_each_reduced_char(cr, ct);
+}
+
+/* A test with multiple mathematical operations to complicate the inference
+ and use of octagons. */
+void arith () {
+ int k = Frama_C_interval(0, 4);
+ int a, b, x, y, r;
+ /* 1. Infer octagons from assignments. */
+ a = Frama_C_interval(5, 25);
+ b = Frama_C_interval(-12, 12);
+ x = 1 - (a + 2*k - 4); // x + a ∈ [-3..5]
+ y = 4*4 - k + (1 + b); // y - b ∈ [13..17]
+ /* 1.1 Use octagons in the evaluation of expressions. */
+ r = 2 * (10 - (b - 1 - y) - (x - 2 + a)); // r ∈ [42..66]
+ Frama_C_show_each_precise(r);
+ r = 2 * (10 - (b + x - 3 - y + a)); // r ∈ [42..66]
+ Frama_C_show_each_imprecise(r);
+ k = Frama_C_interval(0, 4);
+ /* 1.1 Use octagons to propagate variable reductions. */
+ if (12 - x < (k+1)*3) { // x > -3
+ r = 10 * a; // so a < 8
+ Frama_C_show_each(r); // {50; 60; 70}
+ }
+ /* 2. Infer octagons from conditions. */
+ a = Frama_C_interval(-1024, 1024);
+ b = Frama_C_interval(-1024, 1024);
+ if (20*k - a - 17 < 5 - b + (1 << 3) // a - b > -30
+ && a + (k+6)/2 - b <= 32) { // a - b <= 29
+ r = b - a;
+ Frama_C_show_each(r); // [-29..29]
+ }
+ if (a < b && b <= a)
+ Frama_C_show_each_BOTTOM(a, b);
+}
+
+/* Tests the join of the octagon domain. */
+void join () {
+ int a, b, r;
+ int k = Frama_C_interval(-1, 4);
+ if (undet) {
+ a = undet;
+ b = a + k;
+ } else {
+ a = Frama_C_interval(-32, -10);
+ b = k * 5;
+ }
+ // In both cases, we have b - a >= -1. The "else" branch was more precise.
+ r = b - a + 1;
+ Frama_C_show_each_join_positive(r);
+ if (undet) {
+ a = undet;
+ b = - (a + k);
+ } else {
+ a = Frama_C_interval(-32, -10);
+ b = k * 5;
+ }
+ // In both cases, we have b + a <= 10. The "then" branch was more precise.
+ r = b + a - 10;
+ Frama_C_show_each_join_negative(r);
+}
+
+/* Tests the octagon domain within loops. */
+void loop () {
+ int k = Frama_C_interval(-8, 8);
+ int a = Frama_C_interval(-1024, 1024);
+ int b = a + 1;
+ int c = a + 1;
+ int d = a + k;
+ for (int i = 0; i < 421; i++) {
+ a = a + 2;
+ b = b + 2; // The relation between a and b should be maintained in the loop.
+ c = c + 1; // The relation between a and c should be lost in the loop.
+ d = a + k; // This relation should be maintained.
+ }
+ int d1 = b - a;
+ int d2 = c - a;
+ int d3 = d - a;
+ Frama_C_show_each_singleton_1(d1);
+ Frama_C_show_each_imprecise(d2);
+ Frama_C_show_each_precise(d3);
+}
+
+/* Tests the soundness of the octagon domain in presence of pointers. */
+void pointers () {
+ int x, y, r;
+ int *px = &x, *pr = &r;
+ x = Frama_C_interval(-1024, 1024);
+ y = x + 1;
+ r = y - x;
+ Frama_C_show_each_singleton_1(r);
+ *px = Frama_C_interval(-1024, 1024);
+ Frama_C_show_each_singleton_1(r);
+ *pr = Frama_C_interval(-1024, 1024);
+ Frama_C_show_each_unknown(r);
+ r = y - x;
+ Frama_C_show_each_unknown(r);
+ y = x + 2;
+ r = y - x;
+ Frama_C_show_each_singleton_2(r);
+}
+
+/* Tests the saturation of octagons: inference of a relation between (x, z)
+ from relations between (x, y) and between (y, z). */
+void saturate () {
+ int k = Frama_C_interval(-6, 4);
+ int x = Frama_C_interval(-1024, 1024);
+ int y = k - x;
+ int z = y + 1;
+ int result = - z - x; // result == k + 1
+ Frama_C_show_each_saturate(result); // ∈ [-5..5]
+}
+
+int diff (int x, int y) { return x - y; }
+int neg (int x) { return -x; }
+
+/* Tests the propagation of octagons through function calls. */
+void interprocedural () {
+ int a = Frama_C_interval(-4, 12);
+ int b = Frama_C_interval(-4, 12);
+ int neg_a = neg(a);
+ int neg_b = neg(b);
+ /* [r1] is the direct difference [a-b], [r2] uses the result of the function
+ [neg] (and thus need the octagon inferred in [neg]), and [r3] calls the
+ function [diff] (and the analysis of [diff] needs the octagons inferred
+ here about a and b). */
+ int r1, r2, r3;
+ if (a > b) {
+ r1 = a - b;
+ r2 = a + neg_b;
+ r3 = diff (a, b);
+ } else {
+ r1 = b - a;
+ r2 = b + neg_a;
+ r3 = diff (b, a);
+ }
+ /* With the interprocedural octagons, r1, r2 and r3 must be equally precise. */
+ Frama_C_show_each_equal(r1, r2, r3);
+}
+
+/* Prints the octagons state. */
+void dump () {
+ char k = Frama_C_interval(0, 8);
+ char a = undet;
+ char b = a + k;
+ char c = b - k;
+ Frama_C_dump_each();
+}
+
+void main () {
+ demo ();
+ integer_types ();
+ arith ();
+ join ();
+ loop ();
+ pointers ();
+ saturate ();
+ interprocedural ();
+ dump ();
+}
diff --git a/tests/value/oracle/octagons.res.oracle b/tests/value/oracle/octagons.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2f2626a65ffa2d0009b042400cd207ba02de8264
--- /dev/null
+++ b/tests/value/oracle/octagons.res.oracle
@@ -0,0 +1,407 @@
+[kernel] Parsing tests/value/octagons.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 ∈ [--..--]
+[eva] computing for function demo <- main.
+ Called from tests/value/octagons.c:187.
+[eva] computing for function Frama_C_interval <- demo <- main.
+ Called from tests/value/octagons.c:12.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/octagons.c:12:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/value/octagons.c:13: Warning:
+ signed overflow. assert -2147483648 ≤ y - k;
+[eva:alarm] tests/value/octagons.c:14: Warning:
+ signed overflow. assert x + 3 ≤ 2147483647;
+[eva] Recording results for demo
+[eva] Done for function demo
+[eva] computing for function integer_types <- main.
+ Called from tests/value/octagons.c:188.
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+ Called from tests/value/octagons.c:24.
+[eva] tests/value/octagons.c:24:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:29:
+ Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+ Called from tests/value/octagons.c:32.
+[eva] tests/value/octagons.c:32:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:37:
+ Frama_C_show_each_reduced_char: [-7..3], [6..127]
+[eva] Recording results for integer_types
+[eva] Done for function integer_types
+[eva] computing for function arith <- main.
+ Called from tests/value/octagons.c:189.
+[eva] computing for function Frama_C_interval <- arith <- main.
+ Called from tests/value/octagons.c:43.
+[eva] tests/value/octagons.c:43:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- arith <- main.
+ Called from tests/value/octagons.c:46.
+[eva] tests/value/octagons.c:46:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- arith <- main.
+ Called from tests/value/octagons.c:47.
+[eva] tests/value/octagons.c:47:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:52: Frama_C_show_each_precise: [42..66],0%2
+[eva] tests/value/octagons.c:54: Frama_C_show_each_imprecise: [2..106],0%2
+[eva] computing for function Frama_C_interval <- arith <- main.
+ Called from tests/value/octagons.c:55.
+[eva] tests/value/octagons.c:55:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:59: Frama_C_show_each: {50; 60; 70}
+[eva] computing for function Frama_C_interval <- arith <- main.
+ Called from tests/value/octagons.c:62.
+[eva] tests/value/octagons.c:62:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- arith <- main.
+ Called from tests/value/octagons.c:63.
+[eva] tests/value/octagons.c:63:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:67: Frama_C_show_each: [-29..29]
+[eva] Recording results for arith
+[eva] Done for function arith
+[eva] computing for function join <- main.
+ Called from tests/value/octagons.c:190.
+[eva] computing for function Frama_C_interval <- join <- main.
+ Called from tests/value/octagons.c:76.
+[eva] tests/value/octagons.c:76:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/value/octagons.c:79: Warning:
+ signed overflow. assert -2147483648 ≤ a + k;
+[eva:alarm] tests/value/octagons.c:79: Warning:
+ signed overflow. assert a + k ≤ 2147483647;
+[eva] computing for function Frama_C_interval <- join <- main.
+ Called from tests/value/octagons.c:81.
+[eva] tests/value/octagons.c:81:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:86: Frama_C_show_each_join_positive: [0..53]
+[eva:alarm] tests/value/octagons.c:89: Warning:
+ signed overflow. assert -2147483648 ≤ a + k;
+[eva:alarm] tests/value/octagons.c:89: Warning:
+ signed overflow. assert a + k ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:89: Warning:
+ signed overflow. assert -((int)(a + k)) ≤ 2147483647;
+[eva] computing for function Frama_C_interval <- join <- main.
+ Called from tests/value/octagons.c:91.
+[eva] tests/value/octagons.c:91:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:96: Frama_C_show_each_join_negative: [-47..0]
+[eva] Recording results for join
+[eva] Done for function join
+[eva] computing for function loop <- main.
+ Called from tests/value/octagons.c:191.
+[eva] computing for function Frama_C_interval <- loop <- main.
+ Called from tests/value/octagons.c:101.
+[eva] tests/value/octagons.c:101:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- loop <- main.
+ Called from tests/value/octagons.c:102.
+[eva] tests/value/octagons.c:102:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:106: starting to merge loop iterations
+[eva:alarm] tests/value/octagons.c:107: Warning:
+ signed overflow. assert a + 2 ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:108: Warning:
+ signed overflow. assert b + 2 ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:110: Warning:
+ signed overflow. assert a + k ≤ 2147483647;
+[eva:alarm] tests/value/octagons.c:113: Warning:
+ signed overflow. assert -2147483648 ≤ c - a;
+[eva] tests/value/octagons.c:115: Frama_C_show_each_singleton_1: {1}
+[eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
+[eva] tests/value/octagons.c:117: Frama_C_show_each_precise: [-8..8]
+[eva] Recording results for loop
+[eva] Done for function loop
+[eva] computing for function pointers <- main.
+ Called from tests/value/octagons.c:192.
+[eva] computing for function Frama_C_interval <- pointers <- main.
+ Called from tests/value/octagons.c:124.
+[eva] tests/value/octagons.c:124:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:127: Frama_C_show_each_singleton_1: {1}
+[eva] computing for function Frama_C_interval <- pointers <- main.
+ Called from tests/value/octagons.c:128.
+[eva] tests/value/octagons.c:128:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:129: Frama_C_show_each_singleton_1: {1}
+[eva] computing for function Frama_C_interval <- pointers <- main.
+ Called from tests/value/octagons.c:130.
+[eva] tests/value/octagons.c:130:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:131: Frama_C_show_each_unknown: [-1024..1024]
+[eva] tests/value/octagons.c:133: Frama_C_show_each_unknown: [-2047..2049]
+[eva] tests/value/octagons.c:136: Frama_C_show_each_singleton_2: {2}
+[eva] Recording results for pointers
+[eva] Done for function pointers
+[eva] computing for function saturate <- main.
+ Called from tests/value/octagons.c:193.
+[eva] computing for function Frama_C_interval <- saturate <- main.
+ Called from tests/value/octagons.c:142.
+[eva] tests/value/octagons.c:142:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- saturate <- main.
+ Called from tests/value/octagons.c:143.
+[eva] tests/value/octagons.c:143:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:147: Frama_C_show_each_saturate: [-5..5]
+[eva] Recording results for saturate
+[eva] Done for function saturate
+[eva] computing for function interprocedural <- main.
+ Called from tests/value/octagons.c:194.
+[eva] computing for function Frama_C_interval <- interprocedural <- main.
+ Called from tests/value/octagons.c:155.
+[eva] tests/value/octagons.c:155:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- interprocedural <- main.
+ Called from tests/value/octagons.c:156.
+[eva] tests/value/octagons.c:156:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function neg <- interprocedural <- main.
+ Called from tests/value/octagons.c:157.
+[eva] Recording results for neg
+[eva] Done for function neg
+[eva] computing for function neg <- interprocedural <- main.
+ Called from tests/value/octagons.c:158.
+[eva] Recording results for neg
+[eva] Done for function neg
+[eva] computing for function diff <- interprocedural <- main.
+ Called from tests/value/octagons.c:167.
+[eva] Recording results for diff
+[eva] Done for function diff
+[eva] computing for function diff <- interprocedural <- main.
+ Called from tests/value/octagons.c:171.
+[eva] Recording results for diff
+[eva] Done for function diff
+[eva] tests/value/octagons.c:174:
+ Frama_C_show_each_equal: [0..16], [0..16], [0..16]
+[eva] Recording results for interprocedural
+[eva] Done for function interprocedural
+[eva] computing for function dump <- main.
+ Called from tests/value/octagons.c:195.
+[eva] computing for function Frama_C_interval <- dump <- main.
+ Called from tests/value/octagons.c:179.
+[eva] tests/value/octagons.c:179:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:183:
+ Frama_C_dump_each:
+ # Octagon domain:
+ {[ k - tmp ∈ {0}
+ a - b ∈ [-8..0]
+ b - c ∈ [0..8]
+ a - c ∈ [-8..8]
+ ]}
+ ==END OF DUMP==
+[eva] Recording results for dump
+[eva] Done for function dump
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function arith:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ {0; 1; 2; 3; 4}
+ a ∈ [-1024..1024]
+ b ∈ [-1024..1024]
+ x ∈ [-28..0]
+ y ∈ [1..29]
+ r ∈ [-29..106]
+[eva:final-states] Values at end of function demo:
+ Frama_C_entropy_source ∈ [--..--]
+ y ∈ [--..--]
+ k ∈ [0..10]
+ x ∈ [-2147483648..2147483644]
+ r ∈ [-7..3]
+ t ∈ [6..2147483644] or UNINITIALIZED
+[eva:final-states] Values at end of function diff:
+ __retres ∈ [0..16]
+[eva:final-states] Values at end of function dump:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ [0..8]
+ a ∈ [--..--]
+ b ∈ [--..--]
+ c ∈ [--..--]
+[eva:final-states] Values at end of function integer_types:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ [0..10]
+ x ∈ [--..--]
+ y ∈ [--..--]
+ r ∈ [--..--]
+ t ∈ [--..--] or UNINITIALIZED
+ ck ∈ [0..10]
+ cx ∈ [--..--]
+ cy ∈ [--..--]
+ cr ∈ [-7..3]
+ ct ∈ [6..127] or UNINITIALIZED
+[eva:final-states] Values at end of function join:
+ Frama_C_entropy_source ∈ [--..--]
+ a ∈ [--..--]
+ b ∈ [-2147483647..2147483647]
+ r ∈ [-47..0]
+ k ∈ {-1; 0; 1; 2; 3; 4}
+[eva:final-states] Values at end of function loop:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ [-8..8]
+ a ∈ [-1024..2147483647]
+ b ∈ [-1023..2147483647]
+ c ∈ [-1023..2147483647]
+ d ∈ [-1032..2147483647]
+ d1 ∈ {1}
+ d2 ∈ [-2147483648..1]
+ d3 ∈ [-8..8]
+[eva:final-states] Values at end of function neg:
+ __retres ∈ [-12..4]
+[eva:final-states] Values at end of function interprocedural:
+ Frama_C_entropy_source ∈ [--..--]
+ a ∈ [-4..12]
+ b ∈ [-4..12]
+ neg_a ∈ [-12..4]
+ neg_b ∈ [-12..4]
+ r1 ∈ [0..16]
+ r2 ∈ [0..16]
+ r3 ∈ [0..16]
+[eva:final-states] Values at end of function pointers:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ [-1024..1024]
+ y ∈ [-1022..1026]
+ r ∈ {2}
+ px ∈ {{ &x }}
+ pr ∈ {{ &r }}
+[eva:final-states] Values at end of function saturate:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ [-6..4]
+ x ∈ [-1024..1024]
+ y ∈ [-1030..1028]
+ z ∈ [-1029..1029]
+ result ∈ [-5..5]
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+[from] Computing for function arith
+[from] Computing for function Frama_C_interval <-arith
+[from] Done for function Frama_C_interval
+[from] Done for function arith
+[from] Computing for function demo
+[from] Done for function demo
+[from] Computing for function diff
+[from] Done for function diff
+[from] Computing for function dump
+[from] Done for function dump
+[from] Computing for function integer_types
+[from] Done for function integer_types
+[from] Computing for function join
+[from] Done for function join
+[from] Computing for function loop
+[from] Done for function loop
+[from] Computing for function neg
+[from] Done for function neg
+[from] Computing for function interprocedural
+[from] Done for function interprocedural
+[from] Computing for function pointers
+[from] Done for function pointers
+[from] Computing for function saturate
+[from] Done for function saturate
+[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 arith:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function demo:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function diff:
+ \result FROM x; y
+[from] Function dump:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function integer_types:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function join:
+ Frama_C_entropy_source FROM Frama_C_entropy_source; undet (and SELF)
+[from] Function loop:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function neg:
+ \result FROM x
+[from] Function interprocedural:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function pointers:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function saturate:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source; undet (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function arith:
+ Frama_C_entropy_source; k; a; b; x; y; r
+[inout] Inputs for function arith:
+ Frama_C_entropy_source
+[inout] Out (internal) for function demo:
+ Frama_C_entropy_source; y; k; x; r; t
+[inout] Inputs for function demo:
+ Frama_C_entropy_source; undet
+[inout] Out (internal) for function diff:
+ __retres
+[inout] Inputs for function diff:
+ \nothing
+[inout] Out (internal) for function dump:
+ Frama_C_entropy_source; k; tmp; a; b; c
+[inout] Inputs for function dump:
+ Frama_C_entropy_source; undet
+[inout] Out (internal) for function integer_types:
+ Frama_C_entropy_source; k; x; y; r; t; tmp; ck; cx; cy; cr; ct; tmp_0
+[inout] Inputs for function integer_types:
+ Frama_C_entropy_source; undet
+[inout] Out (internal) for function join:
+ Frama_C_entropy_source; a; b; r; k
+[inout] Inputs for function join:
+ Frama_C_entropy_source; undet
+[inout] Out (internal) for function loop:
+ Frama_C_entropy_source; k; a; b; c; d; i; d1; d2; d3
+[inout] Inputs for function loop:
+ Frama_C_entropy_source
+[inout] Out (internal) for function neg:
+ __retres
+[inout] Inputs for function neg:
+ \nothing
+[inout] Out (internal) for function interprocedural:
+ Frama_C_entropy_source; a; b; neg_a; neg_b; r1; r2; r3
+[inout] Inputs for function interprocedural:
+ Frama_C_entropy_source
+[inout] Out (internal) for function pointers:
+ Frama_C_entropy_source; x; y; r; px; pr
+[inout] Inputs for function pointers:
+ Frama_C_entropy_source
+[inout] Out (internal) for function saturate:
+ Frama_C_entropy_source; k; x; y; z; result
+[inout] Inputs for function saturate:
+ Frama_C_entropy_source
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source
+[inout] Inputs for function main:
+ Frama_C_entropy_source; undet