diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index f2dc9ff30e5586e3f4e7d7eb7ed713781fe82655..b512325ade4b44e3cc3eecf4700c20f1de57a9e3 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -186,7 +186,7 @@ module type Transfer = sig
(** [update valuation t] updates the state [t] by the values of expressions
and the locations of lvalues stored in [valuation]. *)
- val update : valuation -> state -> state
+ val update : valuation -> state -> state or_bottom
(** [assign kinstr lv expr v valuation state] is the transfer function for the
assignment [lv = expr] for [state]. It must return the state where the
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ok.ml
index 27aa29d81c1fb68e1a7fccaddc91b732dd74962b..e69f47ab8625886339479d8da73957603665d6aa 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ok.ml
@@ -451,11 +451,7 @@ module Make
let array = Tcons1.array_make env (List.length constraints) in
List.iteri (fun i c -> Tcons1.array_set array i c) constraints;
let st = Abstract1.meet_tcons_array man state array in
- if debug && Abstract1.is_bottom man st then
- Value_parameters.result ~current:true ~once:true
- "Bottom with state %a and constraints %a@."
- Abstract1.print state (fun fmt a -> Tcons1.array_print fmt a) array;
- st
+ if Abstract1.is_bottom man st then `Bottom else `Value st
let _constraint_to_typ env state vars =
let aux (var_apron, vi) =
@@ -615,11 +611,11 @@ module Make
in
let constraints = Valuation.fold gather_constraints valuation [] in
if constraints = []
- then state
+ then `Value state
else meet_with_constraints env state constraints
let assign _stmt lvalue expr _value valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
try
let state =
try
@@ -642,7 +638,7 @@ module Make
let assume _stmt exp bool valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
try
let env = Abstract1.env state in
let eval = make_eval state in
@@ -656,7 +652,7 @@ module Make
| Out_of_Scope _ -> `Value state
let start_call _stmt call valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
let eval = make_eval state in
let oracle = make_oracle valuation in
let process_argument (vars, acc) arg =
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 798c4ea72f7d652d2d5a98d80780ce0f814e5619..995298130d6c76007449e4477f00dbb2b82b3439 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -227,7 +227,7 @@ module State = struct
module T = Cvalue_transfer.Transfer (Valuation)
- let update valuation (s, clob) = T.update valuation s, clob
+ let update valuation (s, clob) = T.update valuation s >>-: fun s -> s, clob
let assign stmt lv expr assigned valuation (s, clob) =
T.assign stmt lv expr assigned valuation s >>-: fun s ->
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index a53f6cf775e0fd80581d1887435b1336fc636403..1e9065ac7f380b65e6abef117e52574c604680aa 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -90,11 +90,7 @@ module Transfer
else t
| _ -> t
in
- let s = Valuation.fold process valuation t in
- s
-
- let assume _stmt _expr _positive valuation state = `Value (update valuation state)
-
+ Valuation.fold process valuation t
(* ---------------------------------------------------------------------- *)
(* Assignments *)
@@ -246,4 +242,10 @@ module Transfer
let typ = Cil.typeOf expr in
Eval_op.pretty_offsetmap typ fmt offsm
| _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
+
+
+ (* ----------------- Export assumption functions -------------------------- *)
+
+ let update valuation state = `Value (update valuation state)
+ let assume _stmt _expr _positive = update
end
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 108c1c4eada23618cd0484c2038734e547a3503d..b27b01329e10386ad60dee893ca52c897b1d10a5 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -79,7 +79,7 @@ module Make_Minimal
and type loc = location)
= struct
- let update _valuation state = state
+ let update _valuation state = `Value state
let assign kinstr lv expr _value _valuation state =
Domain.assign kinstr lv.Eval.lval expr state
@@ -227,7 +227,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let record valuation = { find = find valuation;
find_loc = find_loc valuation; }
- let update _valuation state = state
+ let update _valuation state = `Value state
let assign kinstr lv expr value valuation state =
Domain.assign kinstr lv expr value (record valuation) state
let assume stmt expr positive valuation state =
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 35ada8461ccc5a2169f4c2a5be3ccbb3bfb8e483..fffc784d6c8ec628b931a200e587caf909a8c86c 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -161,8 +161,9 @@ module Make
module Right_Transfer = Right.Transfer (Right_Valuation)
let update valuation (left, right) =
- Left_Transfer.update valuation left,
- Right_Transfer.update valuation right
+ Left_Transfer.update valuation left >>- fun left ->
+ Right_Transfer.update valuation right >>-: fun right ->
+ left, right
let assign stmt lv expr value valuation (left, right) =
Left_Transfer.assign stmt lv expr value valuation left >>- fun left ->
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 69f1c355b3a96660e6ca6536cfd66394270db1d8..7ccb02c97211ab9dfbf100b5cf16abd9c45358d0 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -338,7 +338,7 @@ module Make
let deps = HCESet.fold (add_one_dep valuation) lvalues.read deps in
HCESet.fold (add_one_dep valuation) lvalues.addr deps
- let update _valuation state = state
+ let update _valuation state = `Value state
let is_singleton = match get_cvalue with
| None -> fun _ -> false
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 11b85c2cbe735c3b9ecbf283b83f25d2cc1f3860..1af3127519259cc44ffd7db880c28f39dc8983da 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1174,27 +1174,6 @@ module D_Impl : Abstract_domain.S_with_Structure
and type valuation := Valuation.t
= struct
- let update _valuation st = st (* TODO? *)
-
- exception Unassignable
-
- let assign _kinstr lv e _assignment valuation (state:state) =
- let to_loc lv =
- match Valuation.find_loc valuation lv with
- | `Value r -> Precise_locs.imprecise_location r.loc
- | `Top -> raise Unassignable
- in
- let to_val e =
- match Valuation.find valuation e with
- | `Top -> raise Unassignable
- | `Value v ->
- match v.value.initialized, v.value.escaping, v.value.v with
- | true, false, `Value v -> v
- | _ -> raise Unassignable
- in
- try `Value (G.assign to_loc to_val lv.lval e state)
- with Unassignable -> `Value (kill lv.lloc state)
-
let assume_exp valuation e r state =
if r.reductness = Created || r.reductness = Reduced then
match e.enode with
@@ -1220,10 +1199,32 @@ module D_Impl : Abstract_domain.S_with_Structure
let assume_exp_bot valuation e r state =
state >>- assume_exp valuation e r
- let assume _ _ _ valuation state =
+ let update valuation state =
let assume_one = assume_exp_bot valuation in
Valuation.fold assume_one valuation (`Value state)
+ let assume _ _ _ = update
+
+ exception Unassignable
+
+ let assign _kinstr lv e _assignment valuation (state:state) =
+ update valuation state >>- fun state ->
+ let to_loc lv =
+ match Valuation.find_loc valuation lv with
+ | `Value r -> Precise_locs.imprecise_location r.loc
+ | `Top -> raise Unassignable
+ in
+ let to_val e =
+ match Valuation.find valuation e with
+ | `Top -> raise Unassignable
+ | `Value v ->
+ match v.value.initialized, v.value.escaping, v.value.v with
+ | true, false, `Value v -> v
+ | _ -> raise Unassignable
+ in
+ 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 state =
match function_calls_handling with
@@ -1238,8 +1239,9 @@ module D_Impl : Abstract_domain.S_with_Structure
match function_calls_handling with
| FullInterprocedural -> update valuation state
| IntraproceduralAll
- | IntraproceduralNonReferenced -> G.empty
+ | IntraproceduralNonReferenced -> `Value G.empty
in
+ state >>- fun state ->
(* track [arg.formal] into [state]. Important for functions that
receive a size as argument. *)
let aux_arg state arg =
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index bd2e643f14d79c980524840433d49f992389d28d..12ba3cd152852bbd7ea98e40b0921ae2110bc5a6 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -264,7 +264,7 @@ module Internal
let finalize_call _stmt _call ~pre ~post =
`Value (Transfer.catenate pre post)
- let update _valuation state = state
+ let update _valuation state = `Value state
let show_expr _valuation _state _fmt _expr = ()
end
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index c2653e2de79aad95f7cc5d6d6b5d7fbf056deb03..9eb0b4ef308f90e6784e51eadbe4c34fbb872642 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -129,7 +129,7 @@ module Internal : Domain_builder.InputDomain
and type valuation := Valuation.t
= struct
- let update _valuation st = st (* TODO? *)
+ let update _valuation st = `Value st (* TODO? *)
let kill loc state =
Memory.add_binding ~exact:true state loc V_Or_Uninitialized.top
@@ -171,7 +171,7 @@ module Internal : Domain_builder.InputDomain
let finalize_call _stmt _call ~pre:_ ~post = `Value post
- let start_call _stmt _call valuation state = `Value (update valuation state)
+ let start_call _stmt _call valuation state = update valuation state
let show_expr _valuation _state _fmt _expr = ()
end
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 4f27194587e18fcd830ddd0b26d8612385048a5e..f312b589f11a835903ac4080566ce7f14b81df3a 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -247,25 +247,26 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
(* This function fills [state] according to the information available
in [valuation]. This information is computed by Eva's engine for
all the expressions involved in the current statement. *)
- let update valuation state =
+ let assume_valuation valuation state =
Valuation.fold (assume_exp valuation) valuation state
(* Abstraction of an assignment. *)
let assign _kinstr lv _expr value valuation state =
(* Update the state with the information obtained from evaluating
[lv] and [e] *)
- let state = update valuation state in
+ let state = assume_valuation valuation state in
(* Extract the abstract value *)
let value = Eval.value_assigned value in
(* Store the information [lv = e;] in the state *)
let state = bind_loc lv.lloc lv.ltyp value state in
`Value state
+ let update valuation state = `Value (assume_valuation valuation state)
+
(* Abstraction of a conditional. All information inferred by the engine
is present in the valuation, and must be stored in the memory
abstraction of the domain itself. *)
- let assume _stmt _expr _pos valuation state =
- `Value (update valuation state)
+ let assume _stmt _expr _pos = update
let start_call _stmt call _valuation state =
let bind_argument state argument =
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 952cf517636e04216c67d41e5f55e7d0dbc11d26..42db4cd7cb58a9c6b6cd3cd75b24f28ab2bd0149 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -540,7 +540,7 @@ module Internal : Domain_builder.InputDomain
state
| _ -> state
in
- Valuation.fold aux valuation state
+ `Value (Valuation.fold aux valuation state)
let store_value valuation lv loc state v =
let loc = Precise_locs.imprecise_location loc in
@@ -568,14 +568,14 @@ module Internal : Domain_builder.InputDomain
(* perform [lv = e] in [state] *)
let assign _kinstr lv _e v valuation state =
- let state = update valuation state in
+ update valuation state >>- fun state ->
match v with
| Copy (_, vc) -> store_copy valuation lv lv.lloc state vc
| Assign v -> store_value valuation lv.lval lv.lloc state v
- let assume _stmt _exp _pos valuation state = `Value (update valuation state)
+ let assume _stmt _exp _pos valuation state = update valuation state
- let start_call _stmt _call valuation state = `Value (update valuation state)
+ let start_call _stmt _call valuation state = update valuation state
let finalize_call _stmt _call ~pre:_ ~post = `Value post
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 62aba6028cf854463f08c4ed2e6e2d6b6a308070..4bb14526c7b277ba0348fd36954e862c6d997ab4 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -66,7 +66,7 @@ module Make
and type loc = location)
= struct
- let update _ _ = ()
+ let update _ _ = `Value ()
let assign _ _ _ _ _ _ = `Value ()
let assume _ _ _ _ _ = `Value ()
let start_call _ _ _ _ = `Value ()
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 2a2ac4ca72bba20f9bb343495dacf900ba5c5799..d3edae41ba28d7ebd2c59a6192d96cef00a5cae7 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -412,7 +412,7 @@ module Make
valuation >>- fun valuation ->
Eva.assume ~valuation state argument.concrete post_value
in
- List.fold_left reduce_one_argument valuation reductions >>-: fun valuation ->
+ List.fold_left reduce_one_argument valuation reductions >>- fun valuation ->
TF.update valuation state
(* -------------------- Treat the results of a call ----------------------- *)
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index c3ec4215b3a27fc7e3359de63d965c1d4a964d32..08b9174733a7f6e7d79e466b3f00ca1a63089573 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -191,6 +191,9 @@ let bot_state = function
| `Bottom -> Cvalue.Model.bottom
| `Value s -> s
+let update valuation state =
+ bot_state (Transfer.update valuation state >>-: Cvalue_domain.project)
+
let rec eval_deps state e =
match e.enode with
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ | Const _ ->
@@ -240,7 +243,7 @@ let eval_expr_with_valuation ?with_alarms deps state expr=
match eval with
| `Bottom -> (Cvalue.Model.bottom, deps, Cvalue.V.bottom), None
| `Value (valuation, result) ->
- let state = Cvalue_domain.project (Transfer.update valuation state) in
+ let state = update valuation state in
(state, deps, result), Some valuation
(* Compatibility layer between the old API of eval_exprs and the new evaluation
@@ -274,8 +277,7 @@ module Eval = struct
let eval, _alarms =
Eva.reduce state expr positive
in
- bot_state (eval >>-: fun valuation ->
- Cvalue_domain.project (Transfer.update valuation state))
+ bot_state (eval >>-: fun valuation -> update valuation state)
let lval_to_precise_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index:(_:bool) lval =
@@ -295,8 +297,7 @@ module Eval = struct
notify_opt with_alarms alarms;
match eval with
| `Bottom -> Cvalue.Model.bottom, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
- | `Value (valuation, loc, typ) ->
- Cvalue_domain.project (Transfer.update valuation state), deps, loc, typ
+ | `Value (valuation, loc, typ) -> update valuation state, deps, loc, typ
let lval_to_loc_deps_state ?with_alarms ~deps state ~reduce_valid_index lv =
let state, deps, pl, typ =
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index 99a2a77d76eb36ec86e285bdbb15fcf7486ddd9e..26c5b6d4c45adaf15845328b27805fab45e865c8 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -96,86 +96,104 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
< [eva:alarm] tests/value/gauges.c:158: Warning:
< out of bounds write. assert \valid(tmp);
< (tmp from p--)
-255,258d230
+227,231c203,205
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483646..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+---
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+235c209,210
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+---
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+255,258d229
< [eva:alarm] tests/value/gauges.c:192: Warning:
< out of bounds write. assert \valid(p);
< [eva:alarm] tests/value/gauges.c:193: Warning:
< out of bounds write. assert \valid(q);
-266,271d237
+266,271d236
< [eva:alarm] tests/value/gauges.c:202: Warning:
< out of bounds read. assert \valid_read(tmp);
< (tmp from A++)
< [eva:alarm] tests/value/gauges.c:202: Warning:
< out of bounds read. assert \valid_read(tmp_0);
< (tmp_0 from B++)
-315,318c281
+299,300d263
+< [eva:alarm] tests/value/gauges.c:220: Warning:
+< signed overflow. assert -2147483648 ≤ n - 1;
+315,318c278
< [eva:alarm] tests/value/gauges.c:240: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
< [eva] tests/value/gauges.c:242:
< Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..2147483647]
---
> [eva] tests/value/gauges.c:242: Frama_C_show_each: {47; 48}, {6}
-324,325d286
+324,325d283
< [eva:alarm] tests/value/gauges.c:251: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-327c288
+327c285
< Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..2147483647]
---
> Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, {6; 7}
-333,336c294
+333,336c291
< [eva:alarm] tests/value/gauges.c:263: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
< [eva] tests/value/gauges.c:265:
< Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..2147483647]
---
> [eva] tests/value/gauges.c:265: Frama_C_show_each: {-58; -57}, {9}
-342,343d299
+342,343d296
< [eva:alarm] tests/value/gauges.c:274: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-345c301
+345c298
< Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..2147483647]
---
> Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, {9; 10}
-353,354d308
+353,354d305
< [eva:alarm] tests/value/gauges.c:293: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-356c310
+356c307
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119]
-418a373,376
+418a370,373
> # Gauges domain:
> V: [{[ p -> {{ &x }}
> i -> {1} ]}]
-> s395: λ(0)
-478a437,440
+> s398: λ(0)
+478a434,437
> # Gauges domain:
> V: [{[ i -> {1} ]}]
-> s395: λ([0 .. 1])
+> s398: λ([0 .. 1])
> {[ i -> {1} ]}
-537a500,503
+537a497,500
> # Gauges domain:
> V: [{[ i -> {1} ]}]
-> s395: λ([0 .. 2])
+> s398: λ([0 .. 2])
> {[ i -> {1} ]}
-596a563,566
+596a560,563
> # Gauges domain:
> V: [{[ i -> {1} ]}]
-> s395: λ([0 .. 10])
+> s398: λ([0 .. 10])
> {[ i -> {1} ]}
-661a632,636
+661a629,633
> # Gauges domain:
> V: [{[ p -> {{ &a }}
> i -> {2} ]}]
-> s409: λ(0)
-> s408: λ(0)
-722a698,702
+> s412: λ(0)
+> s411: λ(0)
+722a695,699
> # Gauges domain:
> V: [{[ i -> {2} ]}]
-> s409: λ(0)
-> s408: λ([0 .. 1])
+> s412: λ(0)
+> s411: λ([0 .. 1])
> {[ i -> {0} ]}
-724a705,832
+724a702,829
> [eva] tests/value/gauges.c:325:
> Frama_C_dump_each:
> # Cvalue domain:
@@ -236,8 +254,8 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
> S_1___fc_env[0..1] ∈ [--..--]
> # Gauges domain:
> V: [{[ i -> {2} ]}]
-> s409: λ(0)
-> s408: λ([0 .. 2])
+> s412: λ(0)
+> s411: λ([0 .. 2])
> {[ i -> {0} ]}
> ==END OF DUMP==
> [eva] tests/value/gauges.c:325:
@@ -300,57 +318,75 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
> S_1___fc_env[0..1] ∈ [--..--]
> # Gauges domain:
> V: [{[ i -> {2} ]}]
-> s409: λ(0)
-> s408: λ([0 .. +oo])
+> s412: λ(0)
+> s411: λ([0 .. +oo])
> {[ i -> {0} ]}
> ==END OF DUMP==
-732a841,842
+732a838,839
> [eva] tests/value/gauges.c:343: Call to builtin malloc
> [eva] tests/value/gauges.c:343: Call to builtin malloc
-785,786c895,896
+785,786c892,893
< A ∈ {{ &A + [0..--],0%4 }}
< B ∈ {{ &B + [0..--],0%4 }}
---
> A ∈ {{ &A + [0..36],0%4 }}
> B ∈ {{ &B + [0..36],0%4 }}
-804c914
+798c905
+< n ∈ [-2147483648..99]
+---
+> n ∈ [-2147483547..99]
+804c911
< i ∈ {45; 46; 47; 48; 49; 50; 51}
---
> i ∈ {45; 46; 47; 48}
-810c920
+810c917
< i ∈ {-59; -58; -57; -56; -55; -54; -53}
---
> i ∈ {-58; -57; -56; -55; -54; -53}
-830c940
+830c937
< p ∈ {{ &u + [0..--],0%4 }}
---
> p ∈ {{ &u + [0..400],0%4 }}
-832c942
+832c939
< k ∈ [0..2147483647]
---
> k ∈ [0..390]
-837c947
+837c944
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
-848,849c958,960
+848,849c955,957
< [1..9] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
< p ∈ {{ &y + [4..40],0%4 }}
---
> [1..6] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
> [7..9] ∈ UNINITIALIZED
> p ∈ {{ &y[7] }}
-860c971
+860c968
< p ∈ {{ &T + [--..396],0%4 }}
---
> p ∈ {{ &T + [-4..396],0%4 }}
-995,996c1106,1107
+865,869c973
+< n ∈ {0}
+< arr[0] ∈ {0}
+< [1] ∈ {-1}
+< [2..65535] ∈ [--..--] or UNINITIALIZED
+< p ∈ {{ &arr + [12..--],0%4 }}
+---
+> NON TERMINATING FUNCTION
+972a1077
+> [from] Non-terminating function main8_aux (no dependencies)
+995,996c1100,1101
< p FROM p; A; B; n; p; A[0..9]; B[0..9] (and SELF)
< \result FROM p; A; B; n; p; A[0..9]; B[0..9]
---
> p FROM p; A; B; n; p; A[0..8]; B[0..8] (and SELF)
> \result FROM p; A; B; n; p; A[0..8]; B[0..8]
-1074c1185
+1040c1145
+< NO EFFECTS
+---
+> NON TERMINATING - NO EFFECTS
+1074c1179
< p; A[0..9]; B[0..9]
---
> p; A[0..8]; B[0..8]
@@ -864,6 +900,10 @@ diff tests/value/oracle/reevaluate_alarms.res.oracle tests/value/oracle_gauges/r
< [eva:alarm] tests/value/reevaluate_alarms.i:14: Warning:
< out of bounds write. assert \valid(tmp);
< (tmp from p++)
+59c56
+< p ∈ {{ &T + [0..--],0%4 }}
+---
+> p ∈ {{ &T{[0], [1], [2], [3], [4], [5]} }}
124,125d120
< [ - ] Assertion 'Eva,mem_access' (file tests/value/reevaluate_alarms.i, line 14)
< tried with Eva.
@@ -905,16 +945,22 @@ diff tests/value/oracle/undefined_sequence.0.res.oracle tests/value/oracle_gauge
101a103
> [eva] tests/value/undefined_sequence.i:49: starting to merge loop iterations
diff tests/value/oracle/unroll.res.oracle tests/value/oracle_gauges/unroll.res.oracle
-16a17
+13,14d12
+< [eva:alarm] tests/value/unroll.i:34: Warning:
+< signed overflow. assert -2147483648 ≤ j - 1;
+16a15
> [eva] tests/value/unroll.i:39: starting to merge loop iterations
-26c27
+26c25
< j ∈ [-2147483648..-123]
---
> j ∈ {-238}
diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_gauges/unroll_simple.res.oracle
-11a12
+8,9d7
+< [eva:alarm] tests/value/unroll_simple.i:11: Warning:
+< signed overflow. assert -2147483648 ≤ j - 1;
+11a10
> [eva] tests/value/unroll_simple.i:16: starting to merge loop iterations
-21c22
+21c20
< j ∈ [-2147483648..-126]
---
> j ∈ {-250}
@@ -950,3 +996,8 @@ diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_gau
25a26,27
> [eva] tests/value/widen_on_non_monotonic.i:21: starting to merge loop iterations
> [eva] tests/value/widen_on_non_monotonic.i:18: starting to merge loop iterations
+diff tests/value/oracle/widen_overflow.res.oracle tests/value/oracle_gauges/widen_overflow.res.oracle
+31a32,34
+> [eva] computing for function u <- main.
+> Called from tests/value/widen_overflow.i:9.
+> [eva] Done for function u
diff --git a/tests/value/gauges.c b/tests/value/gauges.c
index cd1619e90e511a5f15dfd714a89486470171026b..ab2963f70b41dbb3f18e2a7915fc2d81a7c0d5d4 100644
--- a/tests/value/gauges.c
+++ b/tests/value/gauges.c
@@ -170,12 +170,12 @@ void main8_aux (unsigned int n) {
int *p = arr;
do {
Frama_C_show_each(n);
- *p++ = n;
+ *p++ = n; // Invalid access memory if more than 65536 iterations.
} while (--n);
}
void main8() {
- main8_aux(0);
+ if (v) main8_aux(0); // This call can legitimately lead to bottom.
}
void main9() {
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 18dd8eea6bdd67932e7fc01d51851c6e6edc9444..fa19ee9d0ef3002d43a7656080239d7a89f6a42b 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -1163,7 +1163,7 @@
[inout] Out (internal) for function main8:
\nothing
[inout] Inputs for function main8:
- \nothing
+ v
[inout] Out (internal) for function main9:
x[0..9]; y[0..9]; p; q; z; i; r
[inout] Inputs for function main9: