diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 0bfde596c3a5a58f79426bb00d5e24df90604f56..0c7e3ba7eeca445689d0faa9b82e4ac3955e2788 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -452,6 +452,7 @@ module Base = struct
let varname = Datatype.undefined
end)
let id = id
+ let pretty_debug = pretty
end
include Base
@@ -549,6 +550,17 @@ let of_string_exp e =
module SetLattice = Make_Hashconsed_Lattice_Set(Base)(Hptset)
+module BMap =
+ Hptmap.Make (Base) (Base) (Hptmap.Comp_unused)
+ (struct let v = [ [] ] end)
+ (struct let l = [ Ast.self ] end)
+
+type substitution = base Hptmap.Shape(Base).t
+
+let substitution_from_list list =
+ let add map (key, elt) = BMap.add key elt map in
+ let bmap = List.fold_left add BMap.empty list in
+ BMap.shape bmap
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/base.mli b/src/kernel_services/abstract_interp/base.mli
index 708c79c5579a7cd21c2b3a44e64001e47d2cbef7..adbbcbc800ddffd87125846e4e7241daf601803f 100644
--- a/src/kernel_services/abstract_interp/base.mli
+++ b/src/kernel_services/abstract_interp/base.mli
@@ -225,6 +225,17 @@ val register_memory_var : Cil_types.varinfo -> validity -> t
They are created only to fill the contents of another variable.
Their field [vsource] is set to false. *)
+
+(** {2 Substituting bases}
+ This is used to efficiently replace some bases by others in locations or
+ in memory states, for instance in {!Locations} or {!Lmap_sig}. *)
+
+type substitution = base Hptmap.Shape(Base).t
+(** Type used for the substitution between bases. *)
+
+val substitution_from_list: (base * base) list -> substitution
+(** Creates a substitution from an association list. *)
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 46906585f7665013e9e5de09741e9e87a4b31377..b2223cda94798f4fd226b56f777c6bb8dfa9e94e 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -638,6 +638,14 @@ struct
| Top -> Top
| Map m -> Map (M.remove b m)
+ let replace_base shape = function
+ | Bottom -> Bottom
+ | Top -> Top
+ | Map map as t ->
+ let decide _key = Offsetmap.join in
+ let modified, map = M.replace_key ~decide shape map in
+ if modified then Map map else t
+
let is_reachable = function
| Bottom -> false
| Top | Map _ -> true
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index 9a7ac8d40b99f7cf4072d0a67e24a5509661db74..f9c31abc77d4b466d0f36735b2c4c8e310e0ee22 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.mli
+++ b/src/kernel_services/abstract_interp/lmap_sig.mli
@@ -150,6 +150,11 @@ val filter_by_shape: 'a Hptmap.Shape(Base.Base).t -> t -> t
(** Removes the base if it is present. Does nothing otherwise. *)
val remove_base : Base.t -> t -> t
+(** [replace_bases substitition map] replaces some bases in [map]
+ according to [substitution]. If [substitution] conflates different bases,
+ the offsetmaps bound to these bases are joined. *)
+val replace_base: Base.substitution -> t -> t
+
(** {2 Iterators} *)
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index f5c126c7119a38108bfa9d98a3f9b0c2bec5ce0d..442b8d59bc652f8e903e810104b36a7dd8f74640 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -358,6 +358,19 @@ module Location_Bytes = struct
| Map _ -> false);
true
+ let replace_base substitution v =
+ let substitute replace make acc =
+ let modified, set' = replace substitution acc in
+ modified, if modified then make set' else v
+ in
+ match v with
+ | Top (Base.SetLattice.Top, _) -> false, v
+ | Top (Base.SetLattice.Set set, origin) ->
+ substitute Base.Hptset.replace (inject_top_origin_internal origin) set
+ | Map map ->
+ let decide _key = Ival.join in
+ substitute (M.replace_key ~decide) (fun m -> Map m) map
+
let overlaps ~partial ~size mm1 mm2 =
match mm1, mm2 with
| Top _, _ | _, Top _ -> intersects mm1 mm2
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 760e1b93fa61909cf5a2fe0326db8f63f205c7bc..4bea9a7b4e218c9c6ff972577fbfdf18904a6ae4 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -78,6 +78,11 @@ module Location_Bytes : sig
(** [add b i loc] binds [b] to [i] in [loc] when [i] is not {!Ival.bottom},
and returns {!bottom} otherwise. *)
+ val replace_base: Base.substitution -> t -> bool * t
+ (** [replace_base subst loc] changes the location [loc] by substituting the
+ pointed bases according to [subst]. If [substitution] conflates different
+ bases, the offsets bound to these bases are joined. *)
+
val diff : t -> t -> t
(** Over-approximation of difference. [arg2] needs to be exact or an
under_approximation. *)
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index d7725d945383f676f453e37184198766270b7d05..670978accabdaaddc3d066435e1648dd28eaacac 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -1131,6 +1131,48 @@ struct
let inter_with_shape shape map = merge_with_shape ~inter:true shape map
let diff_with_shape shape map = merge_with_shape ~inter:false shape map
+ (* Intersection and difference between a map and a shape. *)
+ let partition_with_shape =
+ let rec merge shape map =
+ match shape, map with
+ | Empty, _ -> Empty, map
+ | _, Empty -> Empty, Empty
+ | _, Leaf (key, _, _) -> if mem key shape then map, Empty else Empty, map
+ | Leaf (key, _, _), _ -> begin
+ try
+ let v = find key map in
+ wrap_Leaf key v, remove key map
+ with Not_found -> Empty, map
+ end
+ | Branch (p, m, s0, s1, _), Branch (q, n, t0, t1, _) ->
+ let rewrap p m u0 u1 =
+ if t0 == u0 && t1 == u1 then map
+ else if u0 == Empty then u1 else if u1 == Empty then u0
+ else wrap_Branch p m u0 u1
+ in
+ let rewrap_both p m (inter0, diff0) (inter1, diff1) =
+ rewrap p m inter0 inter1, rewrap p m diff0 diff1
+ in
+ if (p = q) && (m = n) then
+ (* The trees have the same prefix. Merge their sub-trees. *)
+ rewrap_both p m (merge s0 t0) (merge s1 t1)
+ else if (Big_Endian.shorter m n) && (match_prefix q p m) then
+ (* [q] contains [p]. Merge [map] with a sub-tree of [shape]. *)
+ if (q land m) = 0
+ then merge s0 map
+ else merge s1 map
+ else if (Big_Endian.shorter n m) && (match_prefix p q n) then
+ (* [p] contains [q]. Merge [shape] with a sub-tree of [map]. The other
+ sub-tree of [map] matches an empty shape. *)
+ if (p land n) = 0
+ then rewrap_both q n (merge shape t0) (Empty, t1)
+ else rewrap_both q n (Empty, t0) (merge shape t1)
+ else
+ (* The prefixes disagree: [map] matches an empty shape. *)
+ Empty, map
+ in
+ merge
+
let fold2_join_heterogeneous (type arg) (type result) ~cache ~empty_left ~empty_right ~both ~join ~empty =
let cache_merge = match cache with
| Hptmap_sig.NoCache -> (fun f x y -> f x y)
@@ -1302,6 +1344,23 @@ struct
in
aux
+ let replace_key ~decide shape map =
+ let cache = Hptmap_sig.NoCache in
+ let inter, diff = partition_with_shape shape map in
+ if is_empty inter
+ then false, map
+ else
+ let join = join ~cache ~symmetric:true ~idempotent:true ~decide in
+ let both _key value new_key = singleton new_key value in
+ let new_inter =
+ fold2_join_heterogeneous
+ ~cache
+ ~empty_left:(fun _ -> empty)
+ ~empty_right:(fun _ -> assert false)
+ ~empty
+ ~both ~join inter shape
+ in
+ true, join new_inter diff
let generic_predicate exn ~cache ~decide_fast ~decide_fst ~decide_snd ~decide_both =
if debug_cache then Format.eprintf "CACHE generic_predicate %s@." (fst cache);
diff --git a/src/libraries/utils/hptmap_sig.mli b/src/libraries/utils/hptmap_sig.mli
index 3fdc7a3eb082e3d848e9b2ef81e695e286b3cc22..c1aa0b93871cff65581819fe777fb173714f50b2 100644
--- a/src/libraries/utils/hptmap_sig.mli
+++ b/src/libraries/utils/hptmap_sig.mli
@@ -188,6 +188,11 @@ module type S = sig
efficient than successive calls to {!remove} or {!add} to build the
resulting map. *)
+ val partition_with_shape: 'a shape -> t -> t * t
+ (** [partition_with_shape s m] returns two maps [inter, diff] such that:
+ - [inter] contains the elements of [m] bound in the shape [s];
+ - [diff] contains the elements of [m] not bound in the shape [s]. *)
+
(** {2 Binary predicates} *)
type decide_fast = Done | Unknown
@@ -343,6 +348,15 @@ module type S = sig
called in an unspecified order. The results of the function may be cached,
depending on [cache]. *)
+ val replace_key: decide:(key -> v -> v -> v) -> key shape -> t -> bool * t
+ (** [replace_key ~decide shape map] substitute keys in [map] according to
+ [shape]: it returns the [map] in which all bindings from [key] to [v] such
+ that [key] is bound to [key'] in [shape] are replaced by a binding from
+ [key'] to [v]. If the new key [key'] was already bound in the map, or if
+ two keys are replaced by a same key [key'], the [decide] function is used
+ to compute the final value bound to [key'].
+ The returned boolean indicates whether the map has been modified: it is
+ false if the intersection between [shape] and [map] is empty. *)
(**/**) (* Undocumented. *)
val pretty_debug: Format.formatter -> t -> unit
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index 14afb981d47d767ccf65f6eddc36ba168cb9ac09..0d59892b55fe9aba6db38e25257df9cd95202dfc 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -76,6 +76,8 @@ module type S = sig
val shape: t -> unit shape
val from_shape: 'a shape -> t
+ val partition_with_shape: 'a shape -> t -> t * t
+
val fold2_join_heterogeneous:
cache:Hptmap_sig.cache_type ->
empty_left:('a shape -> 'b) ->
@@ -86,6 +88,8 @@ module type S = sig
t -> 'a shape ->
'b
+ val replace: elt shape -> t -> bool * t
+
val clear_caches: unit -> unit
val pretty_debug: t Pretty_utils.formatter
@@ -221,6 +225,10 @@ module Make(X: Hptmap.Id_Datatype)
let both k () v = both k v in
fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both ~join ~empty
+ let replace =
+ let decide _k () () = () in
+ replace_key ~decide
+
end
(*
diff --git a/src/libraries/utils/hptset.mli b/src/libraries/utils/hptset.mli
index ad71b75f4834ae4eeb2c2979e52d8c33b4bfc5fd..1da170653c0006277b2111ae767e974ab6a48d41 100644
--- a/src/libraries/utils/hptset.mli
+++ b/src/libraries/utils/hptset.mli
@@ -88,6 +88,11 @@ module type S = sig
val from_shape: 'a shape -> t
(** Build a set from another [elt]-indexed map or set. *)
+ val partition_with_shape: 'a shape -> t -> t * t
+ (** [partition_with_shape shape set] returns two sets [inter, diff] that are
+ respectively the intersection and the difference between [set] and
+ [shape]. *)
+
val fold2_join_heterogeneous:
cache:Hptmap_sig.cache_type ->
empty_left:('a shape -> 'b) ->
@@ -98,6 +103,11 @@ module type S = sig
t -> 'a shape ->
'b
+ val replace: elt shape -> t -> bool * t
+ (** [replace shape set] replaces the elements of [set] according to [shape].
+ The returned boolean indicates whether the set has been modified; it is
+ false when the intersection between [shape] and [set] is empty. *)
+
(** Clear all the caches used internally by the functions of this module.
Those caches are not project-aware, so this function must be called
at least each a project switch occurs. *)
diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index 8feb6f4e59dde504eb7ad2e4374c94867e39802a..89eb4a6a15c7c0f242611ebc534fea5aafa09d90 100644
--- a/src/plugins/e-acsl/tests/arith/functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/functions_rec.c
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: recursive logic functions
- STDOPT: +"-eva-ignore-recursive-calls"
+ STDOPT: +"-eva-unroll-recursive-calls 100"
*/
/*@ logic integer f1(integer n) =
diff --git a/src/plugins/e-acsl/tests/arith/longlong.i b/src/plugins/e-acsl/tests/arith/longlong.i
index 9be4c44511b20d6b432aee24fd7b92f026d3cd9f..9dc71da4e6dc44fc36bb79c1ed0dd5390cbf0137 100644
--- a/src/plugins/e-acsl/tests/arith/longlong.i
+++ b/src/plugins/e-acsl/tests/arith/longlong.i
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: upgrading longlong to GMP
- STDOPT: +"-eva-ignore-recursive-calls"
+ STDOPT: +"-eva-unroll-recursive-calls 8"
*/
unsigned long long my_pow(unsigned int x, unsigned int n) {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
index 490eda1facc8ddd5e0b0ea133de1d4f871d3e14f..a30ec62a8b4a0a1fc14312fac9b2ef01ef5888c9 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
@@ -8,80 +8,13 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:23: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:7: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f1_2 (__gen_e_acsl_f1_2 <- __gen_e_acsl_f1_2 :: tests/arith/functions_rec.c:7 <-
- __gen_e_acsl_f1 :: tests/arith/functions_rec.c:24 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/arith/functions_rec.c:24: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:24: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:10: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/arith/functions_rec.c:10: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/arith/functions_rec.c:10: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- division by zero. assert __gen_e_acsl_f2_8 ≢ 0;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow. assert __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert
- (int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8 ≤
- 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- division by zero. assert __gen_e_acsl_f2_13 ≢ 0;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:10: Warning:
- signed overflow.
- assert
- (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13 ≤
- 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:26: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:26: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:14: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/arith/functions_rec.c:14 <-
- __gen_e_acsl_f3 :: tests/arith/functions_rec.c:28 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/arith/functions_rec.c:28: Warning:
assertion got status unknown.
-[eva] tests/arith/functions_rec.c:17: Warning:
- recursive call during value analysis
- of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/arith/functions_rec.c:17 <-
- __gen_e_acsl_f4 :: tests/arith/functions_rec.c:30 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/arith/functions_rec.c:30: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:30: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index fc96bb91d0626f1828b71d3eb12c44e8ef57f99f..b766248de7c8fd4d07f231228583ebb240bd00a3 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -183,20 +183,6 @@ int __gen_e_acsl_f2(int n)
__e_acsl_assert(__gen_e_acsl_f2_13 != 0,1,"RTE","f2",
"division_by_zero: __gen_e_acsl_f2_13 != 0",
"tests/arith/functions_rec.c",10);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_13 ≢ 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13
- ≤ 2147483647;
- */
__gen_e_acsl_if_4 = (__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13;
}
return __gen_e_acsl_if_4;
@@ -216,20 +202,6 @@ int __gen_e_acsl_f2_2(long n)
__e_acsl_assert(__gen_e_acsl_f2_8 != 0,1,"RTE","f2_2",
"division_by_zero: __gen_e_acsl_f2_8 != 0",
"tests/arith/functions_rec.c",10);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_8 ≢ 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8
- ≤ 2147483647;
- */
__gen_e_acsl_if_3 = (__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8;
}
return __gen_e_acsl_if_3;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 015b45a630e6b6006768996e99dccb81acf5910e..21f7073ae453abd87367cfa6774390b8b8e87753 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -12,8 +12,6 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
}
tmp_0 = my_pow(x,n / (unsigned int)2);
tmp = (int)tmp_0;
- /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp * tmp; */
- /*@ assert Eva: signed_overflow: tmp * tmp ≤ 2147483647; */
tmp *= tmp;
if (n % (unsigned int)2 == (unsigned int)0) {
__retres = (unsigned long long)tmp;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
index a8d7dc220ee03e4929c36d12d7a5bd8e329e52dd..36e0f42013b7f8302a598494fa5d342a8b7a2b7e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
@@ -1,13 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/arith/longlong.i:9: Warning:
- recursive call during value analysis
- of my_pow (my_pow <- my_pow :: tests/arith/longlong.i:16 <- main). Assuming
- the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/arith/longlong.i:10: Warning:
- signed overflow. assert -2147483648 ≤ tmp * tmp;
-[eva:alarm] tests/arith/longlong.i:10: Warning:
- signed overflow. assert tmp * tmp ≤ 2147483647;
[eva:alarm] tests/arith/longlong.i:17: Warning:
function __gmpz_import: precondition got status unknown.
[eva:alarm] tests/arith/longlong.i:17: Warning:
diff --git a/src/plugins/e-acsl/tests/bts/bts1395.i b/src/plugins/e-acsl/tests/bts/bts1395.i
index ef01c83d78b3a55f12e943321f73fdc7567fe102..34b85b1ee8c73ac93cbf2eb25dde331690ad4ab0 100644
--- a/src/plugins/e-acsl/tests/bts/bts1395.i
+++ b/src/plugins/e-acsl/tests/bts/bts1395.i
@@ -1,6 +1,6 @@
/* run.config_ci
COMMENT: recursive function
- STDOPT: +"-eva-ignore-recursive-calls"
+ STDOPT: +"-eva-unroll-recursive-calls 5"
*/
/*@ requires n > 0; */
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
index 30c8d8ed4cd52200784001e557b21efd970c070b..efd026311297e55d8fefb674326118e6ece88624 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
@@ -1,16 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/bts/bts1395.i:9: Warning:
- recursive call during value analysis
- of __gen_e_acsl_fact (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:7 <-
- __gen_e_acsl_fact :: tests/bts/bts1395.i:13 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/bts/bts1395.i:9: Warning:
- signed overflow. assert -2147483648 ≤ n * tmp;
- (tmp from fact(n - 1))
-[eva:alarm] tests/bts/bts1395.i:9: Warning:
- signed overflow. assert n * tmp ≤ 2147483647;
- (tmp from fact(n - 1))
-[eva:alarm] tests/bts/bts1395.i:14: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
index 1e95f4093d1686374aeefee4b482a76c9516c257..7ffe91bbde5d7c8b8cc2d47711157452d4ab25d5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
@@ -16,8 +16,6 @@ int fact(int n)
}
tmp = __gen_e_acsl_fact(n - 1);
;
- /*@ assert Eva: signed_overflow: -2147483648 ≤ n * tmp; */
- /*@ assert Eva: signed_overflow: n * tmp ≤ 2147483647; */
__retres = n * tmp;
return_label: return __retres;
}
diff --git a/src/plugins/e-acsl/tests/constructs/decrease.i b/src/plugins/e-acsl/tests/constructs/decrease.i
index b5dc3a50ca7515eb3f4fa32bcff259c351083bce..569bcb71d0f339ffec25afb1935e3da6e30b0053 100644
--- a/src/plugins/e-acsl/tests/constructs/decrease.i
+++ b/src/plugins/e-acsl/tests/constructs/decrease.i
@@ -1,5 +1,5 @@
/* run.config_ci, run.config_dev
- STDOPT: +"-eva-ignore-recursive-calls -eva-slevel 7"
+ STDOPT: +"-eva-unroll-recursive-calls 10 -eva-slevel 7"
*/
// Test that the last iteration of the variant can be negative
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle
index 74f4f63423966d0396e43ebbb9a02c8887c3ddcf..2a909408ab28551a31c8128f578c384ab0e246df 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle
@@ -9,65 +9,3 @@
E-ACSL construct `decreases clause' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/constructs/decrease.i:43: Warning:
- recursive call during value analysis
- of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <-
- __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/constructs/decrease.i:43: Warning:
- recursive call during value analysis
- of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <-
- __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/constructs/decrease.i:43: Warning:
- signed overflow.
- assert -2147483648 ≤ tmp + tmp_0;
- (tmp from fib(n - 1), tmp_0 from fib(n - 2))
-[eva:alarm] tests/constructs/decrease.i:43: Warning:
- signed overflow.
- assert tmp + tmp_0 ≤ 2147483647;
- (tmp from fib(n - 1), tmp_0 from fib(n - 2))
-[eva:alarm] tests/constructs/decrease.i:75: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva] tests/constructs/decrease.i:58: Warning:
- recursive call during value analysis
- of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <-
- __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <-
- even :: tests/constructs/decrease.i:50 <-
- __gen_e_acsl_even :: tests/constructs/decrease.i:77 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/constructs/decrease.i:78: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva] tests/constructs/decrease.i:58: Warning:
- recursive call during value analysis
- of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <-
- __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <-
- even :: tests/constructs/decrease.i:50 <-
- __gen_e_acsl_even :: tests/constructs/decrease.i:79 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/constructs/decrease.i:80: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva] tests/constructs/decrease.i:52: Warning:
- recursive call during value analysis
- of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <-
- __gen_e_acsl_even :: tests/constructs/decrease.i:58 <-
- odd :: tests/constructs/decrease.i:47 <-
- __gen_e_acsl_odd :: tests/constructs/decrease.i:81 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/constructs/decrease.i:82: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva] tests/constructs/decrease.i:52: Warning:
- recursive call during value analysis
- of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <-
- __gen_e_acsl_even :: tests/constructs/decrease.i:58 <-
- odd :: tests/constructs/decrease.i:47 <-
- __gen_e_acsl_odd :: tests/constructs/decrease.i:83 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/constructs/decrease.i:84: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c
index 41a66ca7b5efb2a1f491aca7a9eefbe396862a59..116816df289b37cce0dcf9fe63c4b5fe6b748abf 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c
@@ -87,8 +87,6 @@ int fib(int n)
}
tmp = __gen_e_acsl_fib(n - 1);
tmp_0 = __gen_e_acsl_fib(n - 2);
- /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp + tmp_0; */
- /*@ assert Eva: signed_overflow: tmp + tmp_0 ≤ 2147483647; */
__retres = tmp + tmp_0;
return_label: return __retres;
}
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index a667687b8c603e5f9a1c51a5c2d30d39fde832ba..7c5861aa9420ac2df98b4be9602488d1d5e27355 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -251,16 +251,27 @@ module type Transfer = sig
stmt -> exp -> bool ->
(value, location, origin) valuation -> state -> state or_bottom
- (** [start_call stmt call valuation state] returns an initial state
+ (** [start_call stmt call recursion valuation state] returns an initial state
for the analysis of a called function. In particular, this function
should introduce the formal parameters in the state, if necessary.
- [stmt] is the statement of the call site;
- [call] represents the call: the called function and the arguments;
+ - [recursion] is the information needed to interpret a recursive call.
+ It is None if the call is not recursive.
- [state] is the abstract state at the call site, before the call;
- [valuation] is a cache for all values and locations computed during
- the evaluation of the function and its arguments. *)
+ the evaluation of the function and its arguments.
+
+ On recursive calls, [recursion] contains some substitution of variables
+ to be applied on the domain state to prevent mixing up local variables
+ and formal parameters of different recursive calls.
+ See {!Eval.recursion} for more details.
+ This substitution has been applied on values and expressions in [call],
+ but not in the [valuation] given as argument. If the domain uses some
+ information from the [valuation] on a recursive call, it must apply the
+ substitution on it. *)
val start_call:
- stmt -> (location, value) call ->
+ stmt -> (location, value) call -> recursion option ->
(value, location, origin) valuation -> state -> state or_bottom
(** [finalize_call stmt call ~pre ~post] computes the state after a function
@@ -268,10 +279,13 @@ module type Transfer = sig
end of the called function.
- [stmt] is the statement of the call site;
- [call] represents the function call and its arguments.
+ - [recursion] is the information needed to interpret a recursive call.
+ It is None if the call is not recursive.
- [pre] and [post] are the states before and at the end of the call
respectively. *)
val finalize_call:
- stmt -> (location, value) call -> pre:state -> post:state -> state or_bottom
+ stmt -> (location, value) call -> recursion option ->
+ pre:state -> post:state -> state or_bottom
(** Called on the Frama_C_show_each directives. Prints the internal properties
inferred by the domain in the [state] about the expression [exp]. Can use
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 9c2d3e85184dd5ab65a9e17762df7bb46f081255..9bfd7edafd34c312d3b529bd2ec54e7ce0b3c197 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -634,7 +634,11 @@ module Make (Man : Input) = struct
with
| Out_of_Scope _ -> `Value state
- let start_call _stmt call valuation state =
+ let start_call _stmt call recursion valuation state =
+ if recursion <> None
+ then
+ Value_parameters.abort ~current:true
+ "The binding to APRON domains does not support recursive calls.";
update valuation state >>- fun state ->
let eval = make_eval state in
let oracle = make_oracle valuation in
@@ -669,7 +673,7 @@ module Make (Man : Input) = struct
then `Bottom
else `Value state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 661b972b1ad7cc1f53fefcd7a1541b11d16f2aa4..80f885d59365f5a7cc965285394b602cf60d6a7e 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -230,15 +230,53 @@ module State = struct
Cvalue_transfer.assume stmt expr positive valuation s >>-: fun s ->
s, clob
- let start_call stmt call valuation (s, _clob) =
- Cvalue_transfer.start_call stmt call valuation s >>-: fun state ->
- state, Locals_scoping.bottom ()
-
- let finalize_call stmt call ~pre ~post =
- let (post_state, post_clob) = post
- and pre_state, clob = pre in
+ let is_direct_recursion stmt call =
+ try
+ let kf = Kernel_function.find_englobing_kf stmt in
+ Kernel_function.equal kf call.kf
+ with Not_found -> false (* Should not happen *)
+
+ let start_recursive_call stmt call recursion (state, clob) =
+ let direct = is_direct_recursion stmt call in
+ let state = Model.remove_variables recursion.withdrawal state in
+ let substitution = recursion.base_substitution in
+ let clob = if direct then clob else Locals_scoping.top () in
+ let state = Locals_scoping.substitute substitution clob state in
+ Model.replace_base substitution state
+
+ let start_call stmt call recursion valuation (state, clob) =
+ (* Uses the [valuation] to update the [state] before the substitution
+ for recursive calls. *)
+ Cvalue_transfer.update valuation state >>- fun state ->
+ let state =
+ match recursion with
+ | None -> state
+ | Some recursion -> start_recursive_call stmt call recursion (state, clob)
+ in
+ Cvalue_transfer.start_call stmt call recursion valuation state
+ >>-: fun state -> state, Locals_scoping.bottom ()
+
+ let finalize_recursive_call stmt call ~pre recursion state =
+ let direct = is_direct_recursion stmt call in
+ let pre, clob = pre in
+ let substitution = recursion.base_substitution in
+ let state = Model.replace_base substitution state in
+ let clob = if direct then clob else Locals_scoping.top () in
+ let state = Locals_scoping.substitute substitution clob state in
+ let shape = Base.Hptset.shape recursion.base_withdrawal in
+ let inter = Cvalue.Model.filter_by_shape shape pre in
+ Cvalue.Model.merge ~into:state inter
+
+ let finalize_call stmt call recursion ~pre ~post =
+ let (pre, clob) = pre in
+ let (post, post_clob) = post in
Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
- Cvalue_transfer.finalize_call stmt call ~pre:pre_state ~post:post_state
+ let post =
+ Extlib.opt_fold
+ (finalize_recursive_call stmt call ~pre:(pre, clob))
+ recursion post
+ in
+ Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
>>-: fun state ->
state, clob
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 1f2c66726233a8357c3b4bb193f38263caafd06b..26518aa8d7c76a6a249d3c082b9131c453b4bbda 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -204,14 +204,13 @@ let actualize_formals state arguments =
in
List.fold_left treat_one_formal state arguments
-let start_call _stmt call valuation state =
- let state = update valuation state in
+let start_call _stmt call _recursion _valuation state =
let with_formals = actualize_formals state call.arguments in
let stack_with_call = Value_util.call_stack () in
Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
`Value with_formals
-let finalize_call stmt call ~pre:_ ~post:state =
+let finalize_call stmt call _recursion ~pre:_ ~post:state =
(* Deallocate memory allocated via alloca().
To minimize computations, only do it for function definitions. *)
let state' =
diff --git a/src/plugins/value/domains/cvalue/locals_scoping.ml b/src/plugins/value/domains/cvalue/locals_scoping.ml
index 4dd0181e5d2bd153c4455415880c1b1b4b9e1826..9fc5b4d5deedf494e21a35cffe5fed9f5997aa1e 100644
--- a/src/plugins/value/domains/cvalue/locals_scoping.ml
+++ b/src/plugins/value/domains/cvalue/locals_scoping.ml
@@ -127,6 +127,31 @@ let make_escaping_fundec fundec clob vars state =
in
make_escaping ~exact:true ~escaping ~on_escaping ~within:clob.clob state
+let substitute substitution clob state =
+ (* Apply the [substitution] to [offsm]. If it is modified, bind the new
+ offsetmap to [base] in [state], and add the [base] to [set]. *)
+ let replace_offsm base offsm state =
+ let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
+ let offsm' = Cvalue.V_Offsetmap.map_on_values f offsm in
+ if Cvalue.V_Offsetmap.equal offsm' offsm
+ then state
+ else Cvalue.Model.add_base base offsm' state
+ in
+ (* Apply the substitution to the offsetmap bound to [base] in [state] *)
+ let replace_base base acc =
+ match Cvalue.Model.find_base base state with
+ | `Value offsm -> replace_offsm base offsm acc
+ | `Top | `Bottom -> acc
+ | exception Not_found -> acc
+ in
+ (* Iterate on all the bases that might contain a variable to substitute *)
+ try Base.SetLattice.fold replace_base clob.clob (replace_base Base.null state)
+ with Abstract_interp.Error_Top ->
+ (* [clob] is too imprecise. Iterate on the entire memory state instead,
+ which is much slower. *)
+ match state with
+ | Cvalue.Model.Top | Cvalue.Model.Bottom -> state
+ | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map state
(*
Local Variables:
diff --git a/src/plugins/value/domains/cvalue/locals_scoping.mli b/src/plugins/value/domains/cvalue/locals_scoping.mli
index bc78ce6973d84ed9fd0ff586c7612cd468ac2104..64cdf339a39ceacca0dd271eb12b6c2eea56da7d 100644
--- a/src/plugins/value/domains/cvalue/locals_scoping.mli
+++ b/src/plugins/value/domains/cvalue/locals_scoping.mli
@@ -70,6 +70,10 @@ val make_escaping_fundec:
[fdec] is used to detect whether we are deallocating the outer scope of a
function, in which case a different warning is emitted. *)
+val substitute:
+ Base.substitution -> clobbered_set -> Cvalue.Model.t -> Cvalue.Model.t
+(** [substitute substitution clob state] applies [substitution] to all pointer
+ values in the offsetmaps bound to variables in [clob] in [state]. *)
(*
Local Variables:
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index f19b48efa1217c95f8d54bc13b5930e2a7e4e2f0..0c5e09da764e81ee6ed1bd33f195255a9ed31e96 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -48,8 +48,7 @@ let simplify_call call =
{ kf = call.Eval.kf;
arguments = List.map simplify_argument call.Eval.arguments;
rest = List.map fst call.Eval.rest;
- return = call.Eval.return;
- recursive = call.Eval.recursive }
+ return = call.Eval.return; }
module Make_Minimal
(Value: Abstract_value.S)
@@ -82,10 +81,16 @@ module Make_Minimal
let assume stmt expr positive _valuation state =
Domain.assume stmt expr positive state
- let start_call stmt call _valuation state =
- `Value (Domain.start_call stmt (simplify_call call) state)
+ let start_call stmt call recursion _valuation state =
+ match recursion with
+ | None -> `Value (Domain.start_call stmt (simplify_call call) state)
+ | Some _ ->
+ (* TODO *)
+ Value_parameters.abort
+ "The domain %s does not support recursive call." Domain.name
- let finalize_call stmt call ~pre ~post =
+ let finalize_call stmt call recursion ~pre ~post =
+ assert (recursion = None);
Domain.finalize_call stmt (simplify_call call) ~pre ~post
let show_expr _valuation = Domain.show_expr
@@ -218,9 +223,18 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
Domain.assign kinstr lv expr value (record valuation) state
let assume stmt expr positive valuation state =
Domain.assume stmt expr positive (record valuation) state
- let start_call stmt call valuation state =
- `Value (Domain.start_call stmt call (record valuation) state)
- let finalize_call = Domain.finalize_call
+
+ let start_call stmt call recursion valuation state =
+ match recursion with
+ | None -> `Value (Domain.start_call stmt call (record valuation) state)
+ | Some _ ->
+ (* TODO *)
+ Value_parameters.abort
+ "The domain %s does not support recursive call." Domain.name
+
+ let finalize_call stmt call recursion =
+ assert (recursion = None);
+ Domain.finalize_call stmt call
let show_expr _valuation = Domain.show_expr
@@ -436,7 +450,7 @@ module Restrict
- otherwise, only propagate the state from the call site to kill the
properties that depend on locations written in the called functions. *)
- let start_call stmt call valuation state =
+ let start_call stmt call recursion valuation state =
(* Starts the call with mode [new_mode]. [previous_mode] is the current mode
of the caller. *)
let start_call_with_mode ?previous_mode ~new_mode state =
@@ -444,7 +458,7 @@ module Restrict
then
match previous_mode with
| Some mode when mode.current.write ->
- Domain.start_call stmt call valuation state >>-: fun state ->
+ Domain.start_call stmt call recursion valuation state >>-: fun state ->
Some (state, new_mode)
| _ ->
`Value (Some (start_analysis call state, new_mode))
@@ -465,13 +479,13 @@ module Restrict
| None, None ->
`Value None
- let finalize_call stmt call ~pre ~post =
+ let finalize_call stmt call recursion ~pre ~post =
match pre, post with
| None, _ | _, None -> `Value None
| Some (pre, pre_mode), Some (post, post_mode) ->
if post_mode.current.write
then
- Domain.finalize_call stmt call ~pre ~post >>-: fun state ->
+ Domain.finalize_call stmt call recursion ~pre ~post >>-: fun state ->
Some (state, pre_mode)
else
`Value (Some (post, pre_mode))
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 0ff4608c1cdc1bead64778c44b3c8d7d4fe61646..63fe0d3bdf20aea816374463d3a0df398431fafc 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -116,11 +116,12 @@ module Make
let assume stmt expr positive valuation state =
Domain.assume stmt expr positive (lift_valuation valuation) state
- let start_call stmt call valuation state =
- Domain.start_call stmt (lift_call call) (lift_valuation valuation) state
+ let start_call stmt call recursion valuation state =
+ Domain.start_call
+ stmt (lift_call call) recursion (lift_valuation valuation) state
- let finalize_call stmt call ~pre ~post =
- Domain.finalize_call stmt (lift_call call) ~pre ~post
+ let finalize_call stmt call recursion ~pre ~post =
+ Domain.finalize_call stmt (lift_call call) recursion ~pre ~post
let show_expr valuation = Domain.show_expr (lift_valuation valuation)
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 683892ef2dcc07bd5da22c1a3834d06a3437447a..4ea88b8b41f51be54b2ec089efb36e4f948599ed 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -155,18 +155,20 @@ module Make
Right.assume stmt expr positive (right_val valuation) right >>-: fun right ->
left, right
- let finalize_call stmt call ~pre ~post =
+ let finalize_call stmt call recursion ~pre ~post =
let pre_left, pre_right = pre
and left_state, right_state = post in
- Left.finalize_call stmt call ~pre:pre_left ~post:left_state
+ Left.finalize_call stmt call recursion ~pre:pre_left ~post:left_state
>>- fun left ->
- Right.finalize_call stmt call ~pre:pre_right ~post:right_state
+ Right.finalize_call stmt call recursion ~pre:pre_right ~post:right_state
>>-: fun right ->
left, right
- let start_call stmt call valuation (left, right) =
- Left.start_call stmt call (left_val valuation) left >>- fun left ->
- Right.start_call stmt call (right_val valuation) right >>-: fun right ->
+ let start_call stmt call recursion valuation (left, right) =
+ Left.start_call stmt call recursion (left_val valuation) left
+ >>- fun left ->
+ Right.start_call stmt call recursion (right_val valuation) right
+ >>-: fun right ->
left, right
let show_expr =
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 2849ec1f6f3181dc30a8be6536f26c0df68c57c9..74925890fdce72eaba7ab228afc9f19b2cfe097f 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -473,16 +473,28 @@ module Make
end
| _ -> `Value state
- let start_call _stmt call valuation state =
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ unscope state vars
+
+ let start_call _stmt call recursion valuation state =
let state =
- match call_init_state call.kf with
- | ISCaller -> assign_formals valuation call state
- | ISFormals -> assign_formals valuation call empty
- | ISEmpty -> empty
+ match recursion with
+ | Some recursion ->
+ (* No relation inferred from the assignment of formal parameters
+ for recursive calls, because the valuation cannot be used safely
+ as the substitution of local and formals variables has not been
+ applied to it. *)
+ start_recursive_call recursion state
+ | None ->
+ match call_init_state call.kf with
+ | ISCaller -> assign_formals valuation call state
+ | ISFormals -> assign_formals valuation call empty
+ | ISEmpty -> empty
in
`Value state
- let finalize_call _stmt call ~pre ~post =
+ let finalize_call _stmt call _recursion ~pre ~post =
if call_init_state call.kf = ISCaller then
`Value post (* [pre] was the state inferred in the caller, and it
has been updated during the analysis of [kf] into
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 00641adb100e2b346ca8c8de13da269f824c713e..23cef9f01a25a84154166592159a41ad9281d01c 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1208,7 +1208,7 @@ module D_Impl : Abstract_domain.S
try `Value (G.assign to_loc to_val lv.lval e state)
with Unassignable -> `Value (kill lv.lloc state)
- let finalize_call _stmt _call ~pre ~post =
+ let finalize_call _stmt _call _recursion ~pre ~post =
let state =
match function_calls_handling with
| FullInterprocedural -> post
@@ -1217,10 +1217,16 @@ module D_Impl : Abstract_domain.S
in
`Value state
- let start_call _stmt call valuation state =
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ remove_variables vars state
+
+ let start_call _stmt call recursion valuation state =
let state =
match function_calls_handling with
- | FullInterprocedural -> update valuation state
+ | FullInterprocedural ->
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
| IntraproceduralAll
| IntraproceduralNonReferenced -> `Value G.empty
in
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index a51098e16eb63723b7d82f5449f5e835ad5cf58f..bda7c81868aa9913ca0e5b03ba9d9f802203c482 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -241,9 +241,10 @@ module Internal
let effects = Transfer.effects_assume to_z e in
`Value (Transfer.catenate state effects)
- let start_call _stmt _call _valuation _state = `Value LatticeInout.empty
+ let start_call _stmt _call _recursion _valuation _state =
+ `Value LatticeInout.empty
- let finalize_call _stmt _call ~pre ~post =
+ let finalize_call _stmt _call _recursion ~pre ~post =
`Value (Transfer.catenate pre post)
let update _valuation state = `Value state
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 2be0ff0dfa9e97bd2e36809c8ff2c47a932fa51b..e45b1c875de6bb8e1421c9064e1366382cf1982f 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1216,17 +1216,29 @@ module Domain = struct
let assume _stmt _exp _bool = update
- let start_call _stmt call valuation state =
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ List.fold_left State.remove state vars
+
+ let start_call _stmt call recursion 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
+ match recursion with
+ | Some recursion ->
+ (* No relation inferred from the assignment of formal parameters
+ for recursive calls, because the valuation cannot be used safely
+ as the substitution of local and formals variables has not been
+ applied to it. *)
+ `Value (start_recursive_call recursion state)
+ | None ->
+ 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 =
+ let finalize_call _stmt _call _recursion ~pre ~post =
if intraprocedural ()
then `Value (kill post.modified pre)
else
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index a2d8355c3e27b361b452e9898deb331a9b9d2d0c..70f2f43cccafd606c62e5c4484da7feb9601dc4d 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -157,9 +157,15 @@ module Internal : Domain_builder.InputDomain
let assume _ _ _ _ state = `Value state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
- let start_call _stmt _call valuation state = update valuation state
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ Memory.remove_variables vars state
+
+ let start_call _stmt _call recursion valuation state =
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 94a2f4c5f6ce72aa1a962f391fe0a76ef151b060..339d8edb25a19e8e4eb85906a1fe8c10e9f2ae5b 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -52,11 +52,17 @@ module Make_Memory (Value: Value) = struct
module Initial_Values = struct let v = [] end
module Deps = struct let l = [Ast.self] end
- include Hptmap.Make (Base) (Value)(Hptmap.Comp_unused) (Initial_Values) (Deps)
+ include Hptmap.Make
+ (Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps)
let cache_name s =
Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)
+ let disjoint_union =
+ let cache = cache_name "union" in
+ let decide _key _v1 _v2 = assert false in
+ join ~cache ~symmetric:true ~idempotent:true ~decide
+
let narrow =
let module E = struct exception Bottom end in
let cache = cache_name "narrow" in
@@ -259,7 +265,14 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
abstraction of the domain itself. *)
let assume _stmt _expr _pos = update
- let start_call _stmt call _valuation state =
+ let start_recusive_call recursion state =
+ let state = remove_variables recursion.withdrawal state in
+ (* No collision should occur in the substitution. *)
+ let decide _key _v1 _v2 = assert false in
+ snd (replace_key ~decide recursion.base_substitution state)
+
+ let start_call _stmt call recursion _valuation state =
+ let state = Extlib.opt_fold start_recusive_call recursion state in
let bind_argument state argument =
let typ = argument.formal.vtype in
let loc = Main_locations.PLoc.eval_varinfo argument.formal in
@@ -269,8 +282,17 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
let state = List.fold_left bind_argument state call.arguments in
`Value state
- let finalize_call _stmt call ~pre:_ ~post =
+ let finalize_recursive_call ~pre recursion state =
+ let shape = Base.Hptset.shape recursion.base_withdrawal in
+ let inter = inter_with_shape shape pre in
+ let state = disjoint_union state inter in
+ (* No collision should occur in the substitution. *)
+ let decide _key _v1 _v2 = assert false in
+ snd (replace_key ~decide recursion.base_substitution state)
+
+ let finalize_call _stmt call recursion ~pre ~post =
let kf_name = Kernel_function.get_name call.kf in
+ let post = Extlib.opt_fold (finalize_recursive_call ~pre) recursion post in
match find_builtin kf_name, call.return with
| None, _ | _, None -> `Value post
| Some f, Some return ->
diff --git a/src/plugins/value/domains/simpler_domains.mli b/src/plugins/value/domains/simpler_domains.mli
index 37a1209a79b929a90d05f63ff1c3afd2adf57773..ba32d0d3d2e0fd94a2c579e668e52ec73563e775 100644
--- a/src/plugins/value/domains/simpler_domains.mli
+++ b/src/plugins/value/domains/simpler_domains.mli
@@ -42,7 +42,6 @@ type simple_call = {
rest: exp list; (* Extra arguments. *)
return: varinfo option; (* Fake varinfo where the result of the
call is stored. *)
- recursive: bool; (* Is the call recursive? *)
}
(** Simplest interface for an abstract domain. No exchange of information with
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 2c2f51d88a24600c8c1640d4496547dc9926f048..bd2fab8b55a914f5c6639aef3a8a5c494a2fc54d 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -563,9 +563,15 @@ module Internal : Domain_builder.InputDomain
let assume _stmt _exp _pos valuation state = update valuation state
- let start_call _stmt _call valuation state = update valuation state
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ Memory.remove_variables vars state
+
+ let start_call _stmt _call recursion valuation state =
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 408114d15682d5121126bb154111f216bf67c8f6..5f566f15944666fa24003a90c4c87db494064deb 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -865,7 +865,7 @@ module Internal = struct
let trans = Assume (stmt, e, pos) in
`Value (Traces.add_trans state trans)
- let start_call stmt call _valuation state =
+ let start_call stmt call _recursion _valuation state =
let kf = call.Eval.kf in
if Kernel_function.is_definition kf then
let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
@@ -890,7 +890,7 @@ module Internal = struct
(CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
in `Value {state with call_declared_function = true}
- let finalize_call _stmt call ~pre:_ ~post =
+ let finalize_call _stmt call _recursion ~pre:_ ~post =
if post.call_declared_function
then `Value {post with call_declared_function = false}
else
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5633d599dd564bf5884cb63af702ffe887c5eac9..0c90f11a4886e2b4ee61e7489581694a1039e50d 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -63,8 +63,8 @@ module Make
let update _ _ = `Value ()
let assign _ _ _ _ _ _ = `Value ()
let assume _ _ _ _ _ = `Value ()
- let start_call _ _ _ _ = `Value ()
- let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
+ let start_call _ _ _ _ _ = `Value ()
+ let finalize_call _ _ _ ~pre:_ ~post:_ = `Value ()
let show_expr _ _ _ _ = ()
let logic_assign _ _ _ = ()
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index b622130d6e7c272654cfa450ebc47e2f5d7232d1..ece699c60df2f50dfa57448e281799a191c9e1f8 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -160,7 +160,7 @@ module Make (Abstract: Abstractions.Eva) = struct
is the instruction at which the call takes place, and is used to update
the statuses of the preconditions of [kf]. If [show_progress] is true,
the callstack and additional information are printed. *)
- let compute_using_spec_or_body call_kinstr call state =
+ let compute_using_spec_or_body call_kinstr call recursion state =
let kf = call.kf in
Value_results.mark_kf_as_called kf;
let global = match call_kinstr with Kglobal -> true | _ -> false in
@@ -172,9 +172,10 @@ module Make (Abstract: Abstractions.Eva) = struct
Value_types.Callstack.pretty_short call_stack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc call_kinstr);
let use_spec =
- if call.recursive then
- `Spec (Recursion.empty_spec_for_recursive_call kf)
- else
+ match recursion with
+ | Some { depth } when depth >= Value_parameters.RecursiveUnroll.get () ->
+ `Spec (Recursion.get_spec call_kinstr kf)
+ | _ ->
match kf.fundec with
| Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)
| Definition (def, _) ->
@@ -210,8 +211,10 @@ module Make (Abstract: Abstractions.Eva) = struct
module MemExec = Mem_exec.Make (Abstract.Val) (Abstract.Dom)
- let compute_and_cache_call stmt call init_state =
- let default () = compute_using_spec_or_body (Kstmt stmt) call init_state in
+ let compute_and_cache_call stmt call recursion init_state =
+ let default () =
+ compute_using_spec_or_body (Kstmt stmt) call recursion init_state
+ in
if Value_parameters.MemExecAll.get () then
let args =
List.map (fun {avalue} -> Eval.value_assigned avalue) call.arguments
@@ -272,9 +275,9 @@ module Make (Abstract: Abstractions.Eva) = struct
| [state] -> `Value state
| s :: l -> `Value (List.fold_left Abstract.Dom.join s l)
- let compute_call_or_builtin stmt call state =
+ let compute_call_or_builtin stmt call recursion state =
match Builtins.find_builtin_override call.kf with
- | None -> compute_and_cache_call stmt call state
+ | None -> compute_and_cache_call stmt call recursion state
| Some (name, builtin, cacheable, spec) ->
Value_results.mark_kf_as_called call.kf;
let kinstr = Kstmt stmt in
@@ -329,9 +332,11 @@ module Make (Abstract: Abstractions.Eva) = struct
Value_util.push_call_stack kf Kglobal;
store_initial_state kf init_state;
let call =
- {kf; arguments = []; rest = []; return = None; recursive = false}
+ { kf; callstack = []; arguments = []; rest = []; return = None; }
+ in
+ let final_result =
+ compute_using_spec_or_body Kglobal call None init_state
in
- let final_result = compute_using_spec_or_body Kglobal call init_state in
let final_states = final_result.Transfer.states in
let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
Value_util.pop_call_stack ();
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 99d150435c7d019f1cb0bd1a88f5ecb76e347f02..a5abcb4b90ed4470cda6e8ad546d2b8e071ef496 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -21,50 +21,51 @@
(**************************************************************************)
open Cil_types
+open Eval
-(** Recursion *)
-
-(* Our current treatment for recursion -- use the specification for
- the function that begins the recursive cycle -- is incorrect for
- function with formals whose address is taken. Indeed, we do not know
- which "instance" of the formal is updated by the specification. In
- this case, warn the user. *)
-let check_formals_non_referenced kf =
- let formals = Kernel_function.get_formals kf in
- if List.exists (fun vi -> vi.vaddrof) formals then
- Value_parameters.error ~current:true ~once:true
- "function '%a' (involved in a recursive call) has a formal parameter \
- whose address is taken. Analysis may be unsound."
- Kernel_function.pretty kf
+module Varinfo = Cil_datatype.Varinfo
-let warn_recursive_call kf call_stack =
- if Value_parameters.IgnoreRecursiveCalls.get ()
- then begin
- Value_util.warning_once_current
- "@[recursive call@ during@ value@ analysis@ of %a \
- @[(%a <- %a)@].@ Assuming@ the call@ has@ no effect.@ \
- The analysis@ will@ be@ unsound.@]"
- Kernel_function.pretty kf Kernel_function.pretty kf
- Value_types.Callstack.pretty call_stack ;
- check_formals_non_referenced kf;
- Db.Value.recursive_call_occurred kf;
- end
- else begin
- Value_parameters.error ~once:true ~current:true
- "@[@[detected@ recursive@ call@ (%a <- %a)@]@;@[Use %s@ to@ \
- ignore@ (beware@ this@ will@ make@ the analysis@ unsound)@]@]"
- Kernel_function.pretty kf Value_types.Callstack.pretty call_stack
- Value_parameters.IgnoreRecursiveCalls.option_name;
- raise Db.Value.Aborted
- end
-
-(* Check whether the function at the top of the call-stack starts a
- recursive call. *)
-let is_recursive_call kf =
- let call_stack = Value_util.call_stack () in
- if List.exists (fun (f, _) -> f == kf) call_stack
- then (warn_recursive_call kf call_stack; true)
- else false
+let mark_unknown_requires kinstr kf funspec =
+ let stmt =
+ match kinstr with
+ | Kglobal -> assert false
+ | Kstmt stmt -> stmt
+ in
+ let emitter = Value_util.emitter in
+ let status = Property_status.Dont_know in
+ let emit_behavior behavior =
+ let emit_predicate predicate =
+ let ip = Property.ip_of_requires kf Kglobal behavior predicate in
+ Statuses_by_call.setup_precondition_proxy kf ip;
+ let property = Statuses_by_call.precondition_at_call kf ip stmt in
+ Property_status.emit ~distinct:true emitter ~hyps:[] property status
+ in
+ List.iter emit_predicate behavior.b_requires
+ in
+ List.iter emit_behavior funspec.spec_behavior
+
+let get_spec kinstr kf =
+ let funspec = Annotations.funspec ~populate:false kf in
+ if Cil.is_empty_funspec funspec then
+ Value_parameters.abort ~current:true
+ "@[Recursive call to %a@ without a specification.@ Try to increase@ \
+ the %s parameter@ or write a specification@ for function %a.@]"
+ Kernel_function.pretty kf
+ Value_parameters.RecursiveUnroll.name
+ Kernel_function.pretty kf
+ else
+ let depth = Value_parameters.RecursiveUnroll.get () in
+ let () =
+ Value_parameters.warning ~once:true ~current:true
+ "@[Using specification of function %a@ for recursive calls%s.@ \
+ Analysis of function %a@ is thus incomplete@ and its soundness@ \
+ relies on the written specification.@]"
+ Kernel_function.pretty kf
+ (if depth > 0 then Format.asprintf " of depth %i" depth else "")
+ Kernel_function.pretty kf
+ in
+ mark_unknown_requires kinstr kf funspec;
+ funspec
(* Find a spec for a function [kf] that begins a recursive call. If [kf]
has no existing specification, generate (an incorrect) one, and warn
@@ -89,7 +90,7 @@ let _spec_for_recursive_call kf =
~silent_about_merging_behav:true spec initial_spec;
spec
-let empty_spec_for_recursive_call kf =
+let _empty_spec_for_recursive_call kf =
let typ_res = Kernel_function.get_return_type kf in
let empty = Cil.empty_funspec () in
let assigns =
@@ -104,3 +105,79 @@ let empty_spec_for_recursive_call kf =
let bhv = Cil.mk_behavior ~assigns ~name:Cil.default_behavior_name () in
empty.spec_behavior <- [bhv];
empty
+
+
+(* -------------------------------------------------------------------------- *)
+
+module CallDepth =
+ Datatype.Pair_with_collections (Kernel_function) (Datatype.Int)
+ (struct let module_name = "CallDepth" end)
+
+module VarCopies =
+ Datatype.List (Datatype.Pair (Varinfo) (Varinfo))
+
+module VarStack =
+ State_builder.Hashtbl
+ (CallDepth.Hashtbl)
+ (VarCopies)
+ (struct
+ let name = "Eva.Recursion.VarStack"
+ let dependencies = [ Ast.self ]
+ let size = 9
+ end)
+
+let copy_variable fundec depth varinfo =
+ let name = Format.asprintf "\\copy<%s>[%i]" varinfo.vname depth in
+ let v = Cil.copyVarinfo varinfo name in
+ Cil.refresh_local_name fundec v;
+ v
+
+let make_stack (kf, depth) =
+ let fundec =
+ try Kernel_function.get_definition kf
+ with Kernel_function.No_Definition -> assert false
+ in
+ let vars = Kernel_function.(get_formals kf @ get_locals kf) in
+ let copy v = v, copy_variable fundec depth v in
+ List.map copy vars
+
+let get_stack kf depth = VarStack.memo make_stack (kf, depth)
+
+let make_recursion call depth =
+ let dkey = Value_parameters.dkey_recursion in
+ Value_parameters.feedback ~dkey ~once:true ~current:true
+ "@[detected recursive call@ of function %a.@]"
+ Kernel_function.pretty call.kf;
+ let substitution = get_stack call.kf depth in
+ let add_if_copy acc argument =
+ match argument.avalue with
+ | Copy ({ lval = Var vi, _ }, _) -> Varinfo.Set.add vi acc
+ | _ -> acc
+ in
+ let empty = Varinfo.Set.empty in
+ let copied_varinfos = List.fold_left add_if_copy empty call.arguments in
+ let may_be_used (vi, _) = vi.vaddrof || Varinfo.Set.mem vi copied_varinfos in
+ let substitution, withdrawal = List.partition may_be_used substitution in
+ let withdrawal = List.map fst withdrawal in
+ let base_of_varinfo (v1, v2) = Base.of_varinfo v1, Base.of_varinfo v2 in
+ let list_substitution = List.map base_of_varinfo substitution in
+ let base_substitution = Base.substitution_from_list list_substitution in
+ let list_withdrawal = List.map Base.of_varinfo withdrawal in
+ let base_withdrawal = Base.Hptset.of_list list_withdrawal in
+ { depth; substitution; base_substitution; withdrawal; base_withdrawal; }
+
+let make call =
+ let is_same_kf (f, _) = Kernel_function.equal f call.kf in
+ let previous_calls = List.filter is_same_kf call.callstack in
+ let depth = List.length previous_calls in
+ if depth > 0
+ then Some (make_recursion call depth)
+ else None
+
+let revert recursion =
+ let revert (v1, v2) = v2, v1 in
+ let substitution = List.map revert recursion.substitution in
+ let base_of_varinfo (v1, v2) = Base.of_varinfo v1, Base.of_varinfo v2 in
+ let list = List.map base_of_varinfo substitution in
+ let base_substitution = Base.substitution_from_list list in
+ { recursion with substitution; base_substitution; }
diff --git a/src/plugins/value/engine/recursion.mli b/src/plugins/value/engine/recursion.mli
index 3a3255c47d1b22827ef20c36d711d349c5cd1492..d4f21920b0e191596613912e99c2c79f0811af2d 100644
--- a/src/plugins/value/engine/recursion.mli
+++ b/src/plugins/value/engine/recursion.mli
@@ -23,12 +23,16 @@
(** Handling of recursion cycles in the callgraph *)
open Cil_types
+open Eval
-val is_recursive_call: kernel_function -> bool
-(** Given the current state of the call stack, detect whether the
- given given function would start a recursive cycle. *)
+(* Returns the specification for a recursive call to the given function. Fails
+ if the function has no specification. Marks the preconditions of the call
+ as unknowns. *)
+val get_spec: kinstr -> kernel_function -> funspec
-val empty_spec_for_recursive_call: kernel_function -> spec
-(** Generate an empty spec [assigns \nothing] or
- [assigns \result \from \nothing], to be used to "approximate" the
- results of a recursive call. *)
+(** Creates the information about a recursive call. *)
+val make: ('v, 'loc) call -> recursion option
+
+(** Changes the information about a recursive call to be used at the end
+ of the call. *)
+val revert: recursion -> recursion
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 040629aa88699be86afd064e0775d464398b4e34..7ba3de0d199c4f9439b87c9657f175d8ff83fc09 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -27,7 +27,7 @@ open Eval
module type S = sig
type state
type value
- type location
+ type loc
val assign: state -> kinstr -> lval -> exp -> state or_bottom
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
@@ -44,7 +44,7 @@ module type S = sig
builtin: bool;
}
val compute_call_ref:
- (stmt -> (location, value) call -> state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option ->state -> call_result) ref
end
(* Reference filled in by the callwise-inout callback *)
@@ -105,6 +105,17 @@ module DumpFileCounters =
let name = "Transfer_stmt.DumpFileCounters"
end)
+module VarHashtbl = Cil_datatype.Varinfo.Hashtbl
+
+let substitution_visitor table = object
+ inherit Visitor.frama_c_copy (Project.current ())
+
+ method! vvrbl varinfo =
+ match VarHashtbl.find_opt table varinfo with
+ | None -> Cil.JustCopy
+ | Some vi -> Cil.ChangeTo vi
+end
+
module Make (Abstract: Abstractions.Eva) = struct
module Value = Abstract.Val
@@ -114,7 +125,7 @@ module Make (Abstract: Abstractions.Eva) = struct
type state = Domain.t
type value = Value.t
- type location = Location.location
+ type loc = Location.location
(* When using a product of domains, a product of states may have no
concretization (if the domains have inferred incompatible properties)
@@ -295,13 +306,13 @@ module Make (Abstract: Abstractions.Eva) = struct
}
(* Forward reference to [Eval_funs.compute_call] *)
- let compute_call_ref
- : (stmt -> (location, value) call -> Domain.state -> call_result) ref
+ let compute_call_ref :
+ (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
= ref (fun _ -> assert false)
(* Returns the result of a call, and a boolean that indicates whether a
builtin has been used to interpret the call. *)
- let process_call stmt call valuation state =
+ let process_call stmt call recursion valuation state =
Value_util.push_call_stack call.kf (Kstmt stmt);
let cleanup () =
Value_util.pop_call_stack ();
@@ -312,10 +323,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let domain_valuation = Eval.to_domain_valuation valuation in
let res =
(* Process the call according to the domain decision. *)
- match Domain.start_call stmt call domain_valuation state with
+ match Domain.start_call stmt call recursion domain_valuation state with
| `Value state ->
Domain.Store.register_initial_state (Value_util.call_stack ()) state;
- !compute_call_ref stmt call state
+ !compute_call_ref stmt call recursion state
| `Bottom ->
{ states = `Bottom; cacheable = Cacheable; builtin=false }
in
@@ -449,11 +460,11 @@ module Make (Abstract: Abstractions.Eva) = struct
Kernel_function.get_formals kf @ locals
(* Do the call to one function. *)
- let do_one_call valuation stmt lv call state =
+ let do_one_call valuation stmt lv call recursion state =
let kf_callee = call.kf in
let pre = state in
(* Process the call according to the domain decision. *)
- let call_result = process_call stmt call valuation state in
+ let call_result = process_call stmt call recursion valuation state in
call_result.cacheable,
call_result.states >>- fun result ->
let leaving_vars = leaving_vars kf_callee in
@@ -472,22 +483,15 @@ module Make (Abstract: Abstractions.Eva) = struct
>>- fun reductions ->
(* The formals (and the locals) of the called function leave scope. *)
let post = Domain.leave_scope kf_callee leaving_vars state in
+ let recursion = Option.map Recursion.revert recursion in
(* Computes the state after the call, from the post state at the end of
the called function, and the pre state at the call site. *)
- Domain.finalize_call stmt call ~pre ~post >>- fun state ->
+ Domain.finalize_call stmt call recursion ~pre ~post >>- fun state ->
(* Backward propagates the [reductions] on the concrete arguments. *)
reduce_arguments reductions state >>- fun state ->
treat_return ~kf_callee lv call.return stmt state
- and process_recursive state =
- (* When the call is recursive, formals have not been added to the
- domains. Do not reduce them, and more importantly, do not remove
- them from the scope. (Because the instance from the initial,
- non-recursive, call are still present.) *)
- Domain.finalize_call stmt call ~pre ~post:state >>- fun state ->
- treat_return ~kf_callee lv call.return stmt state
in
let states =
- let process = if call.recursive then process_recursive else process in
List.fold_left
(fun acc return -> Bottom.add_to_list (process return) acc)
[] result
@@ -533,30 +537,45 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Create an Eval.call *)
let create_call kf args =
- let recursive = Recursion.is_recursive_call kf in
let return = Library_functions.get_retres_vi kf in
+ let callstack = Value_util.call_stack () in
let arguments, rest =
- if recursive then
- (* For recursive calls, we evaluate 'assigns \result \from \nothing'
- using a specification. We generate a dummy [call] object in which
- formals are not present. This way, domains will not overwrite
- the formals of the recursive function (which would be present
- in scope twice). *)
- [], []
- else
- let formals = Kernel_function.get_formals kf in
- let rec format_arguments acc args formals = match args, formals with
- | _, [] -> acc, args
- | [], _ -> assert false
- | (concrete, avalue) :: args, formal :: formals ->
- let argument = { formal ; concrete; avalue } in
- format_arguments (argument :: acc) args formals
- in
- let arguments, rest = format_arguments [] args formals in
- let arguments = List.rev arguments in
- arguments, rest
+ let formals = Kernel_function.get_formals kf in
+ let rec format_arguments acc args formals = match args, formals with
+ | _, [] -> acc, args
+ | [], _ -> assert false
+ | (concrete, avalue) :: args, formal :: formals ->
+ let argument = { formal ; concrete; avalue } in
+ format_arguments (argument :: acc) args formals
+ in
+ let arguments, rest = format_arguments [] args formals in
+ let arguments = List.rev arguments in
+ arguments, rest
+ in
+ {kf; callstack; arguments; rest; return; }
+
+ let replace_value visitor substitution = function
+ | Assign value -> Assign (Value.replace_base substitution value)
+ | Copy (loc, flagged) ->
+ let v = flagged.v >>-: Value.replace_base substitution in
+ let flagged = { flagged with v } in
+ let lloc = Location.replace_base substitution loc.lloc in
+ let lval = Visitor.visitFramacLval visitor loc.lval in
+ let loc = { loc with lval; lloc } in
+ Copy (loc, flagged)
+
+ let replace_recursive_call recursion call =
+ let tbl = VarHashtbl.create 9 in
+ List.iter (fun (v1, v2) -> VarHashtbl.add tbl v1 v2) recursion.substitution;
+ let visitor = substitution_visitor tbl in
+ let base_substitution = recursion.base_substitution in
+ let replace_arg argument =
+ let concrete = Visitor.visitFramacExpr visitor argument.concrete in
+ let avalue = replace_value visitor base_substitution argument.avalue in
+ { argument with concrete; avalue }
in
- {kf; arguments; rest; return; recursive}
+ let arguments = List.map replace_arg call.arguments in
+ { call with arguments; }
let make_call ~subdivnb kf arguments valuation state =
(* Evaluate the arguments of the call. *)
@@ -564,8 +583,9 @@ module Make (Abstract: Abstractions.Eva) = struct
compute_actuals ~subdivnb ~determinate valuation state arguments
>>=: fun (args, valuation) ->
let call = create_call kf args in
- call, valuation
-
+ let recursion = Recursion.make call in
+ let call = Extlib.opt_fold replace_recursive_call recursion call in
+ call, recursion, valuation
(* ----------------- show_each and dump_each directives ------------------- *)
@@ -744,11 +764,13 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Create the call. *)
let eval, alarms = make_call ~subdivnb kf args valuation state in
Alarmset.emit ki_call alarms;
- eval >>- fun (call, valuation) ->
+ eval >>- fun (call, recursion, valuation) ->
(* Register the call. *)
Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
(* Do the call. *)
- let c, states = do_one_call valuation stmt lval_option call state in
+ let c, states =
+ do_one_call valuation stmt lval_option call recursion state
+ in
(* If needed, propagate that callers cannot be cached. *)
if c = NoCacheCallers then
cacheable := NoCacheCallers;
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index af7e5fa3e7383125abfbb9101e64a23d5b8f9baf..87c505e24111ca06f51ce4a9cb5ee3fe9178c788 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -29,7 +29,7 @@ module type S = sig
type state
type value
- type location
+ type loc
val assign: state -> kinstr -> lval -> exp -> state or_bottom
@@ -55,13 +55,13 @@ module type S = sig
}
val compute_call_ref:
- (stmt -> (location, value) call -> state -> call_result) ref
+ (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
end
module Make (Abstract: Abstractions.Eva)
: S with type state = Abstract.Dom.t
and type value = Abstract.Val.t
- and type location = Abstract.Loc.location
+ and type loc = Abstract.Loc.location
(*
Local Variables:
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 8aab315162a3557beba3835d1b3c821ded536474..7a12a168d662e1d7225531415b317ba18e5bfbaf 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -240,12 +240,24 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned;
}
+
+type call_site = kernel_function * kinstr
+type callstack = call_site list
+
type ('loc, 'value) call = {
kf: kernel_function;
+ callstack: callstack;
arguments: ('loc, 'value) argument list;
rest: (exp * ('loc, 'value) assigned) list;
return: varinfo option;
- recursive: bool;
+}
+
+type recursion = {
+ depth: int;
+ substitution: (varinfo * varinfo) list;
+ base_substitution: Base.substitution;
+ withdrawal: varinfo list;
+ base_withdrawal: Base.Hptset.t;
}
type cacheable = Cacheable | NoCache | NoCacheCallers
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index e050aae784876740fd329e70493c9876495131ef..5714172358fc24dfbc4ba07a05c4fe2722fcb2b0 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -215,7 +215,6 @@ type 'location logic_assign =
(** {2 Interprocedural Analysis } *)
(* -------------------------------------------------------------------------- *)
-
(** Argument of a function call. *)
type ('loc, 'value) argument = {
formal: varinfo; (** The formal argument of the called function. *)
@@ -223,19 +222,55 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned; (** The value of the concrete argument. *)
}
+(** A call_stack is a list, telling which function was called at which
+ site. The head of the list tells about the latest call. *)
+
+(** A call site: the function called, and the call statement
+ (or [Kglobal] for the main function. *)
+type call_site = kernel_function * kinstr
+
+(* A call stack is a list of call sites. The head is the latest call.
+ The last element is the main function. *)
+type callstack = call_site list
+
(** A function call. *)
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
+ callstack: callstack; (** The current callstack
+ (without this call). *)
arguments: ('loc, 'value) argument list; (** The arguments of the call. *)
rest: (exp * ('loc, 'value) assigned) list; (** Extra-arguments. *)
return: varinfo option; (** Fake varinfo to store the
return value of the call.
Same varinfo for every
call to a given function. *)
- recursive: bool;
}
-(* Can the results of a function call be cached with memexec? *)
+(** Information needed to interpret a recursive call.
+ The local variables and formal parameters of different recursive calls
+ should not be mixed up. Those of the current call must be temporary withdraw
+ or replaced from the domain states before starting the new recursive call,
+ and the inverse transformation must be made at the end of the call. *)
+type recursion = {
+ depth: int;
+ (** Depth of the recursive call, i.e. the number of previous call to the
+ called function in the current callstack. *)
+ substitution: (varinfo * varinfo) list;
+ (** List of variables substitutions to be performed by the domains: for each
+ pair, the first variable must be replaced by the second one in the domain
+ state. *)
+ base_substitution: Base.substitution;
+ (** Same substitution as the previous field, for bases. *)
+ withdrawal: varinfo list;
+ (** List of variables to be temporary removed from the state at the start of a
+ new recursive call (by the function [start_call] of the abstract domains),
+ or to be put back in the state at the end of a recursive call (by the
+ function [finalize_call] of the abstract domains). *)
+ base_withdrawal: Base.Hptset.t;
+ (** Same withdrawal as the previous field, for bases. *)
+}
+
+(** Can the results of a function call be cached with memexec? *)
type cacheable =
| Cacheable (** Functions whose result can be safely cached *)
| NoCache (** Functions whose result should not be cached, but for
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 00f2871518eca24188ce2f575e0bfdc71771c7c6..13a005dd2afb149c347bfdd8ed45f51fd90b3262 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -24,11 +24,7 @@ open Cil_types
(* Callstacks related types and functions *)
-(* Function called, and calling instruction. *)
-type call_site = (kernel_function * kinstr)
-type callstack = call_site list
-
-let call_stack : callstack ref = ref []
+let call_stack : Value_types.callstack ref = ref []
(* let call_stack_for_callbacks : (kernel_function * kinstr) list ref = ref [] *)
let clear_call_stack () =
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 61df6ce5331ea7d09ef8efb35e2e607bb5f3d0e5..0bfe89cbe916816878319417b0dc123ad79bea1c 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -24,11 +24,6 @@ open Cil_types
(** {2 Callstacks related types and functions} *)
-(** A call_stack is a list, telling which function was called at which
- site. The head of the list tells about the latest call. *)
-type call_site = (kernel_function * kinstr)
-type callstack = call_site list
-
(** Functions dealing with call stacks. *)
val clear_call_stack : unit -> unit
val pop_call_stack : unit -> unit
@@ -36,7 +31,7 @@ val push_call_stack : kernel_function -> kinstr -> unit
(** The current function is the one on top of the call stack. *)
val current_kf : unit -> kernel_function
-val call_stack : unit -> callstack
+val call_stack : unit -> Value_types.callstack
(** Prints the current callstack. *)
val pp_callstack : Format.formatter -> unit
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index c6027b04ee524ef02df19d3980becc6a53f9a74b..a3d0cb97c5034a4eff502b76729e1d3245bf20a6 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -82,11 +82,13 @@ let dkey_incompatible_states = register_category "incompatible-states"
let dkey_iterator = register_category "iterator"
let dkey_callbacks = register_category "callbacks"
let dkey_widening = register_category "widening"
+let dkey_recursion = register_category "recursion"
let () =
let activate dkey = add_debug_keys dkey in
List.iter activate
- [dkey_initial_state; dkey_final_states; dkey_summary; dkey_cvalue_domain]
+ [dkey_initial_state; dkey_final_states; dkey_summary; dkey_cvalue_domain;
+ dkey_recursion; ]
(* Warning categories. *)
let wkey_alarm = register_warn_category "alarm"
@@ -509,15 +511,20 @@ module WarnPointerSubstraction =
let () = add_correctness_dep WarnPointerSubstraction.parameter
let () = Parameter_customize.set_group alarms
+let () = Parameter_customize.is_invisible ()
module IgnoreRecursiveCalls =
False
(struct
let option_name = "-eva-ignore-recursive-calls"
- let help =
- "Pretend function calls that would be recursive do not happen. \
- Causes unsoundness"
+ let help = "Deprecated."
end)
-let () = add_correctness_dep IgnoreRecursiveCalls.parameter
+let () =
+ IgnoreRecursiveCalls.add_set_hook
+ (fun _old _new ->
+ warning
+ "@[Option -eva-ignore-recursive-calls has no effect.@ Recursive calls \
+ can be unrolled@ through option -eva-unroll-recursive-calls,@ or their \
+ specification is used@ to interpret them.@]")
let () = Parameter_customize.set_group alarms
@@ -671,6 +678,19 @@ module WideningPeriod =
let () = WideningPeriod.set_range ~min:1 ~max:max_int
let () = add_precision_dep WideningPeriod.parameter
+let () = Parameter_customize.set_group precision_tuning
+module RecursiveUnroll =
+ Int
+ (struct
+ let default = 0
+ let option_name = "-eva-unroll-recursive-calls"
+ let arg_name = "n"
+ let help = "Unroll <n> recursive calls before using the specification of \
+ the recursive function to interpret the calls."
+ end)
+let () = RecursiveUnroll.set_range ~min:0 ~max:max_int
+let () = add_precision_dep RecursiveUnroll.parameter
+
(* --- Partitioning --- *)
let () = Parameter_customize.set_group precision_tuning
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 9a6a7172cc20cf89b2a178a6bf40c59cf1e91779..23ce27ed5dedf966bf1a5aeba9c6613aa60caea9 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -65,13 +65,13 @@ module WarnSignedConvertedDowncast: Parameter_sig.Bool
module WarnPointerSubstraction: Parameter_sig.Bool
module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set
-module IgnoreRecursiveCalls: Parameter_sig.Bool
-
module DescendingIteration: Parameter_sig.String
module HierarchicalConvergence: Parameter_sig.Bool
module WideningDelay: Parameter_sig.Int
module WideningPeriod: Parameter_sig.Int
+module RecursiveUnroll: Parameter_sig.Int
+
module SemanticUnrollingLevel: Parameter_sig.Int
module SlevelFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
@@ -218,6 +218,9 @@ val dkey_callbacks : category
(** Debug category used to print the usage of widenings. *)
val dkey_widening : category
+(** Debug category used to print messages about recursive calls. *)
+val dkey_recursion : category
+
(** Registers available cvalue builtins for the -eva-builtin option. *)
val register_builtin: string -> unit
diff --git a/src/plugins/value/values/abstract_location.mli b/src/plugins/value/values/abstract_location.mli
index df2247048bea90ea926809c6af7823d35c41f879..40419bfc573c0b96ea2682ac138d10deeea0386f 100644
--- a/src/plugins/value/values/abstract_location.mli
+++ b/src/plugins/value/values/abstract_location.mli
@@ -44,6 +44,10 @@ module type S = sig
val to_value : location -> value
val size : location -> Int_Base.t
+ (** [replace_base substitution location] replaces the variables represented
+ by the [location] according to [substitution]. *)
+ val replace_base: Base.substitution -> location -> location
+
(** {3 Alarms } *)
(** These functions are used to create the alarms that report undesirable
diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index 05e465434ffa50ad28ba262aeceb2c599fd111bc..50fb3525cae4491c7d1ad3800558923cc3c1066f 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -182,12 +182,18 @@ module type S = sig
dst_val: t ->
t option or_bottom
+ (** {3 Misc } *)
+
val resolve_functions : t -> Kernel_function.t list or_top * bool
(** [resolve_functions v] returns the list of functions that may be pointed to
by the abstract value [v] (representing a function pointer). The returned
boolean must be [true] if some of the values represented by [v] do not
correspond to functions. It is always safe to return [`Top, true]. *)
+ (** For pointer values, [replace_base substitution value] replaces the bases
+ pointed to by [value] according to [substitution]. For arithmetic values,
+ this function returns the [value] unchanged. *)
+ val replace_base: Base.substitution -> t -> t
end
type 'v key = 'v Structure.Key_Value.key
diff --git a/src/plugins/value/values/main_locations.ml b/src/plugins/value/values/main_locations.ml
index 7aab78471dfd377d2cd409d4313505a8bfee7363..7dd75133117b2ccb5902dc3afc4f1026b51ee176 100644
--- a/src/plugins/value/values/main_locations.ml
+++ b/src/plugins/value/values/main_locations.ml
@@ -62,6 +62,8 @@ module PLoc = struct
else `Unknown (l1, l2)
else `True
+ let replace_base = Precise_locs.replace_base
+
(* ------------------------------------------------------------------------ *)
(* Offsets *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/value/values/main_values.ml b/src/plugins/value/values/main_values.ml
index b21f868739e43063cf196d40e5aa1ebea5b3b811..b38d4fcaf3a3eb938642682fc965784ee137b0f2 100644
--- a/src/plugins/value/values/main_values.ml
+++ b/src/plugins/value/values/main_values.ml
@@ -132,6 +132,8 @@ module CVal = struct
let kfs, alarm = Locations.Location_Bytes.fold_topset_ok aux v init in
`Value kfs, alarm
with Abstract_interp.Error_Top -> `Top, true
+
+ let replace_base substitution t = snd (Cvalue.V.replace_base substitution t)
end
module Interval = struct
@@ -175,6 +177,7 @@ module Interval = struct
let forward_cast ~src_type:_ ~dst_type:_ _ = `Value top
let resolve_functions _ = `Top, true
+ let replace_base _substitution t = t
let rewrap_integer range value =
match value with
diff --git a/src/plugins/value/values/numerors/numerors_value.ml b/src/plugins/value/values/numerors/numerors_value.ml
index 2832d06cb3586316b5fe2fa311b2cb2f05e7a3ce..5381969a55fc736414ca52827754b99f6b22cd00 100644
--- a/src/plugins/value/values/numerors/numerors_value.ml
+++ b/src/plugins/value/values/numerors/numerors_value.ml
@@ -318,6 +318,7 @@ let assume_comparable _cmp v1 v2 = `Unknown (v1, v2)
let rewrap_integer _ _ = top
let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
let resolve_functions _ = `Top, true
+let replace_base _substitution t = t
(*-----------------------------------------------------------------------------
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index b46b11002e82269573247c93bebfb48e5e102bb7..f6fd8d3fd663c0c763a80f814b1d343015a6cabe 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -434,6 +434,11 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
else Top
let resolve_functions _ = `Top, true (* TODO: extract value *)
+ let replace_base substitution = function
+ | Top -> Top
+ | O offsm ->
+ let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
+ O (Cvalue.V_Offsetmap.map_on_values f offsm)
let forward_unop _typ op o =
let o' = match o, op with
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index b9f59f90e277c5ef875801640ea6f98d3987a801..08334941537bb65fd0931def46400ca033e12a12 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -107,6 +107,8 @@ let constant _ = function
precisely *)
let resolve_functions _ = `Top, true
+let replace_base _substitution t = t
+
(** {2 Alarms} *)
let assume_non_zero v =
diff --git a/src/plugins/value/values/value_product.ml b/src/plugins/value/values/value_product.ml
index 7e89f1fc751c739bdd1e262ae99ab1b6871f2136..03ec02d71f2b735936b3e84186198d8da1bf5cd9 100644
--- a/src/plugins/value/values/value_product.ml
+++ b/src/plugins/value/values/value_product.ml
@@ -125,6 +125,10 @@ module Make
in
list, b1 && b2
+ let replace_base substitution (left, right) =
+ Left.replace_base substitution left,
+ Right.replace_base substitution right
+
let reduce (orig_left, orig_right) left right = match left, right with
| None, None -> None
| Some left, None -> Some (left, orig_right)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index a545314edfe9d57bca80a5b37ab7d504a507f032..0fdd5f2fea59bd6a63b227433c8c022e8b681597 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -909,6 +909,10 @@ module V_Or_Uninitialized = struct
in
removed, t'
+ let replace_base substitution t =
+ let modified, v = V.replace_base substitution (get_v t) in
+ modified, if modified then create (get_flags t) v else t
+
let reduce_by_initializedness pos v =
if pos then
meet v (C_init_esc V.top)
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index a5c93243c0b2de1d3eeea18c3f4882e641652a3c..717c387372fd1c049d6809987a8ced77534c0271 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -226,6 +226,8 @@ module V_Or_Uninitialized : sig
val unspecify_escaping_locals :
exact:bool -> (V.M.key -> bool) -> t -> bool * t
+ val replace_base: Base.substitution -> t -> bool * t
+
val map: (V.t -> V.t) -> t -> t
val map2: (V.t -> V.t -> V.t) -> t -> t -> t
(** initialized/escaping information is the join of the information
diff --git a/src/plugins/value_types/precise_locs.ml b/src/plugins/value_types/precise_locs.ml
index 63faec349a5f9d1741de1363f98e5dee1ed6ab9d..905339d0fd2bde08242a5848f8285700b8fff543 100644
--- a/src/plugins/value_types/precise_locs.ml
+++ b/src/plugins/value_types/precise_locs.ml
@@ -263,6 +263,25 @@ let loc_top = {
}
let is_top_loc pl = equal_loc loc_top pl
+let replace_base substitution po =
+ match po.loc with
+ | PLBottom -> po
+ | PLLoc loc ->
+ let modified, loc = Location_Bits.replace_base substitution loc in
+ if modified then { po with loc = PLLoc loc } else po
+ | PLVarOffset (base, offset) ->
+ let set = Base.Hptset.singleton base in
+ let modified, set = Base.Hptset.replace substitution set in
+ if modified then
+ let base = Option.get (Base.Hptset.contains_single_elt set) in
+ { po with loc = PLVarOffset (base, offset) }
+ else po
+ | PLLocOffset (loc, offset) ->
+ let modified, loc = Location_Bits.replace_base substitution loc in
+ if modified
+ then { po with loc = PLLocOffset (loc, offset) }
+ else po
+
let rec fold_offset f po acc =
match po with
| POBottom -> f Ival.bottom acc
diff --git a/src/plugins/value_types/precise_locs.mli b/src/plugins/value_types/precise_locs.mli
index ba93233b11aecd14f15cb2d1cc2f355e6ee8d90a..cdff5d94de1b25b9f069419c0ba6c2424177f861 100644
--- a/src/plugins/value_types/precise_locs.mli
+++ b/src/plugins/value_types/precise_locs.mli
@@ -84,6 +84,8 @@ val is_bottom_loc: precise_location -> bool
val loc_top : precise_location
val is_top_loc: precise_location -> bool
+val replace_base: Base.substitution -> precise_location -> precise_location
+
val fold:
(Locations.location -> 'a -> 'a) -> precise_location -> 'a -> 'a
diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
index 9fcbfae2ed2afb6f4498cd8fc01efebb747ea53f..6b943ccd65a9ce9d811f61abbd5135a75d1d49d0 100644
--- a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
@@ -6,15 +6,12 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/defined/recursive.i:8: Warning:
- recursive call during value analysis
- of f (f <- f :: tests/defined/recursive.i:12 <- main). Assuming the call has
- no effect. The analysis will be unsound.
-[eva] using specification for function f
+[eva:recursion] tests/defined/recursive.i:8:
+ detected recursive call of function f.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
- __retres ∈ [--..--]
+ __retres ∈ {42}
[eva:final-states] Values at end of function main:
/* Generated by Frama-C */
diff --git a/src/plugins/variadic/tests/defined/recursive.i b/src/plugins/variadic/tests/defined/recursive.i
index 0757bce330528a5298ebf08e1358a169dcce5d91..35ce1f080d5b5dd8eb702afe9abb829a903d77ec 100644
--- a/src/plugins/variadic/tests/defined/recursive.i
+++ b/src/plugins/variadic/tests/defined/recursive.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-eva-ignore-recursive-calls"
+STDOPT: +"-eva-unroll-recursive-calls 10"
*/
int f(int a, ...){
if(a <= 0)
diff --git a/tests/misc/audit-in.json b/tests/misc/audit-in.json
index 4278dcffc0935c685a650032aba687e7f8ba817a..580f8ac0b0bf71f754b3f4a4b99a41655e8886e6 100644
--- a/tests/misc/audit-in.json
+++ b/tests/misc/audit-in.json
@@ -35,7 +35,6 @@
"-eva-context-depth": "2",
"-eva-context-valid-pointers": "false",
"-eva-context-width": "2",
- "-eva-ignore-recursive-calls": "false",
"-eva-initialization-padding-globals": "yes",
"-eva-initialized-locals": "false",
"-eva-new-initial-state": "0",
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index c12464699ba37e8bab645ecf123b3ca67f8bd9bd..b7d55c35d2b08c652da0b87c0ac9f06e6d2abe66 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -9,7 +9,6 @@
"-eva-context-depth": "2",
"-eva-context-valid-pointers": "false",
"-eva-context-width": "2",
- "-eva-ignore-recursive-calls": "false",
"-eva-initialization-padding-globals": "yes",
"-eva-initialized-locals": "false",
"-eva-new-initial-state": "0",
diff --git a/tests/value/oracle/rec.res.oracle b/tests/value/oracle/rec.res.oracle
deleted file mode 100644
index 1db02fb5692032ddfd08d1f0c71ac1781acb47ad..0000000000000000000000000000000000000000
--- a/tests/value/oracle/rec.res.oracle
+++ /dev/null
@@ -1,22 +0,0 @@
-[kernel] Parsing tests/value/rec.i (no 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
-
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
- X ∈ {0}
-[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 main:
- NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main:
- X
-[inout] Inputs for function main:
- \nothing
diff --git a/tests/value/oracle/recursion.0.res.oracle b/tests/value/oracle/recursion.0.res.oracle
index 11c074e5b372b9701116afdea0737dc70dd5e8d4..ce21d446188bb4c6d799e48dd493768b5edd735b 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -1,21 +1,632 @@
-[kernel] Parsing tests/value/recursion.i (no preprocessing)
-[eva] Analyzing an incomplete application starting at main
+[kernel] Parsing tests/value/recursion.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
- G ∈ [--..--]
+ nondet ∈ [--..--]
+ p ∈ {0}
+[eva:recursion] tests/value/recursion.c:18:
+ detected recursive call of function five.
+[eva] tests/value/recursion.c:18: Warning:
+ Using specification of function five for recursive calls.
+ Analysis of function five is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function five
+[eva:alarm] tests/value/recursion.c:15: Warning:
+ function five: postcondition got status unknown.
+[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
+[eva:recursion] tests/value/recursion.c:28:
+ detected recursive call of function sum.
+[eva] tests/value/recursion.c:28: Warning:
+ Using specification of function sum for recursive calls.
+ Analysis of function sum is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function sum
+[eva:alarm] tests/value/recursion.c:24: Warning:
+ function sum: postcondition got status unknown.
+[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:37:
+ detected recursive call of function factorial.
+[eva] tests/value/recursion.c:37: Warning:
+ Using specification of function factorial for recursive calls.
+ Analysis of function factorial is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function factorial
+[eva] tests/value/recursion.c:346: Frama_C_show_each_120: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:46:
+ detected recursive call of function syracuse.
+[eva] tests/value/recursion.c:46: Warning:
+ Using specification of function syracuse for recursive calls.
+ Analysis of function syracuse is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function syracuse
+[eva] tests/value/recursion.c:348: Frama_C_show_each_1: [0..4294967294]
+[eva:recursion] tests/value/recursion.c:59:
+ detected recursive call of function fibonacci.
+[eva] tests/value/recursion.c:59: Warning:
+ Using specification of function fibonacci for recursive calls.
+ Analysis of function fibonacci is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function fibonacci
+[eva:recursion] tests/value/recursion.c:60:
+ detected recursive call of function fibonacci.
+[eva] tests/value/recursion.c:60: Warning:
+ Using specification of function fibonacci for recursive calls.
+ Analysis of function fibonacci is thus incomplete and its soundness
+ relies on the written specification.
+[eva] tests/value/recursion.c:350: Frama_C_show_each_89: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:76:
+ detected recursive call of function sum_ptr.
+[eva] tests/value/recursion.c:76: Warning:
+ Using specification of function sum_ptr for recursive calls.
+ Analysis of function sum_ptr is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function sum_ptr
+[eva:alarm] tests/value/recursion.c:68: Warning:
+ function sum_ptr: postcondition got status unknown.
+[eva:alarm] tests/value/recursion.c:69: Warning:
+ function sum_ptr: postcondition got status unknown.
+[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:89:
+ detected recursive call of function factorial_ptr.
+[eva] tests/value/recursion.c:89: Warning:
+ Using specification of function factorial_ptr for recursive calls.
+ Analysis of function factorial_ptr is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function factorial_ptr
+[eva:alarm] tests/value/recursion.c:90: Warning:
+ accessing uninitialized left-value. assert \initialized(&res);
+[eva] tests/value/recursion.c:358: Frama_C_show_each_120: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:101:
+ detected recursive call of function syracuse_ptr.
+[eva] tests/value/recursion.c:101: Warning:
+ Using specification of function syracuse_ptr for recursive calls.
+ Analysis of function syracuse_ptr is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function syracuse_ptr
+[eva:alarm] tests/value/recursion.c:102: Warning:
+ accessing uninitialized left-value. assert \initialized(&prev_res);
+[eva] tests/value/recursion.c:361: Frama_C_show_each_1: [0..4294967294]
+[eva:recursion] tests/value/recursion.c:117:
+ detected recursive call of function fibonacci_ptr.
+[eva] tests/value/recursion.c:117: Warning:
+ Using specification of function fibonacci_ptr for recursive calls.
+ Analysis of function fibonacci_ptr is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function fibonacci_ptr
+[eva:recursion] tests/value/recursion.c:119:
+ detected recursive call of function fibonacci_ptr.
+[eva] tests/value/recursion.c:119: Warning:
+ Using specification of function fibonacci_ptr for recursive calls.
+ Analysis of function fibonacci_ptr is thus incomplete and its soundness
+ relies on the written specification.
+[eva:alarm] tests/value/recursion.c:120: Warning:
+ accessing uninitialized left-value. assert \initialized(&x);
+[eva:alarm] tests/value/recursion.c:120: Warning:
+ accessing uninitialized left-value. assert \initialized(&y);
+[eva] tests/value/recursion.c:364: Frama_C_show_each_89: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:137:
+ detected recursive call of function sum_and_fact.
+[eva] tests/value/recursion.c:137: Warning:
+ Using specification of function sum_and_fact for recursive calls.
+ Analysis of function sum_and_fact is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function sum_and_fact
+[eva:alarm] tests/value/recursion.c:128: Warning:
+ function sum_and_fact: postcondition got status unknown.
+[eva:alarm] tests/value/recursion.c:129: Warning:
+ function sum_and_fact: postcondition got status unknown.
+[eva] tests/value/recursion.c:368:
+ Frama_C_show_each_36_40320: {36}, [0..4294967288],0%8
+[eva:recursion] tests/value/recursion.c:161:
+ detected recursive call of function odd.
+[eva] tests/value/recursion.c:161: Warning:
+ Using specification of function odd for recursive calls.
+ Analysis of function odd is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function odd
+[eva:alarm] tests/value/recursion.c:149: Warning:
+ function odd: postcondition got status unknown.
+[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
+[eva:recursion] tests/value/recursion.c:183:
+ detected recursive call of function odd_ptr.
+[eva] tests/value/recursion.c:183: Warning:
+ Using specification of function odd_ptr for recursive calls.
+ Analysis of function odd_ptr is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function odd_ptr
+[eva:alarm] tests/value/recursion.c:167: Warning:
+ function odd_ptr: postcondition got status unknown.
+[eva:alarm] tests/value/recursion.c:184: Warning:
+ accessing uninitialized left-value. assert \initialized(&y);
+[eva:alarm] tests/value/recursion.c:179: Warning:
+ function even_ptr: postcondition got status unknown.
+[eva:recursion] tests/value/recursion.c:171:
+ detected recursive call of function even_ptr.
+[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
+[eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
+[eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [0..4294967295]
+[eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [0..4294967295]
+[eva:alarm] tests/value/recursion.c:222: Warning:
+ function fill_array: precondition got status invalid.
+[eva:alarm] tests/value/recursion.c:226: Warning:
+ function fill_array: precondition got status unknown.
+[eva:recursion] tests/value/recursion.c:200:
+ detected recursive call of function fill_array.
+[eva] tests/value/recursion.c:200: Warning:
+ Using specification of function fill_array for recursive calls.
+ Analysis of function fill_array is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function fill_array
+[eva:alarm] tests/value/recursion.c:200: Warning:
+ function fill_array: precondition got status unknown.
+[eva:alarm] tests/value/recursion.c:194: Warning:
+ function fill_array: postcondition got status unknown.
+[eva:alarm] tests/value/recursion.c:228: Warning:
+ function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
+[eva:recursion] tests/value/recursion.c:214:
+ detected recursive call of function binary_search.
+[eva] tests/value/recursion.c:214: Warning:
+ Using specification of function binary_search for recursive calls.
+ Analysis of function binary_search is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function binary_search
+[eva:recursion] tests/value/recursion.c:216:
+ detected recursive call of function binary_search.
+[eva] tests/value/recursion.c:216: Warning:
+ Using specification of function binary_search for recursive calls.
+ Analysis of function binary_search is thus incomplete and its soundness
+ relies on the written specification.
+[eva] tests/value/recursion.c:229:
+ Frama_C_show_each_3: [-2147483648..2147483647]
+[eva] tests/value/recursion.c:231:
+ Frama_C_show_each_12: [-2147483648..2147483647]
+[eva] tests/value/recursion.c:233:
+ Frama_C_show_each_minus1: [-2147483648..2147483647]
+[eva] tests/value/recursion.c:238:
+ Frama_C_show_each_7_11: [-2147483648..2147483647]
+[eva] tests/value/recursion.c:241:
+ Frama_C_show_each_minus_1_15: [-2147483648..2147483647]
+[eva:recursion] tests/value/recursion.c:252:
+ detected recursive call of function alarm.
+[eva] tests/value/recursion.c:252: Warning:
+ Using specification of function alarm for recursive calls.
+ Analysis of function alarm is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function alarm
+[eva:alarm] tests/value/recursion.c:247: Warning:
+ function alarm: postcondition got status unknown.
+[eva:alarm] tests/value/recursion.c:252: Warning:
+ signed overflow. assert i * tmp ≤ 2147483647;
+ (tmp from alarm(i - 1))
+[eva] tests/value/recursion.c:406:
+ Frama_C_show_each_unreachable: [20..2147483640],0%20
+[eva:recursion] tests/value/recursion.c:261:
+ detected recursive call of function precond.
+[eva] tests/value/recursion.c:261: Warning:
+ Using specification of function precond for recursive calls.
+ Analysis of function precond is thus incomplete and its soundness
+ relies on the written specification.
+[inout] Warning: no assigns clauses for function precond.
+ Results will be imprecise.
+[eva] using specification for function precond
+[eva] tests/value/recursion.c:261: Warning:
+ Cannot handle empty assigns clause. Assuming assigns \nothing: be aware this is probably incorrect.
+[eva:recursion] tests/value/recursion.c:276:
+ detected recursive call of function escaping_local.
+[eva] tests/value/recursion.c:276: Warning:
+ Using specification of function escaping_local for recursive calls.
+ Analysis of function escaping_local is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function escaping_local
+[eva:alarm] tests/value/recursion.c:278: Warning:
+ out of bounds write. assert \valid(p);
+[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {5}
+[eva:locals-escaping] tests/value/recursion.c:277: Warning:
+ locals {x} escaping the scope of a block of escaping_local through p
+[eva:recursion] tests/value/recursion.c:291:
+ detected recursive call of function escaping_formal.
+[eva] tests/value/recursion.c:291: Warning:
+ Using specification of function escaping_formal for recursive calls.
+ Analysis of function escaping_formal is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function escaping_formal
+[eva:alarm] tests/value/recursion.c:293: Warning:
+ out of bounds write. assert \valid(p);
+[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {5}
+[eva:locals-escaping] tests/value/recursion.c:411: Warning:
+ locals {x} escaping the scope of escaping_formal through p
+[eva:recursion] tests/value/recursion.c:307:
+ detected recursive call of function escaping_stack.
+[eva] tests/value/recursion.c:307: Warning:
+ Using specification of function escaping_stack for recursive calls.
+ Analysis of function escaping_stack is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function escaping_stack
+[eva:alarm] tests/value/recursion.c:309: Warning:
+ out of bounds write. assert \valid(p);
+[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {5}
+[eva:locals-escaping] tests/value/recursion.c:308: Warning:
+ locals {x} escaping the scope of a block of escaping_stack through p
+[eva:recursion] tests/value/recursion.c:323:
+ detected recursive call of function decr.
+[eva] tests/value/recursion.c:323: Warning:
+ Using specification of function decr for recursive calls.
+ Analysis of function decr is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function decr
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function alarm:
+ res ∈ [10..2147483647]
+ __retres ∈ [10..2147483647]
+[eva:final-states] Values at end of function decr:
+
+[eva:final-states] Values at end of function bug_memexec:
+
+[eva:final-states] Values at end of function escaping_formal:
+ p ∈ {{ NULL + [--..--] ; &x }}
x ∈ [--..--]
- c ∈ [--..--]
- s ∈ [--..--]
- pg ∈ {{ NULL ; &S_pg[0] }}
- S_pg[0..1] ∈ [--..--]
-[eva] computing for function ff <- main.
- Called from tests/value/recursion.i:68.
-[eva] tests/value/recursion.i:9: User Error:
- detected recursive call (ff <- ff :: tests/value/recursion.i:68 <- main)
- Use -eva-ignore-recursive-calls to ignore (beware this will make the analysis
- unsound)
-[eva] User Error: Degeneration occurred:
- results are not correct for lines of code that can be reached from the degeneration point.
-[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Plug-in eva aborted: invalid user input.
+[eva:final-states] Values at end of function escaping_local:
+ p ∈ [--..--] or ESCAPINGADDR
+[eva:final-states] Values at end of function escaping_stack:
+ p ∈
+ {{ garbled mix of &{a}
+ (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
+ a ∈ [--..--]
+[eva:final-states] Values at end of function even:
+ __retres ∈ UNINITIALIZED
+ __retres ∈ {0; 1}
+[eva:final-states] Values at end of function even_ptr:
+ x ∈ [--..--]
+ b ∈ {0; 1}
+[eva:final-states] Values at end of function factorial:
+ res ∈ [--..--]
+ __retres ∈ [--..--]
+[eva:final-states] Values at end of function factorial_ptr:
+ y ∈ [--..--]
+[eva:final-states] Values at end of function fill_array:
+ array[0] ∈ {0}
+ [1..10] ∈ [--..--]
+ [11..15] ∈ [--..--] or UNINITIALIZED
+[eva:final-states] Values at end of function five:
+ __retres ∈ {5}
+[eva:final-states] Values at end of function odd:
+ __retres ∈ {0; 1}
+ __retres ∈ UNINITIALIZED
+[eva:final-states] Values at end of function odd_ptr:
+ y ∈ [--..--]
+ a ∈ [--..--]
+[eva:final-states] Values at end of function precond:
+Cannot filter: dumping raw memory (including unchanged variables)
+ Frama_C_entropy_source ∈ [--..--]
+ nondet ∈ [--..--]
+ x ∈ {1}
+ y ∈ {-6}
+ p ∈ {0}
+ a ∈ {0}
+ b ∈ {0}
+ x ∈ [10..20]
+ y ∈ [10..2147483647]
+ tmp ∈ [3..11]
+ tmp_0 ∈ [10..20]
+ tmp_1 ∈ [10..2147483647]
+[eva:final-states] Values at end of function sum:
+ res ∈ [6..91]
+ __retres ∈ [6..91]
+[eva:final-states] Values at end of function sum_and_fact:
+ x ∈ {36}
+ __retres ∈ [0..4294967288],0%8
+[eva:final-states] Values at end of function sum_ptr:
+ y ∈ [6..91]
+[eva:final-states] Values at end of function syracuse:
+ __retres ∈ [0..4294967294]
+[eva:final-states] Values at end of function syracuse_ptr:
+ y ∈ [0..4294967294]
+[eva:final-states] Values at end of function binary_search:
+ mid ∈ {7}
+ __retres ∈ [--..--]
+[eva:final-states] Values at end of function fibonacci:
+ __retres ∈ [--..--]
+[eva:final-states] Values at end of function fibonacci_ptr:
+ y ∈ [--..--]
+[eva:final-states] Values at end of function test_array:
+ Frama_C_entropy_source ∈ [--..--]
+ array[0] ∈ {0}
+ [1..9] ∈ [--..--]
+ [10] ∈ {10}
+ [11..15] ∈ [--..--]
+ i ∈ [--..--]
+ j ∈ [7..18]
+ end ∈ {10; 11; 12; 13; 14; 15; 16}
+[eva:final-states] Values at end of function main:
+Cannot filter: dumping raw memory (including unchanged variables)
+ Frama_C_entropy_source ∈ [--..--]
+ nondet ∈ [--..--]
+ p ∈
+ {{ garbled mix of &{a}
+ (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
+ a ∈ [--..--]
+ b ∈ {0}
+ x ∈ [10..20]
+ y ∈ [10..2147483647]
+ tmp ∈ [3..11]
+ tmp_0 ∈ [10..20]
+ tmp_1 ∈ [10..2147483647]
+[from] Computing for function alarm
+[from] Computing for function alarm <-alarm
+[from] Done for function alarm
+[from] Done for function alarm
+[from] Computing for function decr
+[from] Computing for function decr <-decr
+[from] Done for function decr
+[from] Done for function decr
+[from] Computing for function bug_memexec
+[from] Done for function bug_memexec
+[from] Computing for function escaping_formal
+[from] Computing for function escaping_formal <-escaping_formal
+[from] Done for function escaping_formal
+[from] Done for function escaping_formal
+[from] Computing for function escaping_local
+[from] Computing for function escaping_local <-escaping_local
+[from] Done for function escaping_local
+[from] Done for function escaping_local
+[from] Computing for function escaping_stack
+[from] Computing for function escaping_stack <-escaping_stack
+[from] Done for function escaping_stack
+[from] Done for function escaping_stack
+[from] Computing for function even
+[from] Computing for function odd <-even
+[from] Computing for function even <-odd <-even
+[from] Done for function even
+[from] Done for function odd
+[from] Done for function even
+[from] Computing for function even_ptr
+[from] Computing for function odd_ptr <-even_ptr
+[from] Computing for function even_ptr <-odd_ptr <-even_ptr
+[from] Done for function even_ptr
+[from] Done for function odd_ptr
+[from] Done for function even_ptr
+[from] Computing for function factorial
+[from] Computing for function factorial <-factorial
+[from] Done for function factorial
+[from] Done for function factorial
+[from] Computing for function factorial_ptr
+[from] Computing for function factorial_ptr <-factorial_ptr
+[from] Done for function factorial_ptr
+[from] Done for function factorial_ptr
+[from] Computing for function fill_array
+[from] Computing for function fill_array <-fill_array
+[from] Done for function fill_array
+[from] Done for function fill_array
+[from] Computing for function five
+[from] Computing for function five <-five
+[from] Done for function five
+[from] Done for function five
+[from] Computing for function precond
+[from] Computing for function precond <-precond
+[from] Done for function precond
+[from] Done for function precond
+[from] Computing for function sum
+[from] Computing for function sum <-sum
+[from] Done for function sum
+[from] Done for function sum
+[from] Computing for function sum_and_fact
+[from] Computing for function sum_and_fact <-sum_and_fact
+[from] Done for function sum_and_fact
+[from] Done for function sum_and_fact
+[from] Computing for function sum_ptr
+[from] Computing for function sum_ptr <-sum_ptr
+[from] Done for function sum_ptr
+[from] Done for function sum_ptr
+[from] Computing for function syracuse
+[from] Computing for function syracuse <-syracuse
+[from] Done for function syracuse
+[from] Done for function syracuse
+[from] Computing for function syracuse_ptr
+[from] Computing for function syracuse_ptr <-syracuse_ptr
+[from] Done for function syracuse_ptr
+[from] Done for function syracuse_ptr
+[from] Computing for function binary_search
+[from] Computing for function binary_search <-binary_search
+[from] Done for function binary_search
+[from] Done for function binary_search
+[from] Computing for function fibonacci
+[from] Computing for function fibonacci <-fibonacci
+[from] Done for function fibonacci
+[from] Done for function fibonacci
+[from] Computing for function fibonacci_ptr
+[from] Computing for function fibonacci_ptr <-fibonacci_ptr
+[from] Done for function fibonacci_ptr
+[from] Done for function fibonacci_ptr
+[from] Computing for function test_array
+[from] Computing for function Frama_C_interval <-test_array
+[from] Done for function Frama_C_interval
+[from] Done for function test_array
+[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 alarm:
+ res FROM i
+ tmp FROM i
+ __retres FROM i
+ \result FROM i
+[from] Function decr:
+ NO EFFECTS
+[from] Function bug_memexec:
+ NO EFFECTS
+[from] Function escaping_formal:
+ p FROM count
+ x FROM nondet; count (and SELF)
+[from] Function escaping_local:
+ p FROM count
+[from] Function escaping_stack:
+ p FROM count; q
+ a FROM nondet; count; q (and SELF)
+[from] Function even:
+ __retres FROM n
+ __retres FROM n
+ \result FROM n
+[from] Function even_ptr:
+ x FROM n; result (and SELF)
+ a FROM n (and SELF)
+ b FROM n; result (and SELF)
+[from] Function factorial:
+ res FROM i
+ tmp FROM i
+ __retres FROM i
+ \result FROM i
+[from] Function factorial_ptr:
+ y FROM p_0; result; x
+[from] Function fill_array:
+ array{[0]; [10]} FROM data; start; end (and SELF)
+[from] Function five:
+ __retres FROM nondet
+ \result FROM nondet
+[from] Function odd:
+ __retres FROM n
+ \result FROM n
+[from] Function odd_ptr:
+ y FROM n; result (and SELF)
+ a FROM n; result (and SELF)
+[from] Function precond:
+ y FROM x
+[from] Function sum:
+ res FROM i
+ tmp FROM i
+ __retres FROM i
+ \result FROM i
+[from] Function sum_and_fact:
+ x FROM i; sum_0
+ __retres FROM i
+ \result FROM i
+[from] Function sum_ptr:
+ y FROM p_0; result; x
+[from] Function syracuse:
+ __retres FROM i
+ \result FROM i
+[from] Function syracuse_ptr:
+ y FROM p_0; result; x
+[from] Function binary_search:
+ mid FROM start; end
+ __retres FROM data; toFind; start; end; array[7]
+ \result FROM data; toFind; start; end; array[7]
+[from] Function fibonacci:
+ __retres FROM n
+ \result FROM n
+[from] Function fibonacci_ptr:
+ y FROM p_0; result; x
+[from] Function test_array:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ p FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function alarm:
+ res; tmp; __retres
+[inout] Inputs for function alarm:
+ i; res; tmp; __retres
+[inout] Out (internal) for function decr:
+ x
+[inout] Inputs for function decr:
+ nondet; i
+[inout] Out (internal) for function bug_memexec:
+ \nothing
+[inout] Inputs for function bug_memexec:
+ nondet
+[inout] Out (internal) for function escaping_formal:
+ p; x
+[inout] Inputs for function escaping_formal:
+ nondet; p; count; x
+[inout] Out (internal) for function escaping_local:
+ p; x
+[inout] Inputs for function escaping_local:
+ nondet; p; count
+[inout] Out (internal) for function escaping_stack:
+ p; x; a
+[inout] Inputs for function escaping_stack:
+ nondet; p; count; q
+[inout] Out (internal) for function even:
+ tmp; tmp; __retres; __retres
+[inout] Inputs for function even:
+ n; tmp; n; tmp; __retres; __retres
+[inout] Out (internal) for function even_ptr:
+ x; y; b
+[inout] Inputs for function even_ptr:
+ n; result; x; n; result; y
+[inout] Out (internal) for function factorial:
+ res; tmp; __retres
+[inout] Inputs for function factorial:
+ i; res; tmp; __retres
+[inout] Out (internal) for function factorial_ptr:
+ arg; y
+[inout] Inputs for function factorial_ptr:
+ p_0; result; res; x
+[inout] Out (internal) for function fill_array:
+ array[0..15]
+[inout] Inputs for function fill_array:
+ data; start; end
+[inout] Out (internal) for function five:
+ tmp; __retres
+[inout] Inputs for function five:
+ nondet; tmp; __retres
+[inout] Out (internal) for function odd:
+ tmp; tmp; __retres; __retres
+[inout] Inputs for function odd:
+ n; tmp; n; tmp; __retres; __retres
+[inout] Out (internal) for function odd_ptr:
+ x; y; a
+[inout] Inputs for function odd_ptr:
+ n; result; x; n; result; y
+[inout] Out (internal) for function precond:
+ ANYTHING(origin:Unknown)
+[inout] Inputs for function precond:
+ nondet; x
+[inout] Out (internal) for function sum:
+ res; tmp; __retres
+[inout] Inputs for function sum:
+ i; res; tmp; __retres
+[inout] Out (internal) for function sum_and_fact:
+ fact; tmp_0; x; __retres
+[inout] Inputs for function sum_and_fact:
+ i; sum_0; tmp; fact; tmp_0; __retres
+[inout] Out (internal) for function sum_ptr:
+ arg; y
+[inout] Inputs for function sum_ptr:
+ p_0; result; res; x
+[inout] Out (internal) for function syracuse:
+ prev; __retres
+[inout] Inputs for function syracuse:
+ n; i; prev; __retres
+[inout] Out (internal) for function syracuse_ptr:
+ prev_arg; y
+[inout] Inputs for function syracuse_ptr:
+ n; p_0; result; prev_res; x
+[inout] Out (internal) for function binary_search:
+ mid; tmp; tmp_0; __retres
+[inout] Inputs for function binary_search:
+ data; toFind; start; end; mid; tmp; tmp_0; array[7]; __retres
+[inout] Out (internal) for function fibonacci:
+ x; y; __retres
+[inout] Inputs for function fibonacci:
+ n; x; y; __retres
+[inout] Out (internal) for function fibonacci_ptr:
+ a; y
+[inout] Inputs for function fibonacci_ptr:
+ p_0; result; x; y; a; x
+[inout] Out (internal) for function test_array:
+ Frama_C_entropy_source; array[0..15]; i; j; end
+[inout] Inputs for function test_array:
+ Frama_C_entropy_source; nondet
+[inout] Out (internal) for function main:
+ ANYTHING(origin:Unknown)
+[inout] Inputs for function main:
+ Frama_C_entropy_source; nondet; p
diff --git a/tests/value/oracle/recursion.1.res.oracle b/tests/value/oracle/recursion.1.res.oracle
index 4738d12e1cca4cee88dc7dad81f2718b31e1b7ea..5fd6d46ceb18ba3e3efda9e41353d2e7da7de780 100644
--- a/tests/value/oracle/recursion.1.res.oracle
+++ b/tests/value/oracle/recursion.1.res.oracle
@@ -1,110 +1,514 @@
-[kernel] Parsing tests/value/recursion.i (no preprocessing)
-[eva] Analyzing an incomplete application starting at main
+[kernel] Parsing tests/value/recursion.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
- G ∈ [--..--]
- x ∈ [--..--]
- c ∈ [--..--]
- s ∈ [--..--]
- pg ∈ {{ NULL ; &S_pg[0] }}
- S_pg[0..1] ∈ [--..--]
-[eva] computing for function ff <- main.
- Called from tests/value/recursion.i:68.
-[eva] tests/value/recursion.i:9: Warning:
- recursive call during value analysis
- of ff (ff <- ff :: tests/value/recursion.i:68 <- main). Assuming the call has
- no effect. The analysis will be unsound.
-[eva] computing for function ff <- ff <- main.
- Called from tests/value/recursion.i:9.
-[eva] using specification for function ff
-[eva] Done for function ff
-[eva] Recording results for ff
-[eva] Done for function ff
-[eva] computing for function g <- main.
- Called from tests/value/recursion.i:69.
-[eva] tests/value/recursion.i:40: Warning:
- recursive call during value analysis
- of g (g <- g :: tests/value/recursion.i:69 <- main). Assuming the call has
- no effect. The analysis will be unsound.
-[eva] computing for function g <- g <- main.
- Called from tests/value/recursion.i:40.
-[eva] using specification for function g
-[eva] Done for function g
-[eva] Recording results for g
-[eva] Done for function g
-[eva] computing for function h <- main.
- Called from tests/value/recursion.i:71.
-[eva] tests/value/recursion.i:45: Warning:
- recursive call during value analysis
- of h (h <- h :: tests/value/recursion.i:71 <- main). Assuming the call has
- no effect. The analysis will be unsound.
-[eva] computing for function h <- h <- main.
- Called from tests/value/recursion.i:45.
-[eva] using specification for function h
-[eva] Done for function h
-[eva] Recording results for h
-[eva] Done for function h
-[eva] tests/value/recursion.i:72: Frama_C_show_each: Bottom, Bottom
-[eva] computing for function escaping_formal <- main.
- Called from tests/value/recursion.i:73.
-[eva] tests/value/recursion.i:73:
- function escaping_formal: precondition got status valid.
-[eva] tests/value/recursion.i:59: Frama_C_show_each: {{ &i }}, {10}, {0}, {10}
-[eva] tests/value/recursion.i:60: Warning:
- recursive call during value analysis
- of escaping_formal (escaping_formal <- escaping_formal :: tests/value/recursion.i:73 <-
- main).
- Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/value/recursion.i:60: User Error:
- function 'escaping_formal' (involved in a recursive call) has a formal parameter whose address is taken. Analysis may be unsound.
-[eva] computing for function escaping_formal <- escaping_formal <- main.
- Called from tests/value/recursion.i:60.
-[eva] using specification for function escaping_formal
-[eva] Done for function escaping_formal
-[eva] tests/value/recursion.i:63: Frama_C_show_each: {{ &i }}, {10}, {0}, {10}
-[eva] tests/value/recursion.i:55:
- function escaping_formal: postcondition got status valid.
-[eva] Recording results for escaping_formal
-[eva] Done for function escaping_formal
-[eva] computing for function f <- main.
- Called from tests/value/recursion.i:74.
-[eva] tests/value/recursion.i:29: Frama_C_show_each: {2}, {0}
-[eva] tests/value/recursion.i:31: Warning:
- recursive call during value analysis
- of f (f <- f :: tests/value/recursion.i:74 <- main). Assuming the call has
- no effect. The analysis will be unsound.
-[eva] computing for function f <- f <- main.
- Called from tests/value/recursion.i:31.
-[eva] using specification for function f
-[eva] Done for function f
-[eva] tests/value/recursion.i:32: Frama_C_show_each: {2}, {0}
-[eva] Recording results for f
-[eva] Done for function f
-[eva] tests/value/recursion.i:75: Frama_C_show_each: {2}
-[eva:alarm] tests/value/recursion.i:76: Warning:
- signed overflow. assert r.f1 + 1 ≤ 2147483647;
-[eva] Recording results for main
+ nondet ∈ [--..--]
+ p ∈ {0}
+[eva:recursion] tests/value/recursion.c:18:
+ detected recursive call of function five.
+[eva] tests/value/recursion.c:18: Warning:
+ Using specification of function five for recursive calls of depth 20.
+ Analysis of function five is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function five
+[eva:alarm] tests/value/recursion.c:15: Warning:
+ function five: postcondition got status unknown.
+[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
+[eva:recursion] tests/value/recursion.c:28:
+ detected recursive call of function sum.
+[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:37:
+ detected recursive call of function factorial.
+[eva] tests/value/recursion.c:346: Frama_C_show_each_120: {120}
+[eva:recursion] tests/value/recursion.c:46:
+ detected recursive call of function syracuse.
+[eva] tests/value/recursion.c:348: Frama_C_show_each_1: {1}
+[eva:recursion] tests/value/recursion.c:59:
+ detected recursive call of function fibonacci.
+[eva:recursion] tests/value/recursion.c:60:
+ detected recursive call of function fibonacci.
+[eva] tests/value/recursion.c:350: Frama_C_show_each_89: {89}
+[eva:recursion] tests/value/recursion.c:76:
+ detected recursive call of function sum_ptr.
+[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:89:
+ detected recursive call of function factorial_ptr.
+[eva] tests/value/recursion.c:358: Frama_C_show_each_120: {120}
+[eva:recursion] tests/value/recursion.c:101:
+ detected recursive call of function syracuse_ptr.
+[eva] tests/value/recursion.c:361: Frama_C_show_each_1: {1}
+[eva:recursion] tests/value/recursion.c:117:
+ detected recursive call of function fibonacci_ptr.
+[eva:recursion] tests/value/recursion.c:119:
+ detected recursive call of function fibonacci_ptr.
+[eva] tests/value/recursion.c:364: Frama_C_show_each_89: {89}
+[eva:recursion] tests/value/recursion.c:137:
+ detected recursive call of function sum_and_fact.
+[eva] tests/value/recursion.c:368: Frama_C_show_each_36_40320: {36}, {40320}
+[eva:recursion] tests/value/recursion.c:161:
+ detected recursive call of function odd.
+[eva:recursion] tests/value/recursion.c:152:
+ detected recursive call of function even.
+[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
+[eva:recursion] tests/value/recursion.c:183:
+ detected recursive call of function odd_ptr.
+[eva:recursion] tests/value/recursion.c:171:
+ detected recursive call of function even_ptr.
+[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
+[eva] using specification for function Frama_C_interval
+[eva:alarm] tests/value/recursion.c:24: Warning:
+ function sum: postcondition got status unknown.
+[eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
+[eva:alarm] tests/value/recursion.c:69: Warning:
+ function sum_ptr: postcondition got status unknown.
+[eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
+[eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [2..89]
+[eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [2..89]
+[eva:alarm] tests/value/recursion.c:222: Warning:
+ function fill_array: precondition got status invalid.
+[eva:alarm] tests/value/recursion.c:226: Warning:
+ function fill_array: precondition got status unknown.
+[eva:recursion] tests/value/recursion.c:200:
+ detected recursive call of function fill_array.
+[eva:alarm] tests/value/recursion.c:200: Warning:
+ function fill_array: precondition got status unknown.
+[eva:alarm] tests/value/recursion.c:199: Warning:
+ out of bounds write. assert \valid(data + start);
+[kernel] tests/value/recursion.c:199: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/value/recursion.c:194: Warning:
+ function fill_array: postcondition got status unknown.
+[eva:alarm] tests/value/recursion.c:228: Warning:
+ function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
+[eva:recursion] tests/value/recursion.c:214:
+ detected recursive call of function binary_search.
+[eva] tests/value/recursion.c:229: Frama_C_show_each_3: {3}
+[eva:recursion] tests/value/recursion.c:216:
+ detected recursive call of function binary_search.
+[eva] tests/value/recursion.c:231: Frama_C_show_each_12: {12}
+[eva] tests/value/recursion.c:233: Frama_C_show_each_minus1: {-1}
+[eva] tests/value/recursion.c:238: Frama_C_show_each_7_11: {7; 8; 9; 10; 11}
+[eva] tests/value/recursion.c:241: Frama_C_show_each_minus_1_15: [-1..15]
+[eva:recursion] tests/value/recursion.c:252:
+ detected recursive call of function alarm.
+[eva:alarm] tests/value/recursion.c:252: Warning:
+ signed overflow. assert i * tmp ≤ 2147483647;
+ (tmp from alarm(i - 1))
+[eva:recursion] tests/value/recursion.c:261:
+ detected recursive call of function precond.
+[eva:alarm] tests/value/recursion.c:261: Warning:
+ function precond: precondition got status invalid.
+[eva:recursion] tests/value/recursion.c:276:
+ detected recursive call of function escaping_local.
+[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {1}
+[eva:locals-escaping] tests/value/recursion.c:277: Warning:
+ locals {x} escaping the scope of a block of escaping_local through p
+[eva:alarm] tests/value/recursion.c:278: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+[kernel] tests/value/recursion.c:278: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:recursion] tests/value/recursion.c:291:
+ detected recursive call of function escaping_formal.
+[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {1}
+[eva:locals-escaping] tests/value/recursion.c:291: Warning:
+ locals {x} escaping the scope of escaping_formal through p
+[eva:alarm] tests/value/recursion.c:293: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+[kernel] tests/value/recursion.c:293: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:recursion] tests/value/recursion.c:307:
+ detected recursive call of function escaping_stack.
+[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {1}
+[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {2}
+[eva:locals-escaping] tests/value/recursion.c:308: Warning:
+ locals {x} escaping the scope of a block of escaping_stack through p
+[eva:alarm] tests/value/recursion.c:309: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+[kernel] tests/value/recursion.c:309: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:recursion] tests/value/recursion.c:323:
+ detected recursive call of function decr.
+[eva] tests/value/recursion.c:323: Warning:
+ Using specification of function decr for recursive calls of depth 20.
+ Analysis of function decr is thus incomplete and its soundness
+ relies on the written specification.
+[eva] using specification for function decr
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function escaping_formal:
- pg ∈ {0}
-[eva:final-states] Values at end of function f:
- x ∈ {2}
- s ∈ [--..--]
-[eva:final-states] Values at end of function ff:
- __retres ∈ {5}
-[eva:final-states] Values at end of function g:
+[eva:final-states] Values at end of function alarm:
+ res ∈ [2..2147483647]
+ __retres ∈ [1..2147483647]
+[eva:final-states] Values at end of function decr:
-[eva:final-states] Values at end of function h:
+[eva:final-states] Values at end of function bug_memexec:
+[eva:final-states] Values at end of function escaping_formal:
+ p ∈ {{ &x ; &\copy<x>[5] }} or ESCAPINGADDR
+ x ∈ {5; 16}
+[eva:final-states] Values at end of function escaping_local:
+ p ∈ {{ &\copy<x>[5] }} or ESCAPINGADDR
+[eva:final-states] Values at end of function escaping_stack:
+ p ∈ {{ &\copy<x>[4] }} or ESCAPINGADDR
+[eva:final-states] Values at end of function even:
+ __retres ∈ UNINITIALIZED
+ __retres ∈ {0; 1}
+[eva:final-states] Values at end of function even_ptr:
+ x ∈ {0; 1}
+ b ∈ {0; 1}
+[eva:final-states] Values at end of function factorial:
+ res ∈ {2; 6; 24; 120}
+ __retres ∈ {1; 2; 6; 24; 120}
+[eva:final-states] Values at end of function factorial_ptr:
+ y ∈ {91; 120}
+[eva:final-states] Values at end of function fill_array:
+ array[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {3}
+ [4] ∈ {4}
+ [5] ∈ {5}
+ [6] ∈ {6}
+ [7] ∈ {7}
+ [8] ∈ {8}
+ [9] ∈ {9}
+ [10] ∈ {10}
+ [11] ∈ {11} or UNINITIALIZED
+ [12] ∈ {12} or UNINITIALIZED
+ [13] ∈ {13} or UNINITIALIZED
+ [14] ∈ {14} or UNINITIALIZED
+ [15] ∈ {15} or UNINITIALIZED
+[eva:final-states] Values at end of function five:
+ __retres ∈ {5}
+[eva:final-states] Values at end of function odd:
+ __retres ∈ {0; 1}
+ __retres ∈ UNINITIALIZED
+[eva:final-states] Values at end of function odd_ptr:
+ y ∈ {0; 1}
+ a ∈ {0; 1}
+[eva:final-states] Values at end of function precond:
+ y ∈ [-100..-6]
+[eva:final-states] Values at end of function sum:
+ res ∈ [3..91]
+ __retres ∈ [1..91]
+[eva:final-states] Values at end of function sum_and_fact:
+ x ∈ {11; 36}
+ __retres ∈ {1; 2; 6; 24; 120; 720; 5040; 40320}
+[eva:final-states] Values at end of function sum_ptr:
+ y ∈ [0..91]
+[eva:final-states] Values at end of function syracuse:
+ __retres ∈ [1..16]
+[eva:final-states] Values at end of function syracuse_ptr:
+ y ∈ {1; 120}
+[eva:final-states] Values at end of function binary_search:
+ mid ∈ [3..16]
+ __retres ∈ [-1..15]
+[eva:final-states] Values at end of function fibonacci:
+ __retres ∈ [0..89]
+[eva:final-states] Values at end of function fibonacci_ptr:
+ y ∈ [0..89]
+[eva:final-states] Values at end of function test_array:
+ Frama_C_entropy_source ∈ [--..--]
+ array[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {3}
+ [4] ∈ {4}
+ [5] ∈ {5}
+ [6] ∈ {6}
+ [7] ∈ {7}
+ [8] ∈ {8}
+ [9] ∈ {9}
+ [10] ∈ {10}
+ [11] ∈ {11}
+ [12] ∈ {12}
+ [13] ∈ {13}
+ [14] ∈ {14}
+ [15] ∈ {15}
+ i ∈ [-1..15]
+ j ∈ [7..18]
+ end ∈ {10; 11; 12; 13; 14; 15}
[eva:final-states] Values at end of function main:
- G ∈ {5}
- x ∈ {2}
- s ∈ [--..--]
- pg ∈ {0}
- r.f1 ∈ [-2147483648..2147483646]
- .f2 ∈ [--..--]
- __retres ∈ [-2147483647..2147483647]
-[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Plug-in eva aborted: invalid user input.
+ Frama_C_entropy_source ∈ [--..--]
+ p ∈ ESCAPINGADDR
+ a ∈ {0}
+ b ∈ {0}
+ x ∈ [10..20]
+ y ∈ [3628800..2147483647]
+[from] Computing for function alarm
+[from] Computing for function alarm <-alarm
+[from] Done for function alarm
+[from] Done for function alarm
+[from] Computing for function decr
+[from] Computing for function decr <-decr
+[from] Done for function decr
+[from] Done for function decr
+[from] Computing for function bug_memexec
+[from] Done for function bug_memexec
+[from] Computing for function escaping_formal
+[from] Computing for function escaping_formal <-escaping_formal
+[from] Done for function escaping_formal
+[from] Done for function escaping_formal
+[from] Computing for function escaping_local
+[from] Computing for function escaping_local <-escaping_local
+[from] Done for function escaping_local
+[from] Done for function escaping_local
+[from] Computing for function escaping_stack
+[from] Computing for function escaping_stack <-escaping_stack
+[from] Done for function escaping_stack
+[from] Done for function escaping_stack
+[from] Computing for function even
+[from] Computing for function odd <-even
+[from] Computing for function even <-odd <-even
+[from] Done for function even
+[from] Done for function odd
+[from] Done for function even
+[from] Computing for function even_ptr
+[from] Computing for function odd_ptr <-even_ptr
+[from] Computing for function even_ptr <-odd_ptr <-even_ptr
+[from] Done for function even_ptr
+[from] Done for function odd_ptr
+[from] Done for function even_ptr
+[from] Computing for function factorial
+[from] Computing for function factorial <-factorial
+[from] Done for function factorial
+[from] Done for function factorial
+[from] Computing for function factorial_ptr
+[from] Computing for function factorial_ptr <-factorial_ptr
+[from] Done for function factorial_ptr
+[from] Done for function factorial_ptr
+[from] Computing for function fill_array
+[from] Computing for function fill_array <-fill_array
+[from] Done for function fill_array
+[from] Done for function fill_array
+[from] Computing for function five
+[from] Computing for function five <-five
+[from] Done for function five
+[from] Done for function five
+[from] Computing for function precond
+[from] Computing for function precond <-precond
+[from] Done for function precond
+[from] Done for function precond
+[from] Computing for function sum
+[from] Computing for function sum <-sum
+[from] Done for function sum
+[from] Done for function sum
+[from] Computing for function sum_and_fact
+[from] Computing for function sum_and_fact <-sum_and_fact
+[from] Done for function sum_and_fact
+[from] Done for function sum_and_fact
+[from] Computing for function sum_ptr
+[from] Computing for function sum_ptr <-sum_ptr
+[from] Done for function sum_ptr
+[from] Done for function sum_ptr
+[from] Computing for function syracuse
+[from] Computing for function syracuse <-syracuse
+[from] Done for function syracuse
+[from] Done for function syracuse
+[from] Computing for function syracuse_ptr
+[from] Computing for function syracuse_ptr <-syracuse_ptr
+[from] Done for function syracuse_ptr
+[from] Done for function syracuse_ptr
+[from] Computing for function binary_search
+[from] Computing for function binary_search <-binary_search
+[from] Done for function binary_search
+[from] Done for function binary_search
+[from] Computing for function fibonacci
+[from] Computing for function fibonacci <-fibonacci
+[from] Done for function fibonacci
+[from] Done for function fibonacci
+[from] Computing for function fibonacci_ptr
+[from] Computing for function fibonacci_ptr <-fibonacci_ptr
+[from] Done for function fibonacci_ptr
+[from] Done for function fibonacci_ptr
+[from] Computing for function test_array
+[from] Computing for function Frama_C_interval <-test_array
+[from] Done for function Frama_C_interval
+[from] Done for function test_array
+[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 alarm:
+ res FROM i
+ tmp FROM i
+ __retres FROM i
+ \result FROM i
+[from] Function decr:
+ NO EFFECTS
+[from] Function bug_memexec:
+ NO EFFECTS
+[from] Function escaping_formal:
+ p FROM count (and SELF)
+ x FROM nondet; count (and SELF)
+[from] Function escaping_local:
+ p FROM count (and SELF)
+[from] Function escaping_stack:
+ p FROM count; q (and SELF)
+[from] Function even:
+ __retres FROM n (and SELF)
+ __retres FROM n
+ \result FROM n
+[from] Function even_ptr:
+ x FROM n; result (and SELF)
+ a FROM n (and SELF)
+ b FROM n; result (and SELF)
+[from] Function factorial:
+ res FROM i
+ tmp FROM i
+ __retres FROM i
+ \result FROM i
+[from] Function factorial_ptr:
+ y FROM p_0; result; x (and SELF)
+[from] Function fill_array:
+ array[0..15] FROM data; start; end (and SELF)
+[from] Function five:
+ __retres FROM nondet
+ \result FROM nondet
+[from] Function odd:
+ __retres FROM n
+ \result FROM n
+[from] Function odd_ptr:
+ y FROM n; result (and SELF)
+ a FROM n; result (and SELF)
+[from] Function precond:
+ y FROM x
+[from] Function sum:
+ res FROM i
+ tmp FROM i
+ __retres FROM i
+ \result FROM i
+[from] Function sum_and_fact:
+ x FROM i; sum_0 (and SELF)
+ __retres FROM i
+ \result FROM i
+[from] Function sum_ptr:
+ y FROM p_0; result; x (and SELF)
+[from] Function syracuse:
+ __retres FROM n; i
+ \result FROM n; i
+[from] Function syracuse_ptr:
+ y FROM p_0; result; x (and SELF)
+[from] Function binary_search:
+ mid FROM start; end
+ __retres FROM data; toFind; start; end; array[3..15]
+ \result FROM data; toFind; start; end; array[3..15]
+[from] Function fibonacci:
+ __retres FROM n
+ \result FROM n
+[from] Function fibonacci_ptr:
+ y FROM p_0; result; x (and SELF)
+[from] Function test_array:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ p FROM \nothing (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function alarm:
+ res; tmp; __retres
+[inout] Inputs for function alarm:
+ i; res; tmp; __retres
+[inout] Out (internal) for function decr:
+ x
+[inout] Inputs for function decr:
+ nondet; i
+[inout] Out (internal) for function bug_memexec:
+ \nothing
+[inout] Inputs for function bug_memexec:
+ nondet
+[inout] Out (internal) for function escaping_formal:
+ p; x
+[inout] Inputs for function escaping_formal:
+ nondet; p; count; x
+[inout] Out (internal) for function escaping_local:
+ p; x
+[inout] Inputs for function escaping_local:
+ nondet; p; count
+[inout] Out (internal) for function escaping_stack:
+ p; x
+[inout] Inputs for function escaping_stack:
+ nondet; p; count; q
+[inout] Out (internal) for function even:
+ tmp; tmp; __retres; __retres
+[inout] Inputs for function even:
+ n; tmp; n; tmp; __retres; __retres
+[inout] Out (internal) for function even_ptr:
+ x; y; b
+[inout] Inputs for function even_ptr:
+ n; result; x; n; result; y
+[inout] Out (internal) for function factorial:
+ res; tmp; __retres
+[inout] Inputs for function factorial:
+ i; res; tmp; __retres
+[inout] Out (internal) for function factorial_ptr:
+ arg; y
+[inout] Inputs for function factorial_ptr:
+ p_0; result; res; x
+[inout] Out (internal) for function fill_array:
+ array[0..15]
+[inout] Inputs for function fill_array:
+ data; start; end
+[inout] Out (internal) for function five:
+ tmp; __retres
+[inout] Inputs for function five:
+ nondet; tmp; __retres
+[inout] Out (internal) for function odd:
+ tmp; tmp; __retres; __retres
+[inout] Inputs for function odd:
+ n; tmp; n; tmp; __retres; __retres
+[inout] Out (internal) for function odd_ptr:
+ x; y; a
+[inout] Inputs for function odd_ptr:
+ n; result; x; n; result; y
+[inout] Out (internal) for function precond:
+ y
+[inout] Inputs for function precond:
+ nondet; x
+[inout] Out (internal) for function sum:
+ res; tmp; __retres
+[inout] Inputs for function sum:
+ i; res; tmp; __retres
+[inout] Out (internal) for function sum_and_fact:
+ fact; tmp_0; x; __retres
+[inout] Inputs for function sum_and_fact:
+ i; sum_0; tmp; fact; tmp_0; __retres
+[inout] Out (internal) for function sum_ptr:
+ arg; y
+[inout] Inputs for function sum_ptr:
+ p_0; result; res; x
+[inout] Out (internal) for function syracuse:
+ prev; __retres
+[inout] Inputs for function syracuse:
+ n; i; prev; __retres
+[inout] Out (internal) for function syracuse_ptr:
+ prev_arg; y
+[inout] Inputs for function syracuse_ptr:
+ n; p_0; result; prev_res; x
+[inout] Out (internal) for function binary_search:
+ mid; tmp; tmp_0; __retres
+[inout] Inputs for function binary_search:
+ data; toFind; start; end; mid; tmp; tmp_0; array[3..15]; __retres
+[inout] Out (internal) for function fibonacci:
+ x; y; __retres
+[inout] Inputs for function fibonacci:
+ n; x; y; __retres
+[inout] Out (internal) for function fibonacci_ptr:
+ a; y
+[inout] Inputs for function fibonacci_ptr:
+ p_0; result; x; y; a; x
+[inout] Out (internal) for function test_array:
+ Frama_C_entropy_source; array[0..15]; i; j; end
+[inout] Inputs for function test_array:
+ Frama_C_entropy_source; nondet
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; p; a; b; x; y; tmp; tmp_0; tmp_1; tmp_2
+[inout] Inputs for function main:
+ Frama_C_entropy_source; nondet; p
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c4c6916fda19c0763ef4ab50cc3d834a54df296a
--- /dev/null
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing tests/value/recursion.c (with preprocessing)
+[eva] Analyzing a complete application starting at main_fail
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+ p ∈ {0}
+[eva:recursion] tests/value/recursion.c:422:
+ detected recursive call of function sum_nospec.
+[eva] tests/value/recursion.c:429: Frama_C_show_each_10: {10}
+[eva] tests/value/recursion.c:434: Frama_C_show_each_36: {36}
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/recursion.c:422: User Error:
+ Recursive call to sum_nospec without a specification. Try to increase
+ the -eva-unroll-recursive-calls parameter or write a specification
+ for function sum_nospec.
+[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle/recursion2.res.oracle b/tests/value/oracle/recursion2.res.oracle
deleted file mode 100644
index 37b6e009a2a68a864ce6ca86744f97e5a6e2ef92..0000000000000000000000000000000000000000
--- a/tests/value/oracle/recursion2.res.oracle
+++ /dev/null
@@ -1,67 +0,0 @@
-[kernel] Parsing tests/value/recursion2.i (no 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
- x ∈ {0}
- y ∈ {0}
-[eva] computing for function h2 <- main.
- Called from tests/value/recursion2.i:21.
-[eva] computing for function h1 <- h2 <- main.
- Called from tests/value/recursion2.i:17.
-[eva] Recording results for h1
-[eva] Done for function h1
-[eva] Recording results for h2
-[eva] Done for function h2
-[eva] computing for function h1 <- main.
- Called from tests/value/recursion2.i:22.
-[eva] computing for function h2 <- h1 <- main.
- Called from tests/value/recursion2.i:12.
-[eva] Recording results for h2
-[eva] Done for function h2
-[eva] Recording results for h1
-[eva] Done for function h1
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function h1:
- r ∈ {0}
- q ∈ {0}
-[eva:final-states] Values at end of function h2:
- r ∈ {0}
- q ∈ {0}
-[eva:final-states] Values at end of function main:
-
-[inout] Out (internal) for function h1:
- r; q
-[inout] Inputs for function h1:
- x; y; i; j
-[inout] InOut (internal) for function h1:
- Operational inputs:
- x; y; i
- Operational inputs on termination:
- x; y; i
- Sure outputs:
- r
-[inout] Out (internal) for function h2:
- r; q
-[inout] Inputs for function h2:
- x; y; i; j
-[inout] InOut (internal) for function h2:
- Operational inputs:
- x; y; j
- Operational inputs on termination:
- x; y; j
- Sure outputs:
- q
-[inout] Out (internal) for function main:
- \nothing
-[inout] Inputs for function main:
- x; y
-[inout] InOut (internal) for function main:
- Operational inputs:
- x; y
- Operational inputs on termination:
- x; y
- Sure outputs:
- \nothing
diff --git a/tests/value/oracle_apron/recursion.0.res.oracle b/tests/value/oracle_apron/recursion.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..424fb0f10c57946bd4a9bf10e95994d708e89a4a
--- /dev/null
+++ b/tests/value/oracle_apron/recursion.0.res.oracle
@@ -0,0 +1,628 @@
+10,632c10,12
+< [eva] tests/value/recursion.c:18: Warning:
+< Using specification of function five for recursive calls.
+< Analysis of function five is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function five
+< [eva:alarm] tests/value/recursion.c:15: Warning:
+< function five: postcondition got status unknown.
+< [eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
+< [eva:recursion] tests/value/recursion.c:28:
+< detected recursive call of function sum.
+< [eva] tests/value/recursion.c:28: Warning:
+< Using specification of function sum for recursive calls.
+< Analysis of function sum is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function sum
+< [eva:alarm] tests/value/recursion.c:24: Warning:
+< function sum: postcondition got status unknown.
+< [eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
+< [eva:recursion] tests/value/recursion.c:37:
+< detected recursive call of function factorial.
+< [eva] tests/value/recursion.c:37: Warning:
+< Using specification of function factorial for recursive calls.
+< Analysis of function factorial is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function factorial
+< [eva] tests/value/recursion.c:346: Frama_C_show_each_120: [0..4294967295]
+< [eva:recursion] tests/value/recursion.c:46:
+< detected recursive call of function syracuse.
+< [eva] tests/value/recursion.c:46: Warning:
+< Using specification of function syracuse for recursive calls.
+< Analysis of function syracuse is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function syracuse
+< [eva] tests/value/recursion.c:348: Frama_C_show_each_1: [0..4294967294]
+< [eva:recursion] tests/value/recursion.c:59:
+< detected recursive call of function fibonacci.
+< [eva] tests/value/recursion.c:59: Warning:
+< Using specification of function fibonacci for recursive calls.
+< Analysis of function fibonacci is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function fibonacci
+< [eva:recursion] tests/value/recursion.c:60:
+< detected recursive call of function fibonacci.
+< [eva] tests/value/recursion.c:60: Warning:
+< Using specification of function fibonacci for recursive calls.
+< Analysis of function fibonacci is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] tests/value/recursion.c:350: Frama_C_show_each_89: [0..4294967295]
+< [eva:recursion] tests/value/recursion.c:76:
+< detected recursive call of function sum_ptr.
+< [eva] tests/value/recursion.c:76: Warning:
+< Using specification of function sum_ptr for recursive calls.
+< Analysis of function sum_ptr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function sum_ptr
+< [eva:alarm] tests/value/recursion.c:68: Warning:
+< function sum_ptr: postcondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:69: Warning:
+< function sum_ptr: postcondition got status unknown.
+< [eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
+< [eva:recursion] tests/value/recursion.c:89:
+< detected recursive call of function factorial_ptr.
+< [eva] tests/value/recursion.c:89: Warning:
+< Using specification of function factorial_ptr for recursive calls.
+< Analysis of function factorial_ptr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function factorial_ptr
+< [eva:alarm] tests/value/recursion.c:90: Warning:
+< accessing uninitialized left-value. assert \initialized(&res);
+< [eva] tests/value/recursion.c:358: Frama_C_show_each_120: [0..4294967295]
+< [eva:recursion] tests/value/recursion.c:101:
+< detected recursive call of function syracuse_ptr.
+< [eva] tests/value/recursion.c:101: Warning:
+< Using specification of function syracuse_ptr for recursive calls.
+< Analysis of function syracuse_ptr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function syracuse_ptr
+< [eva:alarm] tests/value/recursion.c:102: Warning:
+< accessing uninitialized left-value. assert \initialized(&prev_res);
+< [eva] tests/value/recursion.c:361: Frama_C_show_each_1: [0..4294967294]
+< [eva:recursion] tests/value/recursion.c:117:
+< detected recursive call of function fibonacci_ptr.
+< [eva] tests/value/recursion.c:117: Warning:
+< Using specification of function fibonacci_ptr for recursive calls.
+< Analysis of function fibonacci_ptr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function fibonacci_ptr
+< [eva:recursion] tests/value/recursion.c:119:
+< detected recursive call of function fibonacci_ptr.
+< [eva] tests/value/recursion.c:119: Warning:
+< Using specification of function fibonacci_ptr for recursive calls.
+< Analysis of function fibonacci_ptr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva:alarm] tests/value/recursion.c:120: Warning:
+< accessing uninitialized left-value. assert \initialized(&x);
+< [eva:alarm] tests/value/recursion.c:120: Warning:
+< accessing uninitialized left-value. assert \initialized(&y);
+< [eva] tests/value/recursion.c:364: Frama_C_show_each_89: [0..4294967295]
+< [eva:recursion] tests/value/recursion.c:137:
+< detected recursive call of function sum_and_fact.
+< [eva] tests/value/recursion.c:137: Warning:
+< Using specification of function sum_and_fact for recursive calls.
+< Analysis of function sum_and_fact is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function sum_and_fact
+< [eva:alarm] tests/value/recursion.c:128: Warning:
+< function sum_and_fact: postcondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:129: Warning:
+< function sum_and_fact: postcondition got status unknown.
+< [eva] tests/value/recursion.c:368:
+< Frama_C_show_each_36_40320: {36}, [0..4294967288],0%8
+< [eva:recursion] tests/value/recursion.c:161:
+< detected recursive call of function odd.
+< [eva] tests/value/recursion.c:161: Warning:
+< Using specification of function odd for recursive calls.
+< Analysis of function odd is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function odd
+< [eva:alarm] tests/value/recursion.c:149: Warning:
+< function odd: postcondition got status unknown.
+< [eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
+< [eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
+< [eva:recursion] tests/value/recursion.c:183:
+< detected recursive call of function odd_ptr.
+< [eva] tests/value/recursion.c:183: Warning:
+< Using specification of function odd_ptr for recursive calls.
+< Analysis of function odd_ptr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function odd_ptr
+< [eva:alarm] tests/value/recursion.c:167: Warning:
+< function odd_ptr: postcondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:184: Warning:
+< accessing uninitialized left-value. assert \initialized(&y);
+< [eva:alarm] tests/value/recursion.c:179: Warning:
+< function even_ptr: postcondition got status unknown.
+< [eva:recursion] tests/value/recursion.c:171:
+< detected recursive call of function even_ptr.
+< [eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
+< [eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
+< [eva] using specification for function Frama_C_interval
+< [eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
+< [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
+< [eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [0..4294967295]
+< [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [0..4294967295]
+< [eva:alarm] tests/value/recursion.c:222: Warning:
+< function fill_array: precondition got status invalid.
+< [eva:alarm] tests/value/recursion.c:226: Warning:
+< function fill_array: precondition got status unknown.
+< [eva:recursion] tests/value/recursion.c:200:
+< detected recursive call of function fill_array.
+< [eva] tests/value/recursion.c:200: Warning:
+< Using specification of function fill_array for recursive calls.
+< Analysis of function fill_array is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function fill_array
+< [eva:alarm] tests/value/recursion.c:200: Warning:
+< function fill_array: precondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:194: Warning:
+< function fill_array: postcondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:228: Warning:
+< function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
+< [eva:recursion] tests/value/recursion.c:214:
+< detected recursive call of function binary_search.
+< [eva] tests/value/recursion.c:214: Warning:
+< Using specification of function binary_search for recursive calls.
+< Analysis of function binary_search is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function binary_search
+< [eva:recursion] tests/value/recursion.c:216:
+< detected recursive call of function binary_search.
+< [eva] tests/value/recursion.c:216: Warning:
+< Using specification of function binary_search for recursive calls.
+< Analysis of function binary_search is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] tests/value/recursion.c:229:
+< Frama_C_show_each_3: [-2147483648..2147483647]
+< [eva] tests/value/recursion.c:231:
+< Frama_C_show_each_12: [-2147483648..2147483647]
+< [eva] tests/value/recursion.c:233:
+< Frama_C_show_each_minus1: [-2147483648..2147483647]
+< [eva] tests/value/recursion.c:238:
+< Frama_C_show_each_7_11: [-2147483648..2147483647]
+< [eva] tests/value/recursion.c:241:
+< Frama_C_show_each_minus_1_15: [-2147483648..2147483647]
+< [eva:recursion] tests/value/recursion.c:252:
+< detected recursive call of function alarm.
+< [eva] tests/value/recursion.c:252: Warning:
+< Using specification of function alarm for recursive calls.
+< Analysis of function alarm is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function alarm
+< [eva:alarm] tests/value/recursion.c:247: Warning:
+< function alarm: postcondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:252: Warning:
+< signed overflow. assert i * tmp ≤ 2147483647;
+< (tmp from alarm(i - 1))
+< [eva] tests/value/recursion.c:406:
+< Frama_C_show_each_unreachable: [20..2147483640],0%20
+< [eva:recursion] tests/value/recursion.c:261:
+< detected recursive call of function precond.
+< [eva] tests/value/recursion.c:261: Warning:
+< Using specification of function precond for recursive calls.
+< Analysis of function precond is thus incomplete and its soundness
+< relies on the written specification.
+< [inout] Warning: no assigns clauses for function precond.
+< Results will be imprecise.
+< [eva] using specification for function precond
+< [eva] tests/value/recursion.c:261: Warning:
+< Cannot handle empty assigns clause. Assuming assigns \nothing: be aware this is probably incorrect.
+< [eva:recursion] tests/value/recursion.c:276:
+< detected recursive call of function escaping_local.
+< [eva] tests/value/recursion.c:276: Warning:
+< Using specification of function escaping_local for recursive calls.
+< Analysis of function escaping_local is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function escaping_local
+< [eva:alarm] tests/value/recursion.c:278: Warning:
+< out of bounds write. assert \valid(p);
+< [eva] tests/value/recursion.c:279: Frama_C_show_each_1: {5}
+< [eva:locals-escaping] tests/value/recursion.c:277: Warning:
+< locals {x} escaping the scope of a block of escaping_local through p
+< [eva:recursion] tests/value/recursion.c:291:
+< detected recursive call of function escaping_formal.
+< [eva] tests/value/recursion.c:291: Warning:
+< Using specification of function escaping_formal for recursive calls.
+< Analysis of function escaping_formal is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function escaping_formal
+< [eva:alarm] tests/value/recursion.c:293: Warning:
+< out of bounds write. assert \valid(p);
+< [eva] tests/value/recursion.c:294: Frama_C_show_each_1: {5}
+< [eva:locals-escaping] tests/value/recursion.c:411: Warning:
+< locals {x} escaping the scope of escaping_formal through p
+< [eva:recursion] tests/value/recursion.c:307:
+< detected recursive call of function escaping_stack.
+< [eva] tests/value/recursion.c:307: Warning:
+< Using specification of function escaping_stack for recursive calls.
+< Analysis of function escaping_stack is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function escaping_stack
+< [eva:alarm] tests/value/recursion.c:309: Warning:
+< out of bounds write. assert \valid(p);
+< [eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {5}
+< [eva:locals-escaping] tests/value/recursion.c:308: Warning:
+< locals {x} escaping the scope of a block of escaping_stack through p
+< [eva:recursion] tests/value/recursion.c:323:
+< detected recursive call of function decr.
+< [eva] tests/value/recursion.c:323: Warning:
+< Using specification of function decr for recursive calls.
+< Analysis of function decr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function decr
+< [eva] done for function main
+< [eva] ====== VALUES COMPUTED ======
+< [eva:final-states] Values at end of function alarm:
+< res ∈ [10..2147483647]
+< __retres ∈ [10..2147483647]
+< [eva:final-states] Values at end of function decr:
+<
+< [eva:final-states] Values at end of function bug_memexec:
+<
+< [eva:final-states] Values at end of function escaping_formal:
+< p ∈ {{ NULL + [--..--] ; &x }}
+< x ∈ [--..--]
+< [eva:final-states] Values at end of function escaping_local:
+< p ∈ [--..--] or ESCAPINGADDR
+< [eva:final-states] Values at end of function escaping_stack:
+< p ∈
+< {{ garbled mix of &{a}
+< (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
+< a ∈ [--..--]
+< [eva:final-states] Values at end of function even:
+< __retres ∈ UNINITIALIZED
+< __retres ∈ {0; 1}
+< [eva:final-states] Values at end of function even_ptr:
+< x ∈ [--..--]
+< b ∈ {0; 1}
+< [eva:final-states] Values at end of function factorial:
+< res ∈ [--..--]
+< __retres ∈ [--..--]
+< [eva:final-states] Values at end of function factorial_ptr:
+< y ∈ [--..--]
+< [eva:final-states] Values at end of function fill_array:
+< array[0] ∈ {0}
+< [1..10] ∈ [--..--]
+< [11..15] ∈ [--..--] or UNINITIALIZED
+< [eva:final-states] Values at end of function five:
+< __retres ∈ {5}
+< [eva:final-states] Values at end of function odd:
+< __retres ∈ {0; 1}
+< __retres ∈ UNINITIALIZED
+< [eva:final-states] Values at end of function odd_ptr:
+< y ∈ [--..--]
+< a ∈ [--..--]
+< [eva:final-states] Values at end of function precond:
+< Cannot filter: dumping raw memory (including unchanged variables)
+< Frama_C_entropy_source ∈ [--..--]
+< nondet ∈ [--..--]
+< x ∈ {1}
+< y ∈ {-6}
+< p ∈ {0}
+< a ∈ {0}
+< b ∈ {0}
+< x ∈ [10..20]
+< y ∈ [10..2147483647]
+< tmp ∈ [3..11]
+< tmp_0 ∈ [10..20]
+< tmp_1 ∈ [10..2147483647]
+< [eva:final-states] Values at end of function sum:
+< res ∈ [6..91]
+< __retres ∈ [6..91]
+< [eva:final-states] Values at end of function sum_and_fact:
+< x ∈ {36}
+< __retres ∈ [0..4294967288],0%8
+< [eva:final-states] Values at end of function sum_ptr:
+< y ∈ [6..91]
+< [eva:final-states] Values at end of function syracuse:
+< __retres ∈ [0..4294967294]
+< [eva:final-states] Values at end of function syracuse_ptr:
+< y ∈ [0..4294967294]
+< [eva:final-states] Values at end of function binary_search:
+< mid ∈ {7}
+< __retres ∈ [--..--]
+< [eva:final-states] Values at end of function fibonacci:
+< __retres ∈ [--..--]
+< [eva:final-states] Values at end of function fibonacci_ptr:
+< y ∈ [--..--]
+< [eva:final-states] Values at end of function test_array:
+< Frama_C_entropy_source ∈ [--..--]
+< array[0] ∈ {0}
+< [1..9] ∈ [--..--]
+< [10] ∈ {10}
+< [11..15] ∈ [--..--]
+< i ∈ [--..--]
+< j ∈ [7..18]
+< end ∈ {10; 11; 12; 13; 14; 15; 16}
+< [eva:final-states] Values at end of function main:
+< Cannot filter: dumping raw memory (including unchanged variables)
+< Frama_C_entropy_source ∈ [--..--]
+< nondet ∈ [--..--]
+< p ∈
+< {{ garbled mix of &{a}
+< (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
+< a ∈ [--..--]
+< b ∈ {0}
+< x ∈ [10..20]
+< y ∈ [10..2147483647]
+< tmp ∈ [3..11]
+< tmp_0 ∈ [10..20]
+< tmp_1 ∈ [10..2147483647]
+< [from] Computing for function alarm
+< [from] Computing for function alarm <-alarm
+< [from] Done for function alarm
+< [from] Done for function alarm
+< [from] Computing for function decr
+< [from] Computing for function decr <-decr
+< [from] Done for function decr
+< [from] Done for function decr
+< [from] Computing for function bug_memexec
+< [from] Done for function bug_memexec
+< [from] Computing for function escaping_formal
+< [from] Computing for function escaping_formal <-escaping_formal
+< [from] Done for function escaping_formal
+< [from] Done for function escaping_formal
+< [from] Computing for function escaping_local
+< [from] Computing for function escaping_local <-escaping_local
+< [from] Done for function escaping_local
+< [from] Done for function escaping_local
+< [from] Computing for function escaping_stack
+< [from] Computing for function escaping_stack <-escaping_stack
+< [from] Done for function escaping_stack
+< [from] Done for function escaping_stack
+< [from] Computing for function even
+< [from] Computing for function odd <-even
+< [from] Computing for function even <-odd <-even
+< [from] Done for function even
+< [from] Done for function odd
+< [from] Done for function even
+< [from] Computing for function even_ptr
+< [from] Computing for function odd_ptr <-even_ptr
+< [from] Computing for function even_ptr <-odd_ptr <-even_ptr
+< [from] Done for function even_ptr
+< [from] Done for function odd_ptr
+< [from] Done for function even_ptr
+< [from] Computing for function factorial
+< [from] Computing for function factorial <-factorial
+< [from] Done for function factorial
+< [from] Done for function factorial
+< [from] Computing for function factorial_ptr
+< [from] Computing for function factorial_ptr <-factorial_ptr
+< [from] Done for function factorial_ptr
+< [from] Done for function factorial_ptr
+< [from] Computing for function fill_array
+< [from] Computing for function fill_array <-fill_array
+< [from] Done for function fill_array
+< [from] Done for function fill_array
+< [from] Computing for function five
+< [from] Computing for function five <-five
+< [from] Done for function five
+< [from] Done for function five
+< [from] Computing for function precond
+< [from] Computing for function precond <-precond
+< [from] Done for function precond
+< [from] Done for function precond
+< [from] Computing for function sum
+< [from] Computing for function sum <-sum
+< [from] Done for function sum
+< [from] Done for function sum
+< [from] Computing for function sum_and_fact
+< [from] Computing for function sum_and_fact <-sum_and_fact
+< [from] Done for function sum_and_fact
+< [from] Done for function sum_and_fact
+< [from] Computing for function sum_ptr
+< [from] Computing for function sum_ptr <-sum_ptr
+< [from] Done for function sum_ptr
+< [from] Done for function sum_ptr
+< [from] Computing for function syracuse
+< [from] Computing for function syracuse <-syracuse
+< [from] Done for function syracuse
+< [from] Done for function syracuse
+< [from] Computing for function syracuse_ptr
+< [from] Computing for function syracuse_ptr <-syracuse_ptr
+< [from] Done for function syracuse_ptr
+< [from] Done for function syracuse_ptr
+< [from] Computing for function binary_search
+< [from] Computing for function binary_search <-binary_search
+< [from] Done for function binary_search
+< [from] Done for function binary_search
+< [from] Computing for function fibonacci
+< [from] Computing for function fibonacci <-fibonacci
+< [from] Done for function fibonacci
+< [from] Done for function fibonacci
+< [from] Computing for function fibonacci_ptr
+< [from] Computing for function fibonacci_ptr <-fibonacci_ptr
+< [from] Done for function fibonacci_ptr
+< [from] Done for function fibonacci_ptr
+< [from] Computing for function test_array
+< [from] Computing for function Frama_C_interval <-test_array
+< [from] Done for function Frama_C_interval
+< [from] Done for function test_array
+< [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 alarm:
+< res FROM i
+< tmp FROM i
+< __retres FROM i
+< \result FROM i
+< [from] Function decr:
+< NO EFFECTS
+< [from] Function bug_memexec:
+< NO EFFECTS
+< [from] Function escaping_formal:
+< p FROM count
+< x FROM nondet; count (and SELF)
+< [from] Function escaping_local:
+< p FROM count
+< [from] Function escaping_stack:
+< p FROM count; q
+< a FROM nondet; count; q (and SELF)
+< [from] Function even:
+< __retres FROM n
+< __retres FROM n
+< \result FROM n
+< [from] Function even_ptr:
+< x FROM n; result (and SELF)
+< a FROM n (and SELF)
+< b FROM n; result (and SELF)
+< [from] Function factorial:
+< res FROM i
+< tmp FROM i
+< __retres FROM i
+< \result FROM i
+< [from] Function factorial_ptr:
+< y FROM p_0; result; x
+< [from] Function fill_array:
+< array{[0]; [10]} FROM data; start; end (and SELF)
+< [from] Function five:
+< __retres FROM nondet
+< \result FROM nondet
+< [from] Function odd:
+< __retres FROM n
+< \result FROM n
+< [from] Function odd_ptr:
+< y FROM n; result (and SELF)
+< a FROM n; result (and SELF)
+< [from] Function precond:
+< y FROM x
+< [from] Function sum:
+< res FROM i
+< tmp FROM i
+< __retres FROM i
+< \result FROM i
+< [from] Function sum_and_fact:
+< x FROM i; sum_0
+< __retres FROM i
+< \result FROM i
+< [from] Function sum_ptr:
+< y FROM p_0; result; x
+< [from] Function syracuse:
+< __retres FROM i
+< \result FROM i
+< [from] Function syracuse_ptr:
+< y FROM p_0; result; x
+< [from] Function binary_search:
+< mid FROM start; end
+< __retres FROM data; toFind; start; end; array[7]
+< \result FROM data; toFind; start; end; array[7]
+< [from] Function fibonacci:
+< __retres FROM n
+< \result FROM n
+< [from] Function fibonacci_ptr:
+< y FROM p_0; result; x
+< [from] Function test_array:
+< Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+< [from] Function main:
+< Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+< p FROM \nothing
+< [from] ====== END OF DEPENDENCIES ======
+< [inout] Out (internal) for function alarm:
+< res; tmp; __retres
+< [inout] Inputs for function alarm:
+< i; res; tmp; __retres
+< [inout] Out (internal) for function decr:
+< x
+< [inout] Inputs for function decr:
+< nondet; i
+< [inout] Out (internal) for function bug_memexec:
+< \nothing
+< [inout] Inputs for function bug_memexec:
+< nondet
+< [inout] Out (internal) for function escaping_formal:
+< p; x
+< [inout] Inputs for function escaping_formal:
+< nondet; p; count; x
+< [inout] Out (internal) for function escaping_local:
+< p; x
+< [inout] Inputs for function escaping_local:
+< nondet; p; count
+< [inout] Out (internal) for function escaping_stack:
+< p; x; a
+< [inout] Inputs for function escaping_stack:
+< nondet; p; count; q
+< [inout] Out (internal) for function even:
+< tmp; tmp; __retres; __retres
+< [inout] Inputs for function even:
+< n; tmp; n; tmp; __retres; __retres
+< [inout] Out (internal) for function even_ptr:
+< x; y; b
+< [inout] Inputs for function even_ptr:
+< n; result; x; n; result; y
+< [inout] Out (internal) for function factorial:
+< res; tmp; __retres
+< [inout] Inputs for function factorial:
+< i; res; tmp; __retres
+< [inout] Out (internal) for function factorial_ptr:
+< arg; y
+< [inout] Inputs for function factorial_ptr:
+< p_0; result; res; x
+< [inout] Out (internal) for function fill_array:
+< array[0..15]
+< [inout] Inputs for function fill_array:
+< data; start; end
+< [inout] Out (internal) for function five:
+< tmp; __retres
+< [inout] Inputs for function five:
+< nondet; tmp; __retres
+< [inout] Out (internal) for function odd:
+< tmp; tmp; __retres; __retres
+< [inout] Inputs for function odd:
+< n; tmp; n; tmp; __retres; __retres
+< [inout] Out (internal) for function odd_ptr:
+< x; y; a
+< [inout] Inputs for function odd_ptr:
+< n; result; x; n; result; y
+< [inout] Out (internal) for function precond:
+< ANYTHING(origin:Unknown)
+< [inout] Inputs for function precond:
+< nondet; x
+< [inout] Out (internal) for function sum:
+< res; tmp; __retres
+< [inout] Inputs for function sum:
+< i; res; tmp; __retres
+< [inout] Out (internal) for function sum_and_fact:
+< fact; tmp_0; x; __retres
+< [inout] Inputs for function sum_and_fact:
+< i; sum_0; tmp; fact; tmp_0; __retres
+< [inout] Out (internal) for function sum_ptr:
+< arg; y
+< [inout] Inputs for function sum_ptr:
+< p_0; result; res; x
+< [inout] Out (internal) for function syracuse:
+< prev; __retres
+< [inout] Inputs for function syracuse:
+< n; i; prev; __retres
+< [inout] Out (internal) for function syracuse_ptr:
+< prev_arg; y
+< [inout] Inputs for function syracuse_ptr:
+< n; p_0; result; prev_res; x
+< [inout] Out (internal) for function binary_search:
+< mid; tmp; tmp_0; __retres
+< [inout] Inputs for function binary_search:
+< data; toFind; start; end; mid; tmp; tmp_0; array[7]; __retres
+< [inout] Out (internal) for function fibonacci:
+< x; y; __retres
+< [inout] Inputs for function fibonacci:
+< n; x; y; __retres
+< [inout] Out (internal) for function fibonacci_ptr:
+< a; y
+< [inout] Inputs for function fibonacci_ptr:
+< p_0; result; x; y; a; x
+< [inout] Out (internal) for function test_array:
+< Frama_C_entropy_source; array[0..15]; i; j; end
+< [inout] Inputs for function test_array:
+< Frama_C_entropy_source; nondet
+< [inout] Out (internal) for function main:
+< ANYTHING(origin:Unknown)
+< [inout] Inputs for function main:
+< Frama_C_entropy_source; nondet; p
+---
+> [eva] tests/value/recursion.c:18: User Error:
+> The binding to APRON domains does not support recursive calls.
+> [kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle_apron/recursion.1.res.oracle b/tests/value/oracle_apron/recursion.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7556d61ac85a09c7c94d6176127ef66655521b91
--- /dev/null
+++ b/tests/value/oracle_apron/recursion.1.res.oracle
@@ -0,0 +1,510 @@
+10,514c10,12
+< [eva] tests/value/recursion.c:18: Warning:
+< Using specification of function five for recursive calls of depth 20.
+< Analysis of function five is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function five
+< [eva:alarm] tests/value/recursion.c:15: Warning:
+< function five: postcondition got status unknown.
+< [eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
+< [eva:recursion] tests/value/recursion.c:28:
+< detected recursive call of function sum.
+< [eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
+< [eva:recursion] tests/value/recursion.c:37:
+< detected recursive call of function factorial.
+< [eva] tests/value/recursion.c:346: Frama_C_show_each_120: {120}
+< [eva:recursion] tests/value/recursion.c:46:
+< detected recursive call of function syracuse.
+< [eva] tests/value/recursion.c:348: Frama_C_show_each_1: {1}
+< [eva:recursion] tests/value/recursion.c:59:
+< detected recursive call of function fibonacci.
+< [eva:recursion] tests/value/recursion.c:60:
+< detected recursive call of function fibonacci.
+< [eva] tests/value/recursion.c:350: Frama_C_show_each_89: {89}
+< [eva:recursion] tests/value/recursion.c:76:
+< detected recursive call of function sum_ptr.
+< [eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
+< [eva:recursion] tests/value/recursion.c:89:
+< detected recursive call of function factorial_ptr.
+< [eva] tests/value/recursion.c:358: Frama_C_show_each_120: {120}
+< [eva:recursion] tests/value/recursion.c:101:
+< detected recursive call of function syracuse_ptr.
+< [eva] tests/value/recursion.c:361: Frama_C_show_each_1: {1}
+< [eva:recursion] tests/value/recursion.c:117:
+< detected recursive call of function fibonacci_ptr.
+< [eva:recursion] tests/value/recursion.c:119:
+< detected recursive call of function fibonacci_ptr.
+< [eva] tests/value/recursion.c:364: Frama_C_show_each_89: {89}
+< [eva:recursion] tests/value/recursion.c:137:
+< detected recursive call of function sum_and_fact.
+< [eva] tests/value/recursion.c:368: Frama_C_show_each_36_40320: {36}, {40320}
+< [eva:recursion] tests/value/recursion.c:161:
+< detected recursive call of function odd.
+< [eva:recursion] tests/value/recursion.c:152:
+< detected recursive call of function even.
+< [eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
+< [eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
+< [eva:recursion] tests/value/recursion.c:183:
+< detected recursive call of function odd_ptr.
+< [eva:recursion] tests/value/recursion.c:171:
+< detected recursive call of function even_ptr.
+< [eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
+< [eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
+< [eva] using specification for function Frama_C_interval
+< [eva:alarm] tests/value/recursion.c:24: Warning:
+< function sum: postcondition got status unknown.
+< [eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
+< [eva:alarm] tests/value/recursion.c:69: Warning:
+< function sum_ptr: postcondition got status unknown.
+< [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
+< [eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [2..89]
+< [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [2..89]
+< [eva:alarm] tests/value/recursion.c:222: Warning:
+< function fill_array: precondition got status invalid.
+< [eva:alarm] tests/value/recursion.c:226: Warning:
+< function fill_array: precondition got status unknown.
+< [eva:recursion] tests/value/recursion.c:200:
+< detected recursive call of function fill_array.
+< [eva:alarm] tests/value/recursion.c:200: Warning:
+< function fill_array: precondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:199: Warning:
+< out of bounds write. assert \valid(data + start);
+< [kernel] tests/value/recursion.c:199: Warning:
+< all target addresses were invalid. This path is assumed to be dead.
+< [eva:alarm] tests/value/recursion.c:194: Warning:
+< function fill_array: postcondition got status unknown.
+< [eva:alarm] tests/value/recursion.c:228: Warning:
+< function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
+< [eva:recursion] tests/value/recursion.c:214:
+< detected recursive call of function binary_search.
+< [eva] tests/value/recursion.c:229: Frama_C_show_each_3: {3}
+< [eva:recursion] tests/value/recursion.c:216:
+< detected recursive call of function binary_search.
+< [eva] tests/value/recursion.c:231: Frama_C_show_each_12: {12}
+< [eva] tests/value/recursion.c:233: Frama_C_show_each_minus1: {-1}
+< [eva] tests/value/recursion.c:238: Frama_C_show_each_7_11: {7; 8; 9; 10; 11}
+< [eva] tests/value/recursion.c:241: Frama_C_show_each_minus_1_15: [-1..15]
+< [eva:recursion] tests/value/recursion.c:252:
+< detected recursive call of function alarm.
+< [eva:alarm] tests/value/recursion.c:252: Warning:
+< signed overflow. assert i * tmp ≤ 2147483647;
+< (tmp from alarm(i - 1))
+< [eva:recursion] tests/value/recursion.c:261:
+< detected recursive call of function precond.
+< [eva:alarm] tests/value/recursion.c:261: Warning:
+< function precond: precondition got status invalid.
+< [eva:recursion] tests/value/recursion.c:276:
+< detected recursive call of function escaping_local.
+< [eva] tests/value/recursion.c:279: Frama_C_show_each_1: {1}
+< [eva:locals-escaping] tests/value/recursion.c:277: Warning:
+< locals {x} escaping the scope of a block of escaping_local through p
+< [eva:alarm] tests/value/recursion.c:278: Warning:
+< accessing left-value that contains escaping addresses.
+< assert ¬\dangling(&p);
+< [kernel] tests/value/recursion.c:278: Warning:
+< all target addresses were invalid. This path is assumed to be dead.
+< [eva:recursion] tests/value/recursion.c:291:
+< detected recursive call of function escaping_formal.
+< [eva] tests/value/recursion.c:294: Frama_C_show_each_1: {1}
+< [eva:locals-escaping] tests/value/recursion.c:291: Warning:
+< locals {x} escaping the scope of escaping_formal through p
+< [eva:alarm] tests/value/recursion.c:293: Warning:
+< accessing left-value that contains escaping addresses.
+< assert ¬\dangling(&p);
+< [kernel] tests/value/recursion.c:293: Warning:
+< all target addresses were invalid. This path is assumed to be dead.
+< [eva:recursion] tests/value/recursion.c:307:
+< detected recursive call of function escaping_stack.
+< [eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {1}
+< [eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {2}
+< [eva:locals-escaping] tests/value/recursion.c:308: Warning:
+< locals {x} escaping the scope of a block of escaping_stack through p
+< [eva:alarm] tests/value/recursion.c:309: Warning:
+< accessing left-value that contains escaping addresses.
+< assert ¬\dangling(&p);
+< [kernel] tests/value/recursion.c:309: Warning:
+< all target addresses were invalid. This path is assumed to be dead.
+< [eva:recursion] tests/value/recursion.c:323:
+< detected recursive call of function decr.
+< [eva] tests/value/recursion.c:323: Warning:
+< Using specification of function decr for recursive calls of depth 20.
+< Analysis of function decr is thus incomplete and its soundness
+< relies on the written specification.
+< [eva] using specification for function decr
+< [eva] done for function main
+< [eva] ====== VALUES COMPUTED ======
+< [eva:final-states] Values at end of function alarm:
+< res ∈ [2..2147483647]
+< __retres ∈ [1..2147483647]
+< [eva:final-states] Values at end of function decr:
+<
+< [eva:final-states] Values at end of function bug_memexec:
+<
+< [eva:final-states] Values at end of function escaping_formal:
+< p ∈ {{ &x ; &\copy<x>[5] }} or ESCAPINGADDR
+< x ∈ {5; 16}
+< [eva:final-states] Values at end of function escaping_local:
+< p ∈ {{ &\copy<x>[5] }} or ESCAPINGADDR
+< [eva:final-states] Values at end of function escaping_stack:
+< p ∈ {{ &\copy<x>[4] }} or ESCAPINGADDR
+< [eva:final-states] Values at end of function even:
+< __retres ∈ UNINITIALIZED
+< __retres ∈ {0; 1}
+< [eva:final-states] Values at end of function even_ptr:
+< x ∈ {0; 1}
+< b ∈ {0; 1}
+< [eva:final-states] Values at end of function factorial:
+< res ∈ {2; 6; 24; 120}
+< __retres ∈ {1; 2; 6; 24; 120}
+< [eva:final-states] Values at end of function factorial_ptr:
+< y ∈ {91; 120}
+< [eva:final-states] Values at end of function fill_array:
+< array[0] ∈ {0}
+< [1] ∈ {1}
+< [2] ∈ {2}
+< [3] ∈ {3}
+< [4] ∈ {4}
+< [5] ∈ {5}
+< [6] ∈ {6}
+< [7] ∈ {7}
+< [8] ∈ {8}
+< [9] ∈ {9}
+< [10] ∈ {10}
+< [11] ∈ {11} or UNINITIALIZED
+< [12] ∈ {12} or UNINITIALIZED
+< [13] ∈ {13} or UNINITIALIZED
+< [14] ∈ {14} or UNINITIALIZED
+< [15] ∈ {15} or UNINITIALIZED
+< [eva:final-states] Values at end of function five:
+< __retres ∈ {5}
+< [eva:final-states] Values at end of function odd:
+< __retres ∈ {0; 1}
+< __retres ∈ UNINITIALIZED
+< [eva:final-states] Values at end of function odd_ptr:
+< y ∈ {0; 1}
+< a ∈ {0; 1}
+< [eva:final-states] Values at end of function precond:
+< y ∈ [-100..-6]
+< [eva:final-states] Values at end of function sum:
+< res ∈ [3..91]
+< __retres ∈ [1..91]
+< [eva:final-states] Values at end of function sum_and_fact:
+< x ∈ {11; 36}
+< __retres ∈ {1; 2; 6; 24; 120; 720; 5040; 40320}
+< [eva:final-states] Values at end of function sum_ptr:
+< y ∈ [0..91]
+< [eva:final-states] Values at end of function syracuse:
+< __retres ∈ [1..16]
+< [eva:final-states] Values at end of function syracuse_ptr:
+< y ∈ {1; 120}
+< [eva:final-states] Values at end of function binary_search:
+< mid ∈ [3..16]
+< __retres ∈ [-1..15]
+< [eva:final-states] Values at end of function fibonacci:
+< __retres ∈ [0..89]
+< [eva:final-states] Values at end of function fibonacci_ptr:
+< y ∈ [0..89]
+< [eva:final-states] Values at end of function test_array:
+< Frama_C_entropy_source ∈ [--..--]
+< array[0] ∈ {0}
+< [1] ∈ {1}
+< [2] ∈ {2}
+< [3] ∈ {3}
+< [4] ∈ {4}
+< [5] ∈ {5}
+< [6] ∈ {6}
+< [7] ∈ {7}
+< [8] ∈ {8}
+< [9] ∈ {9}
+< [10] ∈ {10}
+< [11] ∈ {11}
+< [12] ∈ {12}
+< [13] ∈ {13}
+< [14] ∈ {14}
+< [15] ∈ {15}
+< i ∈ [-1..15]
+< j ∈ [7..18]
+< end ∈ {10; 11; 12; 13; 14; 15}
+< [eva:final-states] Values at end of function main:
+< Frama_C_entropy_source ∈ [--..--]
+< p ∈ ESCAPINGADDR
+< a ∈ {0}
+< b ∈ {0}
+< x ∈ [10..20]
+< y ∈ [3628800..2147483647]
+< [from] Computing for function alarm
+< [from] Computing for function alarm <-alarm
+< [from] Done for function alarm
+< [from] Done for function alarm
+< [from] Computing for function decr
+< [from] Computing for function decr <-decr
+< [from] Done for function decr
+< [from] Done for function decr
+< [from] Computing for function bug_memexec
+< [from] Done for function bug_memexec
+< [from] Computing for function escaping_formal
+< [from] Computing for function escaping_formal <-escaping_formal
+< [from] Done for function escaping_formal
+< [from] Done for function escaping_formal
+< [from] Computing for function escaping_local
+< [from] Computing for function escaping_local <-escaping_local
+< [from] Done for function escaping_local
+< [from] Done for function escaping_local
+< [from] Computing for function escaping_stack
+< [from] Computing for function escaping_stack <-escaping_stack
+< [from] Done for function escaping_stack
+< [from] Done for function escaping_stack
+< [from] Computing for function even
+< [from] Computing for function odd <-even
+< [from] Computing for function even <-odd <-even
+< [from] Done for function even
+< [from] Done for function odd
+< [from] Done for function even
+< [from] Computing for function even_ptr
+< [from] Computing for function odd_ptr <-even_ptr
+< [from] Computing for function even_ptr <-odd_ptr <-even_ptr
+< [from] Done for function even_ptr
+< [from] Done for function odd_ptr
+< [from] Done for function even_ptr
+< [from] Computing for function factorial
+< [from] Computing for function factorial <-factorial
+< [from] Done for function factorial
+< [from] Done for function factorial
+< [from] Computing for function factorial_ptr
+< [from] Computing for function factorial_ptr <-factorial_ptr
+< [from] Done for function factorial_ptr
+< [from] Done for function factorial_ptr
+< [from] Computing for function fill_array
+< [from] Computing for function fill_array <-fill_array
+< [from] Done for function fill_array
+< [from] Done for function fill_array
+< [from] Computing for function five
+< [from] Computing for function five <-five
+< [from] Done for function five
+< [from] Done for function five
+< [from] Computing for function precond
+< [from] Computing for function precond <-precond
+< [from] Done for function precond
+< [from] Done for function precond
+< [from] Computing for function sum
+< [from] Computing for function sum <-sum
+< [from] Done for function sum
+< [from] Done for function sum
+< [from] Computing for function sum_and_fact
+< [from] Computing for function sum_and_fact <-sum_and_fact
+< [from] Done for function sum_and_fact
+< [from] Done for function sum_and_fact
+< [from] Computing for function sum_ptr
+< [from] Computing for function sum_ptr <-sum_ptr
+< [from] Done for function sum_ptr
+< [from] Done for function sum_ptr
+< [from] Computing for function syracuse
+< [from] Computing for function syracuse <-syracuse
+< [from] Done for function syracuse
+< [from] Done for function syracuse
+< [from] Computing for function syracuse_ptr
+< [from] Computing for function syracuse_ptr <-syracuse_ptr
+< [from] Done for function syracuse_ptr
+< [from] Done for function syracuse_ptr
+< [from] Computing for function binary_search
+< [from] Computing for function binary_search <-binary_search
+< [from] Done for function binary_search
+< [from] Done for function binary_search
+< [from] Computing for function fibonacci
+< [from] Computing for function fibonacci <-fibonacci
+< [from] Done for function fibonacci
+< [from] Done for function fibonacci
+< [from] Computing for function fibonacci_ptr
+< [from] Computing for function fibonacci_ptr <-fibonacci_ptr
+< [from] Done for function fibonacci_ptr
+< [from] Done for function fibonacci_ptr
+< [from] Computing for function test_array
+< [from] Computing for function Frama_C_interval <-test_array
+< [from] Done for function Frama_C_interval
+< [from] Done for function test_array
+< [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 alarm:
+< res FROM i
+< tmp FROM i
+< __retres FROM i
+< \result FROM i
+< [from] Function decr:
+< NO EFFECTS
+< [from] Function bug_memexec:
+< NO EFFECTS
+< [from] Function escaping_formal:
+< p FROM count (and SELF)
+< x FROM nondet; count (and SELF)
+< [from] Function escaping_local:
+< p FROM count (and SELF)
+< [from] Function escaping_stack:
+< p FROM count; q (and SELF)
+< [from] Function even:
+< __retres FROM n (and SELF)
+< __retres FROM n
+< \result FROM n
+< [from] Function even_ptr:
+< x FROM n; result (and SELF)
+< a FROM n (and SELF)
+< b FROM n; result (and SELF)
+< [from] Function factorial:
+< res FROM i
+< tmp FROM i
+< __retres FROM i
+< \result FROM i
+< [from] Function factorial_ptr:
+< y FROM p_0; result; x (and SELF)
+< [from] Function fill_array:
+< array[0..15] FROM data; start; end (and SELF)
+< [from] Function five:
+< __retres FROM nondet
+< \result FROM nondet
+< [from] Function odd:
+< __retres FROM n
+< \result FROM n
+< [from] Function odd_ptr:
+< y FROM n; result (and SELF)
+< a FROM n; result (and SELF)
+< [from] Function precond:
+< y FROM x
+< [from] Function sum:
+< res FROM i
+< tmp FROM i
+< __retres FROM i
+< \result FROM i
+< [from] Function sum_and_fact:
+< x FROM i; sum_0 (and SELF)
+< __retres FROM i
+< \result FROM i
+< [from] Function sum_ptr:
+< y FROM p_0; result; x (and SELF)
+< [from] Function syracuse:
+< __retres FROM n; i
+< \result FROM n; i
+< [from] Function syracuse_ptr:
+< y FROM p_0; result; x (and SELF)
+< [from] Function binary_search:
+< mid FROM start; end
+< __retres FROM data; toFind; start; end; array[3..15]
+< \result FROM data; toFind; start; end; array[3..15]
+< [from] Function fibonacci:
+< __retres FROM n
+< \result FROM n
+< [from] Function fibonacci_ptr:
+< y FROM p_0; result; x (and SELF)
+< [from] Function test_array:
+< Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+< [from] Function main:
+< Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+< p FROM \nothing (and SELF)
+< [from] ====== END OF DEPENDENCIES ======
+< [inout] Out (internal) for function alarm:
+< res; tmp; __retres
+< [inout] Inputs for function alarm:
+< i; res; tmp; __retres
+< [inout] Out (internal) for function decr:
+< x
+< [inout] Inputs for function decr:
+< nondet; i
+< [inout] Out (internal) for function bug_memexec:
+< \nothing
+< [inout] Inputs for function bug_memexec:
+< nondet
+< [inout] Out (internal) for function escaping_formal:
+< p; x
+< [inout] Inputs for function escaping_formal:
+< nondet; p; count; x
+< [inout] Out (internal) for function escaping_local:
+< p; x
+< [inout] Inputs for function escaping_local:
+< nondet; p; count
+< [inout] Out (internal) for function escaping_stack:
+< p; x
+< [inout] Inputs for function escaping_stack:
+< nondet; p; count; q
+< [inout] Out (internal) for function even:
+< tmp; tmp; __retres; __retres
+< [inout] Inputs for function even:
+< n; tmp; n; tmp; __retres; __retres
+< [inout] Out (internal) for function even_ptr:
+< x; y; b
+< [inout] Inputs for function even_ptr:
+< n; result; x; n; result; y
+< [inout] Out (internal) for function factorial:
+< res; tmp; __retres
+< [inout] Inputs for function factorial:
+< i; res; tmp; __retres
+< [inout] Out (internal) for function factorial_ptr:
+< arg; y
+< [inout] Inputs for function factorial_ptr:
+< p_0; result; res; x
+< [inout] Out (internal) for function fill_array:
+< array[0..15]
+< [inout] Inputs for function fill_array:
+< data; start; end
+< [inout] Out (internal) for function five:
+< tmp; __retres
+< [inout] Inputs for function five:
+< nondet; tmp; __retres
+< [inout] Out (internal) for function odd:
+< tmp; tmp; __retres; __retres
+< [inout] Inputs for function odd:
+< n; tmp; n; tmp; __retres; __retres
+< [inout] Out (internal) for function odd_ptr:
+< x; y; a
+< [inout] Inputs for function odd_ptr:
+< n; result; x; n; result; y
+< [inout] Out (internal) for function precond:
+< y
+< [inout] Inputs for function precond:
+< nondet; x
+< [inout] Out (internal) for function sum:
+< res; tmp; __retres
+< [inout] Inputs for function sum:
+< i; res; tmp; __retres
+< [inout] Out (internal) for function sum_and_fact:
+< fact; tmp_0; x; __retres
+< [inout] Inputs for function sum_and_fact:
+< i; sum_0; tmp; fact; tmp_0; __retres
+< [inout] Out (internal) for function sum_ptr:
+< arg; y
+< [inout] Inputs for function sum_ptr:
+< p_0; result; res; x
+< [inout] Out (internal) for function syracuse:
+< prev; __retres
+< [inout] Inputs for function syracuse:
+< n; i; prev; __retres
+< [inout] Out (internal) for function syracuse_ptr:
+< prev_arg; y
+< [inout] Inputs for function syracuse_ptr:
+< n; p_0; result; prev_res; x
+< [inout] Out (internal) for function binary_search:
+< mid; tmp; tmp_0; __retres
+< [inout] Inputs for function binary_search:
+< data; toFind; start; end; mid; tmp; tmp_0; array[3..15]; __retres
+< [inout] Out (internal) for function fibonacci:
+< x; y; __retres
+< [inout] Inputs for function fibonacci:
+< n; x; y; __retres
+< [inout] Out (internal) for function fibonacci_ptr:
+< a; y
+< [inout] Inputs for function fibonacci_ptr:
+< p_0; result; x; y; a; x
+< [inout] Out (internal) for function test_array:
+< Frama_C_entropy_source; array[0..15]; i; j; end
+< [inout] Inputs for function test_array:
+< Frama_C_entropy_source; nondet
+< [inout] Out (internal) for function main:
+< Frama_C_entropy_source; p; a; b; x; y; tmp; tmp_0; tmp_1; tmp_2
+< [inout] Inputs for function main:
+< Frama_C_entropy_source; nondet; p
+---
+> [eva] tests/value/recursion.c:18: User Error:
+> The binding to APRON domains does not support recursive calls.
+> [kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle_apron/recursion.2.res.oracle b/tests/value/oracle_apron/recursion.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..61f9a6838a929c95b6fd56661df773f25660b4e3
--- /dev/null
+++ b/tests/value/oracle_apron/recursion.2.res.oracle
@@ -0,0 +1,10 @@
+10,12d9
+< [eva] tests/value/recursion.c:429: Frama_C_show_each_10: {10}
+< [eva] tests/value/recursion.c:434: Frama_C_show_each_36: {36}
+< [eva] using specification for function Frama_C_interval
+14,16c11
+< Recursive call to sum_nospec without a specification. Try to increase
+< the -eva-unroll-recursive-calls parameter or write a specification
+< for function sum_nospec.
+---
+> The binding to APRON domains does not support recursive calls.
diff --git a/tests/value/rec.i b/tests/value/rec.i
deleted file mode 100644
index dcbe796370f429c7945141198bde9e110c758103..0000000000000000000000000000000000000000
--- a/tests/value/rec.i
+++ /dev/null
@@ -1,5 +0,0 @@
-void main() {
- int X=0;
- if (X) main();
-
-}
diff --git a/tests/value/recursion.c b/tests/value/recursion.c
new file mode 100644
index 0000000000000000000000000000000000000000..1dad1842fcd65526388f6ca3bc2d1a08a340c7d3
--- /dev/null
+++ b/tests/value/recursion.c
@@ -0,0 +1,439 @@
+/* run.config*
+ STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 0"
+ STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 20"
+ EXIT: 1
+ STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 5 -main main_fail"
+*/
+
+#include <__fc_builtin.h>
+
+volatile int nondet;
+
+/* ----- Simple recursive functions. ---------------------------------------- */
+
+/*@ assigns \result \from \nothing;
+ ensures \result == 5; */
+int five () {
+ if (nondet)
+ return five();
+ else
+ return 5;
+}
+
+/*@ assigns \result \from i;
+ ensures \result == (i * (i+1)) / 2; */
+unsigned int sum (unsigned int i) {
+ if (i < 2)
+ return i;
+ unsigned int res = i + sum(i - 1);
+ return res;
+}
+
+/*@ assigns \result \from i; */
+unsigned int factorial (unsigned int i) {
+ if(i <= 1) {
+ return 1;
+ }
+ unsigned int res = i * factorial(i - 1);
+ return res;
+}
+
+/*@ assigns \result \from i, n; */
+unsigned int syracuse (unsigned int n, unsigned int i) {
+ if (i == 0)
+ return n;
+ else {
+ unsigned int prev = syracuse(n, i-1);
+ if (prev % 2)
+ return 3*prev + 1;
+ else
+ return prev / 2;
+ }
+}
+
+/*@ assigns \result \from n; */
+unsigned int fibonacci (unsigned int n) {
+ if (n < 2)
+ return n;
+ else {
+ unsigned int x = fibonacci(n-1);
+ unsigned int y = fibonacci(n-2);
+ return x + y;
+ }
+}
+
+/* ----- Recursive functions using pointers on the stack. ------------------ */
+
+/*@ assigns *result \from *p;
+ ensures \initialized(result);
+ ensures *result == (*p * (*p+1)) / 2; */
+void sum_ptr (unsigned int *p, unsigned int *result) {
+ if (*p < 2)
+ *result = *p;
+ else {
+ unsigned int res;
+ unsigned int arg = *p - 1;
+ sum_ptr(&arg, &res);
+ *result = *p + res;
+ }
+}
+
+/*@ assigns *result \from *p; */
+void factorial_ptr(unsigned int *p, unsigned int *result) {
+ if(*p < 2) {
+ *result = 1;
+ }
+ else {
+ unsigned int res;
+ unsigned int arg = *p - 1;
+ factorial_ptr(&arg, &res);
+ *result = *p * res;
+ }
+}
+
+/*@ assigns *result \from n, *p; */
+void syracuse_ptr (unsigned int n, unsigned int *p, unsigned int *result) {
+ if (*p == 0)
+ *result = n;
+ else {
+ unsigned int prev_res;
+ unsigned int prev_arg = *p - 1;
+ syracuse_ptr(n, &prev_arg, &prev_res);
+ if (prev_res % 2)
+ *result = 3*prev_res + 1;
+ else
+ *result = prev_res / 2;
+ }
+}
+
+/*@ assigns *result \from *p; */
+void fibonacci_ptr (unsigned int *p, unsigned int *result) {
+ if (*p < 2)
+ *result = *p;
+ else {
+ unsigned int x, y;
+ unsigned int a = *p;
+ a--;
+ fibonacci_ptr(&a, &x);
+ a--;
+ fibonacci_ptr(&a, &y);
+ *result = x + y;
+ }
+}
+
+/* ----- Recursive functions performing several computations at once. ------- */
+
+/*@ assigns \result \from i;
+ assigns *sum \from i;
+ ensures \initialized(sum);
+ ensures *sum == (i * (i+1)) / 2; */
+unsigned int sum_and_fact (unsigned int i, unsigned int *sum) {
+ if (i < 2) {
+ *sum = i;
+ return i;
+ }
+ else {
+ unsigned int tmp;
+ unsigned int fact = i * sum_and_fact(i-1, &tmp);
+ *sum = i + tmp;
+ return fact;
+ }
+}
+
+/* ----- Mutually recursive functions. -------------------------------------- */
+
+int even (unsigned int);
+void even_ptr (unsigned int, int*);
+
+/*@ assigns \result \from n;
+ ensures \result == n % 2; */
+int odd (unsigned int n) {
+ if (n)
+ return even(n-1);
+ else
+ return 0;
+}
+
+/*@ assigns \result \from n;
+ ensures \result == !(n % 2); */
+int even (unsigned int n) {
+ if (n)
+ return odd(n-1);
+ else
+ return 1;
+}
+
+/*@ assigns *result \from n;
+ ensures *result == n % 2; */
+void odd_ptr (unsigned int n, int *result) {
+ if (n) {
+ int x;
+ even_ptr(n-1, &x);
+ *result = x;
+ }
+ else
+ *result = 0;
+}
+
+/*@ assigns *result \from n;
+ ensures *result == !(n % 2); */
+void even_ptr (unsigned int n, int *result) {
+ if (n) {
+ int y;
+ odd_ptr(n-1, &y);
+ *result = y;
+ }
+ else
+ *result = 1;
+}
+
+/* ----- Recursive functions on arrays. ------------------------------------- */
+
+/*@ requires \valid(&data[start..end]);
+ assigns data[start..end] \from start;
+ ensures \initialized(&data[start..end]); */
+void fill_array (int *data, int start, int end) {
+ if (start < 0 || start > end)
+ return;
+ else {
+ data[start] = start;
+ fill_array(data, start + 1, end);
+ }
+}
+
+/*@ requires \valid_read(&data[start..end]);
+ requires \initialized(&data[start..end]);
+ assigns \result \from data[start..end], toFind; */
+int binary_search (int *data, int toFind, int start, int end) {
+ int mid = start + (end - start)/2;
+ if (start > end)
+ return -1;
+ else if (data[mid] == toFind)
+ return mid;
+ else if (data[mid] > toFind)
+ return binary_search(data, toFind, start, mid-1);
+ else
+ return binary_search(data, toFind, mid+1, end);
+}
+
+void test_array () {
+ int array[16], i, j, end;
+ if (nondet) {
+ fill_array(array, 0, 16);
+ Frama_C_show_each_unreachable(array);
+ }
+ end = Frama_C_interval(10, 16);
+ fill_array(array, 0, end);
+
+ i = binary_search(array, 3, 0, 15);
+ Frama_C_show_each_3(i);
+ i = binary_search(array, 12, 0, 15);
+ Frama_C_show_each_12(i);
+ i = binary_search(array, 20, 0, 15);
+ Frama_C_show_each_minus1(i);
+
+ fill_array(array, 10, 15);
+ j = Frama_C_interval(7, 11);
+ i = binary_search(array, j, 0, 15);
+ Frama_C_show_each_7_11(i);
+ j = Frama_C_interval(7, 18);
+ i = binary_search(array, j, 0, 15);
+ Frama_C_show_each_minus_1_15(i);
+}
+
+/* ----- Alarms or invalid preconditions in recursive calls. ---------------- */
+
+/*@ assigns \result \from i;
+ ensures \result > 0; */
+int alarm (int i) {
+ if(i <= 1) {
+ return 1;
+ }
+ int res = i * alarm(i - 1); // alarm if enough recursive calls are made.
+ return res;
+}
+
+/* The precondition should become invalid if enough recursive calls are made. */
+/*@ requires x != 16; */
+void precond (int x) {
+ int y = 100 / (x - 16);
+ if (nondet)
+ precond(x+1);
+}
+
+/* ----- Variables escaping scope through recursive function. --------------- */
+
+int *p;
+
+/*@ assigns p \from \nothing;
+ assigns *p \from \nothing; */
+void escaping_local (int count) {
+ if (count <= 0)
+ return;
+ else {
+ int x;
+ p = &x;
+ escaping_local(count - 1);
+ if (nondet) {
+ *p = 17; // invalid, except the penultimate recursive call where count = 1
+ Frama_C_show_each_1(count);
+ }
+ }
+}
+
+/*@ assigns p \from \nothing;
+ assigns *p \from \nothing; */
+void escaping_formal (int count, int x) {
+ if (count <= 0)
+ return;
+ else {
+ p = &x;
+ escaping_formal(count - 1, x);
+ if (nondet) {
+ *p = 16; // invalid, except the penultimate recursive call where count = 1
+ Frama_C_show_each_1(count);
+ }
+ }
+}
+
+/*@ assigns p \from q;
+ assigns *p \from \nothing; */
+void escaping_stack (int count, int *q) {
+ if (count <= 0)
+ return;
+ else {
+ int x;
+ p = q;
+ escaping_stack(count - 1, &x);
+ if (nondet) {
+ *p = 15;
+ Frama_C_show_each_1_2(count);
+ }
+ }
+}
+
+/* ----- Bug with memexec. -------------------------------------------------- */
+
+/*@ assigns \nothing; */
+void decr (int i) {
+ if (nondet)
+ return;
+ else {
+ int x = 100 / i; // alarm if i = 0.
+ decr(i-1);
+ }
+}
+
+void bug_memexec () {
+ decr(25);
+ /* Should trigger the alarm with -eva-unroll-recursive-calls 20, except that
+ the memexec cache use the results of the previous call to not reinterpret
+ the call. */
+ decr(15);
+}
+
+/* ----- Main. -------------------------------------------------------------- */
+
+void main () {
+ int a, b;
+ unsigned int x, y;
+ /* Simple recursive functions. */
+ a = five();
+ Frama_C_show_each_5(a);
+ y = sum(13);
+ Frama_C_show_each_91(y);
+ y = factorial(5);
+ Frama_C_show_each_120(y);
+ y = syracuse(12, 9);
+ Frama_C_show_each_1(y);
+ y = fibonacci(11);
+ Frama_C_show_each_89(y);
+
+ /* Recursive functions using pointers on the stack. */
+ x = 13;
+ sum_ptr(&x, &y);
+ Frama_C_show_each_91(y);
+ x = 5;
+ factorial_ptr(&x, &y);
+ Frama_C_show_each_120(y);
+ x = 9;
+ syracuse_ptr(12, &x, &y);
+ Frama_C_show_each_1(y);
+ x = 11;
+ fibonacci_ptr(&x, &y);
+ Frama_C_show_each_89(y);
+
+ /* Recursive functions performing several computations at once. */
+ y = sum_and_fact(8, &x);
+ Frama_C_show_each_36_40320(x, y);
+
+ /* Mutually recursive functions. */
+ a = odd(7);
+ b = even(8);
+ Frama_C_show_each_1(a, b);
+ a = odd(8);
+ b = even(9);
+ Frama_C_show_each_0(a, b);
+ odd_ptr(7, &a);
+ even_ptr(8, &b);
+ Frama_C_show_each_1(a, b);
+ odd_ptr(8, &a);
+ even_ptr(9, &b);
+ Frama_C_show_each_0(a, b);
+
+ /* Using intervals. */
+
+ x = Frama_C_interval(3, 11);
+ y = sum(x);
+ Frama_C_show_each_6_66(y);
+ y = 0;
+ sum_ptr(&x, &y);
+ Frama_C_show_each_6_66(y);
+ y = 0;
+ y = fibonacci(x);
+ Frama_C_show_each_2_89(y);
+ y = 0;
+ fibonacci_ptr(&x, &y);
+ Frama_C_show_each_2_89(y);
+
+ /* Misc */
+ test_array();
+
+ x = Frama_C_interval(10, 20);
+ y = alarm(x);
+ if (nondet) {
+ y = alarm(20);
+ Frama_C_show_each_unreachable(y);
+ }
+ precond(1);
+
+ escaping_local(5);
+ escaping_formal(5, 5);
+ escaping_stack(5, &a);
+
+ bug_memexec();
+}
+
+/* ----- Recursive function without specification. -------------------------- */
+
+unsigned int sum_nospec (unsigned int i) {
+ if (i < 2)
+ return i;
+ unsigned int res = i + sum_nospec(i - 1);
+ return res;
+}
+
+void main_fail () {
+ int x, y;
+ y = sum_nospec(4);
+ Frama_C_show_each_10(y);
+ /* This call don't fail, as only 4 unrolling of [sum_nospec] are needed before
+ using the results from the first call stored in the memexec cache. However,
+ this call would fail without the first call to [sum_no_spec]. */
+ y = sum_nospec(8);
+ Frama_C_show_each_36(y);
+ x = Frama_C_interval(4, 16);
+ /* This call cannot be interpreted without a specification for [sum_nospec]. */
+ y = sum_nospec(x);
+ Frama_C_show_each_unreachable(y);
+}
diff --git a/tests/value/recursion.i b/tests/value/recursion.i
deleted file mode 100644
index c3670163290ec5e0d912bff2106bc72a63fc1466..0000000000000000000000000000000000000000
--- a/tests/value/recursion.i
+++ /dev/null
@@ -1,78 +0,0 @@
-/* run.config*
- EXIT: 1
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -journal-disable
- OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -eva-ignore-recursive-calls -journal-disable
- */
-int G;
-
-int ff() {
- if (G) ff();
- return 5;
-}
-
-int x;
-
-volatile int c;
-
-struct s {
- int f1;
- int f2;
-} s;
-
-// Use given assigns
-/*@ assigns x \from x, y;
- assigns s.f1 \from s.f2;
- assigns \result \from s;
-*/
-struct s f(int y) {
- x = 2+y;
- Frama_C_show_each(x, y);
- if (c) {
- s = f(y);
- Frama_C_show_each(x, y);
- }
- s.f1 = s.f2;
- return s;
-}
-
-// Infers assigns \nothing
-void g() {
- g();
-}
-
-// Infer assigns clause that overwrite *p1 and *p2. Currently unsound
-void h(int *p1, int *p2) {
- h(p1, p2);
-}
-
-
-int *pg;
-
-/* &i escapes. The precondition is true on all calls, but could be computed
- false if one overwrites the value of i naively at each call. Currently unsound */
-/*@ requires stage > 0 ==> *pg == i-5;
- assigns *pg \from \nothing;
- ensures stage > 0 ==> *pg == 8;
-*/
-void escaping_formal(int stage, int i) {
- pg = &i;
- Frama_C_show_each (pg, *pg, stage, i);
- escaping_formal (1, i+5);
- if (stage > 0)
- *pg = 8;
- Frama_C_show_each (pg, *pg, stage, i);
- pg = 0;
-}
-
-int main() {
- G = ff();
- g();
- int v1, v2;
- h(&v1, &v2);
- Frama_C_show_each(v1, v2);
- escaping_formal(0, 10);
- struct s r = f(0);
- Frama_C_show_each(x);
- return r.f1+1;
-}
-
diff --git a/tests/value/recursion2.i b/tests/value/recursion2.i
deleted file mode 100644
index ec3ea022c9c7e35712cf0f8b466c78c91b7ceace..0000000000000000000000000000000000000000
--- a/tests/value/recursion2.i
+++ /dev/null
@@ -1,23 +0,0 @@
-/*run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva @EVA_CONFIG@ -journal-disable -then -input -out -inout
- */
-int x, y;
-
-void h2 (int);
-void h1 (int);
-
-void h1 (int i) {
- int r = x;
- if (i)
- h2 (i);
-}
-void h2 (int j) {
- int q = y;
- if (!j)
- h1 (j);
-}
-
-void main() {
- h2(0);
- h1(1);
-}