From 10b576b80794118cb0b537330fee45c0dd9597ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 22 Sep 2023 12:43:17 +0200
Subject: [PATCH] [Eva] Adds tests of the evaluation of \let bindings in ACSL
predicates.
---
tests/value/logic.c | 38 ++++++++++++-
tests/value/oracle/logic.res.oracle | 87 +++++++++++++++++++++++------
2 files changed, 107 insertions(+), 18 deletions(-)
diff --git a/tests/value/logic.c b/tests/value/logic.c
index 8806b193051..b91a17f6003 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 30722c6f920..f88f05e9117 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:
--
GitLab