diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
index 046a6a7f967f4de51161c85675714c523fe96060..888e5f6719ee01a513e3c06aaa09b8e30ed6c5bd 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
@@ -3,7 +3,6 @@
[eva:alarm] tests/arith/quantif.i:15: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/quantif.i:15: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:20: Warning: assertion got status unknown.
[eva:alarm] tests/arith/quantif.i:24: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/quantif.i:24: Warning: assertion got status unknown.
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 5de658b98e54d52516fc62bf0f3e08d402e3bda4..2ae8f263be7c99c80cac23faa1cc354cbbb240ed 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -300,14 +300,6 @@ let env_only_here state = {
contracts *);
}
-(* Return the base and the type corresponding to the logic var if it is within
- the scope of the supported ones. Fail otherwise. *)
-let c_logic_var lvi =
- match Logic_utils.unroll_type lvi.lv_type with
- | Ctype ty when Cil.isIntegralType ty ->
- (Base.of_c_logic_var lvi), ty
- | _ -> unsupported_lvar lvi
-
let top_float =
let neg_infinity = Fval.F.of_float neg_infinity
and pos_infinity = Fval.F.of_float infinity in
@@ -322,26 +314,46 @@ let bind_logic_vars env lvs =
match Logic_utils.unroll_type lv.lv_type with
| Linteger -> bind_logic_var Ival.top
| Lreal -> bind_logic_var top_float
- | _ ->
- try
- let b, cty = c_logic_var lv in
- let size = Int.of_int (Cil.bitsSizeOf cty) in
- let v = Cvalue.V_Or_Uninitialized.initialized V.top_int in
- let state = Model.add_base_value b ~size v ~size_v:Int.one state in
- state, logic_vars
- with Cil.SizeOfError _ -> unsupported_lvar lv
+ | Ctype ctyp when Cil.isIntegralType ctyp ->
+ let base = Base.of_c_logic_var lv in
+ let size = Int.of_int (Cil.bitsSizeOf ctyp) in
+ let v = Cvalue.V_Or_Uninitialized.initialized V.top_int in
+ let state = Model.add_base_value base ~size v ~size_v:Int.one state in
+ state, logic_vars
+ | _ -> unsupported_lvar lv
in
let state = env_current_state env in
let state, logic_vars = List.fold_left bind_one (state, env.logic_vars) lvs in
overwrite_current_state { env with logic_vars } state
+let copy_logic_vars ~src ~dst lvars =
+ let copy_one env lvar =
+ match Logic_utils.unroll_type lvar.lv_type with
+ | Linteger | Lreal ->
+ let value = LogicVarEnv.find lvar src.logic_vars in
+ let logic_vars = LogicVarEnv.add lvar value env.logic_vars in
+ { env with logic_vars }
+ | Ctype _ ->
+ begin
+ let base = Base.of_c_logic_var lvar in
+ match Model.find_base base (env_current_state src) with
+ | `Bottom | `Top -> env
+ | `Value offsm ->
+ let state = Model.add_base base offsm (env_current_state env) in
+ overwrite_current_state env state
+ end
+ | _ -> unsupported_lvar lvar
+ in
+ List.fold_left copy_one dst lvars
+
let unbind_logic_vars env lvs =
let unbind_one (state, logic_vars) lv =
match Logic_utils.unroll_type lv.lv_type with
| Linteger | Lreal -> state, LogicVarEnv.remove lv logic_vars
- | _ ->
- let b, _ = c_logic_var lv in
- Model.remove_base b state, logic_vars
+ | Ctype _ ->
+ let base = Base.of_c_logic_var lv in
+ Model.remove_base base state, logic_vars
+ | _ -> unsupported_lvar lv
in
let state = env_current_state env in
let state, logic_vars = List.fold_left unbind_one (state, env.logic_vars) lvs in
@@ -1158,9 +1170,15 @@ and eval_binop ~alarm_mode env op t1 t2 =
and eval_tlhost ~alarm_mode env lv =
match lv with
- | TVar { lv_origin = Some v } ->
- let loc = Location_Bits.inject (Base.of_varinfo v) Ival.zero in
- { etype = v.vtype;
+ | TVar lvar ->
+ let base, typ =
+ match lvar.lv_origin, Logic_utils.unroll_type lvar.lv_type with
+ | Some v, _ -> Base.of_varinfo v, v.vtype
+ | None, Ctype typ -> Base.of_c_logic_var lvar, typ
+ | _ -> unsupported_lvar lvar
+ in
+ let loc = Location_Bits.inject base Ival.zero in
+ { etype = typ;
ldeps = empty_logic_deps;
eover = loc;
eunder = under_loc_from_over loc;
@@ -1174,14 +1192,6 @@ and eval_tlhost ~alarm_mode env lv =
eunder = loc; eover = loc;
empty = false; }
| None -> no_result ())
- | TVar ({ lv_origin = None } as tlv) ->
- let b, ty = c_logic_var tlv in
- let loc = Location_Bits.inject b Ival.zero in
- { etype = ty;
- ldeps = empty_logic_deps;
- eover = loc;
- eunder = under_loc_from_over loc;
- empty = false; }
| TMem t ->
let r = eval_term ~alarm_mode env t in
let tres = match Cil.unrollType r.etype with
@@ -2417,14 +2427,32 @@ and eval_predicate env pred =
| Pforall (varl, p') | Pexists (varl, p') ->
begin
- try
- let env = bind_logic_vars env varl in
- let r = do_eval env p' in
- match p.pred_content with
- | Pexists _ -> if r = False then False else Unknown
- | Pforall _ -> if r = True then True else Unknown
- | _ -> assert false
- with LogicEvalError _ee -> Unknown (* No error display? *)
+ (* If [p'] is true (or false) for all possible values of [varl],
+ then so is Pforall(varl, p') and Pexists(varl, p'). *)
+ let env = bind_logic_vars env varl in
+ let r = do_eval env p' in
+ if r <> Unknown then r else
+ (* Otherwise:
+ - if [p'] evaluates to [false] for at least some values of [varl],
+ then Pforall (varl, p') is false.
+ - if [p'] evaluates to [true] for at least some values of [varl],
+ then Pexists (varl, p') is true.
+
+ In order to find such values, we reduce the environment by assuming
+ [p'] is true (for Pexists) or false (for Pforall), and then we
+ reevaluate [p'] with these values. *)
+ let positive =
+ match p.pred_content with Pforall _ -> false | _ -> true
+ in
+ let reduced_env = reduce_by_predicate ~alarm_mode env positive p' in
+ (* Reduce the values of logical variables [varl] in [env] according to
+ [reduced_env]. To be more precise, we could reduce them to
+ singleton values — for instance by using the interval bounds. *)
+ let env = copy_logic_vars ~src:reduced_env ~dst:env varl in
+ match p.pred_content, do_eval env p' with
+ | Pexists _, True -> True
+ | Pforall _, False -> False
+ | _ -> Unknown
end
| Pnot p -> begin match do_eval env p with
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index 21fd920919affc8afd1710f3d43042b975c924b3..770361f547028d044dea20eeb4bd77a6108ac9bb 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -23,6 +23,8 @@
[eva] tests/builtins/strchr.c:88: Call to builtin strchr
[eva] tests/builtins/strchr.c:88:
function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva] tests/builtins/strchr.c:88: Frama_C_show_each_mystrchr: {3}
[eva] tests/builtins/strchr.c:89: assertion got status valid.
[eva] tests/builtins/strchr.c:92: Call to builtin strchr
diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index fc9107a81028a0d522e0ae1ecb02cfdafa64c96b..e39d01ba5bf5415cbb065c34c0e0af0a79d49307 100644
--- a/tests/libc/oracle/stdlib_c_env.res.oracle
+++ b/tests/libc/oracle/stdlib_c_env.res.oracle
@@ -9,6 +9,8 @@
[eva] share/libc/stdlib.c:114: Call to builtin strchr
[eva] share/libc/stdlib.c:114:
function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva] share/libc/stdlib.c:115:
assertion 'string_contains_separator' got status valid.
[eva] share/libc/stdlib.c:116: assertion 'name_is_not_empty' got status valid.
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 033c83c6b476d861790f1c98a4074809e81bc6e2..401829973b44023601fe892716db53d08870ea00 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -668,6 +668,8 @@
function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] share/libc/string.h:164:
function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva:alarm] share/libc/string.h:165: Warning:
function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] share/libc/string.h:171:
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index d2f546a60acf81596b0b9778e9f97cfd59ddedba..4e1e5145535fa6ef9dd6ed43f042e6125df52320 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -288,6 +288,8 @@
function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] share/libc/string.h:164:
function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva:alarm] share/libc/string.h:165: Warning:
function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] share/libc/string.h:171:
diff --git a/tests/libc/oracle/string_c_strchr.res.oracle b/tests/libc/oracle/string_c_strchr.res.oracle
index 965af4a3862fe7990d7ca5c2fa9ece0a8c3fc0f8..d389a3cf5615c82c1b364e246fbcfeded5ef7fca 100644
--- a/tests/libc/oracle/string_c_strchr.res.oracle
+++ b/tests/libc/oracle/string_c_strchr.res.oracle
@@ -67,6 +67,8 @@
function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] share/libc/string.h:164:
function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva:alarm] share/libc/string.h:165: Warning:
function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] Recording results for strchr
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 5e1e94a0719c6c96067d3788889d10788b9d8c45..fd2eaee19bf54f636ccc83358a1c4dc259534597 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -143,12 +143,8 @@
[eva] tests/libc/string_h.c:75:
function strtok: precondition 'valid_string_delim' got status valid.
[eva:alarm] tests/libc/string_h.c:75: Warning:
- function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:75:
- Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+ function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
[eva] Done for function strtok
-[eva:alarm] tests/libc/string_h.c:76: Warning:
- assertion 'unreachable_if_precise' got status invalid (stopping propagation).
[eva] Recording results for test_strtok
[eva] Done for function test_strtok
[eva] computing for function test_strtok_r <- main.
@@ -232,12 +228,8 @@
[eva] tests/libc/string_h.c:105:
function strtok_r: precondition 'valid_saveptr' got status valid.
[eva:alarm] tests/libc/string_h.c:105: Warning:
- function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:105:
- Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+ function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
[eva] Done for function strtok_r
-[eva:alarm] tests/libc/string_h.c:106: Warning:
- assertion 'unreachable_if_precise' got status invalid (stopping propagation).
[eva] Recording results for test_strtok_r
[eva] Done for function test_strtok_r
[eva] computing for function strdup <- main.
@@ -333,6 +325,8 @@
[eva] tests/libc/string_h.c:154: Call to builtin strchr
[eva] tests/libc/string_h.c:154:
function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165:
+ cannot evaluate ACSL term, unsupported logic var p
[eva] computing for function strchrnul <- main.
Called from tests/libc/string_h.c:155.
[eva] using specification for function strchrnul
diff --git a/tests/value/oracle/annot_valid.res.oracle b/tests/value/oracle/annot_valid.res.oracle
index 88f57174bb9ee088a5e1aff1fccb060ef9e86128..557e8ca2b58d364e59f43e41c027e413c56505f4 100644
--- a/tests/value/oracle/annot_valid.res.oracle
+++ b/tests/value/oracle/annot_valid.res.oracle
@@ -17,7 +17,7 @@
[eva:alarm] tests/value/annot_valid.i:29: Warning: assertion got status unknown.
[eva:alarm] tests/value/annot_valid.i:32: Warning: assertion got status unknown.
[eva:alarm] tests/value/annot_valid.i:35: Warning: assertion got status unknown.
-[eva:alarm] tests/value/annot_valid.i:38: Warning: assertion got status unknown.
+[eva] tests/value/annot_valid.i:38: assertion got status valid.
[eva] tests/value/annot_valid.i:41: assertion got status valid.
[eva:alarm] tests/value/annot_valid.i:44: Warning:
assertion got status invalid (stopping propagation).