diff --git a/Changelog b/Changelog
index 623565a33191e0e7cc2981f02586ebe6513117f2..af982521df4008755c7375baf505f081d9ea2490 100644
--- a/Changelog
+++ b/Changelog
@@ -20,6 +20,8 @@ Open Source Release <next-release>
o! Kernel [2023-09-25] Remove Dynamic.Unloadable exception, useless since
the move from dynamic to static API for plug-ins.
+- Eva [2023-09-26] Support evaluation of simple \let bindings in
+ ACSL terms and predicates.
- Alias [2023-09-07] New alias plugin that implements a points-to
analysis and an alias analysis based on Steensgaard's algorithm.
For these purposes it presents a more efficient (albeit less
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
index dfb2831b7e1fb2c512075fbb37544a05759f0641..be579f0c089d5e145728881ec7f99f776477edb4 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
@@ -104,8 +104,6 @@
[eva:alarm] at_on-purely-logic-variables.c:8: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] at_on-purely-logic-variables.c:8: Warning:
- function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
index 85052dd4ea7316d44413049ff6732f212331098e..c5e891963e67ed9e48b55760010e0f968d7b0652 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
@@ -9,7 +9,6 @@
[eva:alarm] let.c:7: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] let.c:7: Warning: assertion got status unknown.
[eva:alarm] let.c:10: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -19,16 +18,12 @@
[eva:alarm] let.c:9: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] let.c:9: Warning: assertion got status unknown.
-[eva:alarm] let.c:13: Warning: assertion got status unknown.
[eva:alarm] let.c:16: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] let.c:15: Warning: assertion got status unknown.
[eva:alarm] let.c:20: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] let.c:19: Warning: assertion got status unknown.
[eva:alarm] let.c:24: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -40,11 +35,9 @@
\valid(data->values) got status unknown.
[eva:alarm] let.c:24: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] let.c:24: Warning: assertion got status unknown.
[eva:alarm] let.c:27: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] let.c:27: Warning: assertion got status unknown.
[eva:alarm] let.c:30: Warning:
function __e_acsl_assert_register_float: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
index 975e9069daf2c99a92e3c70e6d3ae88b300b9d87..cf11459002f1821c1e89815272a46409efcf8364 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
@@ -76,7 +76,6 @@
[eva:alarm] quantif.i:32: Warning: assertion got status unknown.
[eva:alarm] quantif.i:47: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] quantif.i:54: Warning: assertion got status unknown.
[eva:alarm] quantif.i:63: Warning:
assertion 'forall_multiple_binders_2' got status unknown.
[eva:alarm] quantif.i:66: Warning:
diff --git a/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
index 444a3336dbb7b59bcf72c7399d89669a2fb6845e..5369620ae88c86367b489c9891f32dfdd33a899f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
@@ -63,8 +63,6 @@
\valid(data->values) got status unknown.
[eva:alarm] rationals.c:4: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] rationals.c:4: Warning:
- function __gen_e_acsl_avg: postcondition got status unknown.
[eva:alarm] rationals.c:28: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] rationals.c:28: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
index b4ebb69309d93985fd1365457c92e3c9389af275..f1fe7b2f966ab67583688e66c1953c46f6845304 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
@@ -6,4 +6,3 @@
[eva:alarm] issue69.c:10: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] issue69.c:10: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/printed_data.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/printed_data.res.oracle
index f9589246d101d590ef5796c6a6b6ca0e6620532d..69585cc1635bd49b570fdae6888c54113e4fcf26 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/printed_data.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/printed_data.res.oracle
@@ -1,20 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] printed_data.c:69: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:71: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:73: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:75: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:77: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:79: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:81: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:83: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:85: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:87: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:89: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:91: Warning: assertion got status unknown.
[eva:alarm] printed_data.c:93: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] printed_data.c:93: Warning: assertion got status unknown.
[eva:alarm] printed_data.c:98: Warning: assertion got status unknown.
[eva:alarm] printed_data.c:100: Warning: assertion got status unknown.
[eva] printed_data.c:101: Warning:
@@ -29,7 +16,6 @@
[eva:alarm] printed_data.c:102: Warning: assertion got status unknown.
[eva:alarm] printed_data.c:104: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] printed_data.c:104: Warning: assertion got status unknown.
[eva:alarm] printed_data.c:113: Warning:
function __e_acsl_assert_register_array: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -39,18 +25,6 @@
\valid(data->values) got status unknown.
[eva:alarm] printed_data.c:123: Warning: assertion got status unknown.
[eva:alarm] printed_data.c:128: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:133: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:135: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:137: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:139: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:141: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:143: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:145: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:147: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:149: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:151: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:153: Warning: assertion got status unknown.
-[eva:alarm] printed_data.c:155: Warning: assertion got status unknown.
[eva:alarm] printed_data.c:161: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -69,4 +43,3 @@
[eva:alarm] printed_data.c:161: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] printed_data.c:161: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/rte.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/rte.res.oracle
index 2edd48595be133ab838ee24c62105a3b2115d9e9..b4ef67fe9875b620068a64728a007151307ef09e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/rte.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/rte.res.oracle
@@ -1,8 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] rte.i:24: Warning:
- function __gen_e_acsl_test, behavior bhvr: precondition \let var = 1;
- var % j == 1 got status unknown.
[eva:alarm] rte.i:24: Warning:
function __gen_e_acsl_test, behavior bhvr: precondition \forall integer var;
0 <= var < k ==>
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
index 25b29e657268924f21394d4f097ae54dc80d6846..9fa111188d02e2affab248706d8b35d275af1c3e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
@@ -76,7 +76,6 @@
[eva:alarm] ranges_in_builtins.c:57: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] ranges_in_builtins.c:57: Warning: assertion got status unknown.
[eva:alarm] ranges_in_builtins.c:62: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-external-print-value.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-external-print-value.res.oracle
index eb1f35be8d738d8ce5f4358e58bf31dcfa272bd2..0b6fde6e6256bd60044381eed0142bc578cbcbbd 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-external-print-value.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-external-print-value.res.oracle
@@ -2,4 +2,4 @@
[e-acsl] translation done in project "e-acsl".
[eva:alarm] e-acsl-external-print-value.c:7: Warning:
function __e_acsl_assert, behavior non_blocking: precondition got status invalid.
-[eva:alarm] e-acsl-external-print-value.c:7: Warning: check got status unknown.
+[eva:alarm] e-acsl-external-print-value.c:7: Warning: check got status invalid.
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-no-assert-print-data.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-no-assert-print-data.res.oracle
index 982d49ee960fcd4d1c6c8c838a11c0321ef073d6..9bcfd2ee685623053efe3827555705706945133d 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-no-assert-print-data.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-no-assert-print-data.res.oracle
@@ -2,4 +2,4 @@
[e-acsl] translation done in project "e-acsl".
[eva:alarm] e-acsl-no-assert-print-data.c:14: Warning:
function __e_acsl_assert, behavior non_blocking: precondition got status invalid.
-[eva:alarm] e-acsl-no-assert-print-data.c:14: Warning: check got status unknown.
+[eva:alarm] e-acsl-no-assert-print-data.c:14: Warning: check got status invalid.
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 33d434deb9819cfe16e8506fe206fc62e690cf59..778fa0710e35a5e82c7627ef700acda5d56e7a11 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -745,11 +745,6 @@ module Logic_inout: sig
pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
Cil_types.predicate -> Locations.Zone.t option
- (** [term_deps state t] computes the logic dependencies needed to evaluate
- the term [t] in cvalue state [state].
- Returns None on either an evaluation error or on unsupported construct. *)
- val term_deps: Cvalue.Model.t -> Cil_types.term -> Locations.Zone.t option
-
(** Returns the list of behaviors of the given function that are active for
the given initial state. *)
val valid_behaviors:
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 0eceb70bf4872593ecfed55d2ff0353f4261d740..6f7b8fe7f10a96f00f209706d8e1a3bf1a47cc0a 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -1321,12 +1321,15 @@ let rec eval_term ~alarm_mode env t =
in
{ r with empty = true; ldeps }
+ | Tlet (li, t') ->
+ let env = eval_let_binding ~alarm_mode env li in
+ eval_term ~alarm_mode env t'
+
| Tlambda _ -> unsupported "logic functions or predicates"
| TUpdate _ -> unsupported "functional updates"
| Ttype _ -> unsupported "\\type operator"
| Ttypeof _ -> unsupported "\\typeof operator"
| Tinter _ -> unsupported "set intersection"
- | Tlet _ -> unsupported "\\let bindings"
| TConst (LStr _) -> unsupported "constant strings"
| TConst (LWStr _) -> unsupported "wide constant strings"
@@ -1633,6 +1636,15 @@ and bind_comprehension_quantifiers env quantifiers predicate =
display_evaluation_error ~loc:pred.pred_loc error;
env
+and eval_let_binding ~alarm_mode env logic_info =
+ match logic_info with
+ | { l_labels = []; l_tparams = []; l_profile = []; l_body = LBterm term } ->
+ let var = logic_info.l_var_info in
+ let env = bind_logic_vars env [var] in
+ let var_term = Logic_const.tvar var in
+ reduce_by_left_relation ~alarm_mode env true var_term Req term
+ | _ -> unsupported "\\let binding"
+
(* -------------------------------------------------------------------------- *)
(* --- Evaluation of term lval and of terms as location --- *)
(* -------------------------------------------------------------------------- *)
@@ -2284,6 +2296,16 @@ and reduce_by_predicate ~alarm_mode env positive p =
unbind_logic_vars env_result varl
with LogicEvalError _ -> env
end
+
+ | _, Plet (li, p') ->
+ begin
+ try
+ let env = eval_let_binding ~alarm_mode env li in
+ let env_result = reduce_by_predicate ~alarm_mode env positive p' in
+ unbind_logic_vars env_result [li.l_var_info]
+ with LogicEvalError _ -> env
+ end
+
| _,Papp (li, labels, args) -> begin
if is_known_predicate li.l_var_info then
try reduce_by_known_papp ~alarm_mode env positive li labels args
@@ -2316,7 +2338,6 @@ and reduce_by_predicate ~alarm_mode env positive p =
| false, false -> assert false (* a logic alarm would have been raised*)
end
| true, Pexists (_, _) | false, Pforall (_, _)
- | _,Plet (_, _)
| _,Pallocable (_,_) | _,Pfreeable (_,_) | _,Pfresh (_,_,_,_)
| _, Pseparated _
-> env
@@ -2513,6 +2534,10 @@ and eval_predicate env pred =
| _ -> Unknown
end
+ | Plet (li, p') ->
+ let env = eval_let_binding ~alarm_mode env li in
+ do_eval env p'
+
| Pnot p -> begin match do_eval env p with
| True -> False
| False -> True
@@ -2586,10 +2611,7 @@ and eval_predicate env pred =
| Pfreeable (BuiltinLabel Here, t) ->
let r = eval_term ~alarm_mode env t in
Builtins_malloc.freeable r.eover
- | Pfresh (_,_,_,_)
- | Pallocable _ | Pfreeable _
- | Plet (_,_)
- -> Unknown
+ | Pfresh _ | Pallocable _ | Pfreeable _ -> Unknown
(* Logic predicates. Update the list known_predicates above if you
add something here. *)
@@ -2690,6 +2712,13 @@ and predicate_deps env pred =
let rec do_eval env p =
let term_deps term = (eval_term ~alarm_mode env term).ldeps in
let tsets_deps lbl tsets = eval_tsets_deps ~alarm_mode env lbl tsets in
+ let logic_info_deps li =
+ match li.l_body with
+ | LBnone -> empty_logic_deps
+ | LBterm t -> term_deps t
+ | LBpred p -> do_eval env p
+ | _ -> unsupported (Format.asprintf "%a" Printer.pp_logic_info li)
+ in
match p.pred_content with
| Ptrue | Pfalse -> empty_logic_deps
@@ -2727,8 +2756,9 @@ and predicate_deps env pred =
Logic_interp.do_term_lval. *)
do_eval env p
- | Plet (_v, p) -> do_eval env p (* will this work when when we need [_v]
- to evaluate [p] ?.. *)
+ | Plet (li, p) ->
+ let env = eval_let_binding ~alarm_mode env li in
+ join_logic_deps (logic_info_deps li) (do_eval env p)
| Papp (li, _labels, args) -> begin
if is_known_predicate li.l_var_info then
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index 9ed96ed03ade8bc969f784768289f74663412b07..ddec2c39239451d647383b453d55c3800a534a7c 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -34,11 +34,6 @@ val predicate_deps:
pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
Cil_types.predicate -> Locations.Zone.t option
-(** [term_deps state t] computes the logic dependencies needed to evaluate
- the term [t] in cvalue state [state].
- Returns None on either an evaluation error or on unsupported construct. *)
-val term_deps: Cvalue.Model.t -> Cil_types.term -> Locations.Zone.t option
-
(** Returns the list of behaviors of the given function that are active for
the given initial state. *)
val valid_behaviors:
diff --git a/tests/value/logic.c b/tests/value/logic.c
index 8806b1930519098b26629b39b460e9e53098c516..b91a17f6003d68520e79c5f642ca7ccbb7406542 100644
--- a/tests/value/logic.c
+++ b/tests/value/logic.c
@@ -134,7 +134,7 @@ void eq_tsets () {
//@ assert s1 == s2; // True at link-time
//@ assert t != u; // false
- //@ assert \union(0) == \union(0.0);
+ //@ assert \union(0) == \union(0.0);
//@ assert \union(1.0) == \union(1);
//@ assert \union(1, 1.0) == \union(1.0, 1);
@@ -503,6 +503,41 @@ void set_comprehension_assigns () {
multi_memset(p, 1, 2, 10);
}
+/* Tests the evaluation of \let bindings in ACSL predicates. */
+void plet () {
+ int x = Frama_C_interval(0, 120);
+ int y = Frama_C_interval(0, 10);
+ int z = Frama_C_interval(10, 30);
+ if (v) {
+ //@ assert unknown: \let l = 25; x < l;
+ Frama_C_show_each_0_24(x);
+ }
+ if (v) {
+ //@ assert true: \let l = 250; x < l;
+ Frama_C_show_each_0_120(x);
+ }
+ if (v) {
+ //@ assert false: \let l = 0; x < l;
+ Frama_C_show_each_bottom(x);
+ }
+
+ /* Tests multiple \let bindings. */
+ //@ assert true: \let l = y + z; \let l2 = 100; l < l2;
+ //@ assert unknown: \let l = y + z; \let l2 = x; l < l2;
+
+ /* Tests the kind of assertions generated by the instantiate plugin. */
+ unsigned int t[12];
+ /*@ assert valid: \let __fc_len=12; \valid(t + (0 .. __fc_len-1)); */
+ /*@ assert unknown: \let __fc_len=z; \valid(t + (0 .. __fc_len-1)); */
+ if (v) {
+ /*@ assert invalid: \let __fc_len=12; \valid(t + (0 .. __fc_len)); */
+ Frama_C_show_each_bottom(t);
+ }
+
+ /* Unsupported \let bindings. */
+ /*@ assert unsupported: \let id = (\lambda integer y; y); id(42) == 42; */
+}
+
void main () {
eq_tsets();
eq_char();
@@ -521,4 +556,5 @@ void main () {
float_abs();
set_comprehension();
set_comprehension_assigns();
+ plet();
}
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index 30722c6f9202a123856a2607a254fc4cd1c34f78..f88f05e9117129bb86b043b56223a54f5c3c6475 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -14,7 +14,7 @@
arr_ptr[0..2] ∈ {0}
arr_ptr_arr[0..5] ∈ {0}
[eva] computing for function eq_tsets <- main.
- Called from logic.c:507.
+ Called from logic.c:542.
[eva] logic.c:103:
cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#8>
[eva:alarm] logic.c:103: Warning: assertion got status unknown.
@@ -56,20 +56,20 @@
[eva] Recording results for eq_tsets
[eva] Done for function eq_tsets
[eva] computing for function eq_char <- main.
- Called from logic.c:508.
+ Called from logic.c:543.
[eva] logic.c:149: Frama_C_show_each: {-126}
[eva] logic.c:150: assertion got status valid.
[eva] logic.c:151: assertion got status valid.
[eva] Recording results for eq_char
[eva] Done for function eq_char
[eva] computing for function casts <- main.
- Called from logic.c:509.
+ Called from logic.c:544.
[eva] logic.c:155: assertion got status valid.
[eva] logic.c:156: assertion got status valid.
[eva] Recording results for casts
[eva] Done for function casts
[eva] computing for function empty_tset <- main.
- Called from logic.c:510.
+ Called from logic.c:545.
[eva] computing for function f_empty_tset <- empty_tset <- main.
Called from logic.c:166.
[eva] using specification for function f_empty_tset
@@ -80,7 +80,7 @@
[eva] Recording results for empty_tset
[eva] Done for function empty_tset
[eva] computing for function reduce_by_equal <- main.
- Called from logic.c:511.
+ Called from logic.c:546.
[eva:alarm] logic.c:172: Warning: accessing out of bounds index. assert 0 ≤ v;
[eva:alarm] logic.c:172: Warning: accessing out of bounds index. assert v < 10;
[eva:alarm] logic.c:173: Warning: assertion got status unknown.
@@ -88,7 +88,7 @@
[eva] Recording results for reduce_by_equal
[eva] Done for function reduce_by_equal
[eva] computing for function alarms <- main.
- Called from logic.c:512.
+ Called from logic.c:547.
[eva:alarm] logic.c:182: Warning: assertion 'ASSUME' got status unknown.
[eva:alarm] logic.c:184: Warning: assertion 'UNK' got status unknown.
[eva] logic.c:185: Frama_C_show_each: {-1; 1}
@@ -112,7 +112,7 @@
[eva] Recording results for alarms
[eva] Done for function alarms
[eva] computing for function cond_in_lval <- main.
- Called from logic.c:513.
+ Called from logic.c:548.
[eva] computing for function select_like <- cond_in_lval <- main.
Called from logic.c:228.
[eva] using specification for function select_like
@@ -140,7 +140,7 @@
[eva] Recording results for cond_in_lval
[eva] Done for function cond_in_lval
[eva] computing for function pred <- main.
- Called from logic.c:514.
+ Called from logic.c:549.
[eva] logic.c:90: assertion got status valid.
[eva] logic.c:91: assertion got status valid.
[eva] logic.c:31: cannot evaluate ACSL term, \at() on a C label is unsupported
@@ -185,7 +185,7 @@
[eva] Recording results for pred
[eva] Done for function pred
[eva] computing for function float_sign <- main.
- Called from logic.c:515.
+ Called from logic.c:550.
[eva] logic.c:251: assertion got status valid.
[eva] logic.c:252: assertion got status valid.
[eva] logic.c:253: assertion got status valid.
@@ -194,7 +194,7 @@
[eva] Recording results for float_sign
[eva] Done for function float_sign
[eva] computing for function min_max <- main.
- Called from logic.c:516.
+ Called from logic.c:551.
[eva] computing for function Frama_C_interval <- min_max <- main.
Called from logic.c:274.
[eva] using specification for function Frama_C_interval
@@ -219,7 +219,7 @@
[eva] Recording results for min_max
[eva] Done for function min_max
[eva] computing for function assign_tsets <- main.
- Called from logic.c:517.
+ Called from logic.c:552.
[eva] computing for function assign_tsets_aux <- assign_tsets <- main.
Called from logic.c:269.
[eva] using specification for function assign_tsets_aux
@@ -227,7 +227,7 @@
[eva] Recording results for assign_tsets
[eva] Done for function assign_tsets
[eva] computing for function check_and_assert <- main.
- Called from logic.c:518.
+ Called from logic.c:553.
[eva:alarm] logic.c:295: Warning: assertion got status unknown.
[eva] logic.c:296: Frama_C_show_each_42: {42}
[eva] logic.c:297: check got status valid.
@@ -241,7 +241,7 @@
[eva] Recording results for check_and_assert
[eva] Done for function check_and_assert
[eva] computing for function min_max_quantifier <- main.
- Called from logic.c:519.
+ Called from logic.c:554.
[eva] logic.c:321: check 'valid' got status valid.
[eva] logic.c:322: check 'valid' got status valid.
[eva] logic.c:323: check 'valid' got status valid.
@@ -303,7 +303,7 @@
[eva] Recording results for min_max_quantifier
[eva] Done for function min_max_quantifier
[eva] computing for function int_abs <- main.
- Called from logic.c:520.
+ Called from logic.c:555.
[eva] computing for function abs <- int_abs <- main.
Called from logic.c:365.
[eva] using specification for function abs
@@ -425,7 +425,7 @@
[eva] Recording results for int_abs
[eva] Done for function int_abs
[eva] computing for function float_abs <- main.
- Called from logic.c:521.
+ Called from logic.c:556.
[eva] computing for function fabs <- float_abs <- main.
Called from logic.c:421.
[eva] using specification for function fabs
@@ -484,7 +484,7 @@
[eva] Recording results for float_abs
[eva] Done for function float_abs
[eva] computing for function set_comprehension <- main.
- Called from logic.c:522.
+ Called from logic.c:557.
[eva:alarm] logic.c:444: Warning: assertion got status unknown.
[eva] logic.c:445: Frama_C_show_each_10_100: [10..100]
[eva:alarm] logic.c:448: Warning: assertion got status unknown.
@@ -520,15 +520,55 @@
[eva] Recording results for set_comprehension
[eva] Done for function set_comprehension
[eva] computing for function set_comprehension_assigns <- main.
- Called from logic.c:523.
+ Called from logic.c:558.
[eva] computing for function multi_memset <- set_comprehension_assigns <- main.
Called from logic.c:503.
[eva] using specification for function multi_memset
[eva] Done for function multi_memset
[eva] Recording results for set_comprehension_assigns
[eva] Done for function set_comprehension_assigns
+[eva] computing for function plet <- main.
+ Called from logic.c:559.
+[eva] computing for function Frama_C_interval <- plet <- main.
+ Called from logic.c:508.
+[eva] logic.c:508:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- plet <- main.
+ Called from logic.c:509.
+[eva] logic.c:509:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- plet <- main.
+ Called from logic.c:510.
+[eva] logic.c:510:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] logic.c:512: Warning: assertion 'unknown' got status unknown.
+[eva] logic.c:513: Frama_C_show_each_0_24: [0..24]
+[eva] logic.c:516: assertion 'true' got status valid.
+[eva] logic.c:517: Frama_C_show_each_0_120: [0..120]
+[eva:alarm] logic.c:520: Warning:
+ assertion 'false' got status invalid (stopping propagation).
+[eva] logic.c:525: assertion 'true' got status valid.
+[eva:alarm] logic.c:526: Warning: assertion 'unknown' got status unknown.
+[eva] logic.c:530: assertion 'valid' got status valid.
+[eva:alarm] logic.c:531: Warning: assertion 'unknown' got status unknown.
+[eva:alarm] logic.c:533: Warning:
+ assertion 'invalid' got status invalid (stopping propagation).
+[eva] logic.c:538:
+ cannot evaluate ACSL term, unsupported ACSL construct: \let binding
+[eva:alarm] logic.c:538: Warning: assertion 'unsupported' got status unknown.
+[eva] Recording results for plet
+[eva] Done for function plet
[eva] Recording results for main
[eva] Done for function main
+[eva] logic.c:530:
+ Cannot evaluate range bound __fc_len - 1
+ (unsupported logic var __fc_len). Approximating
+[eva] logic.c:533:
+ Cannot evaluate range bound __fc_len
+ (unsupported logic var __fc_len). Approximating
[scope:rm_asserts] removing 5 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function alarms:
@@ -661,6 +701,11 @@
[61] ∈ {3}
[62] ∈ {2}
[63] ∈ {1}
+[eva:final-states] Values at end of function plet:
+ Frama_C_entropy_source ∈ [--..--]
+ x_0 ∈ [0..120]
+ y ∈ [0..10]
+ z ∈ [10..30]
[eva:final-states] Values at end of function reduce_by_equal:
a[0..8] ∈ {1}
[9] ∈ [--..--]
@@ -762,6 +807,8 @@
[from] Done for function min_max
[from] Computing for function min_max_quantifier
[from] Done for function min_max_quantifier
+[from] Computing for function plet
+[from] Done for function plet
[from] Computing for function reduce_by_equal
[from] Done for function reduce_by_equal
[from] Computing for function cond_in_lval
@@ -830,6 +877,8 @@
[from] Function multi_memset:
buf1[0..9] FROM \nothing (and SELF)
buf2[0..7] FROM \nothing (and SELF)
+[from] Function plet:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function reduce_by_equal:
NO EFFECTS
[from] Function select_like:
@@ -914,6 +963,10 @@
Frama_C_entropy_source; i; j; t_0[0..63]
[inout] Inputs for function min_max_quantifier:
Frama_C_entropy_source
+[inout] Out (internal) for function plet:
+ Frama_C_entropy_source; x_0; y; z
+[inout] Inputs for function plet:
+ Frama_C_entropy_source; v
[inout] Out (internal) for function reduce_by_equal:
a[0..9]
[inout] Inputs for function reduce_by_equal: