From 2c09ea263db731fa6278b6f8c675c45df7cbd65e Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 28 Mar 2024 21:35:31 +0100
Subject: [PATCH] [Eva] test reduction by valid_wstring and valid_read_wstring
---
tests/value/oracle/strings_logic.res.oracle | 52 ++++++++++++++++++++-
tests/value/strings_logic.c | 35 +++++++++++++-
2 files changed, 85 insertions(+), 2 deletions(-)
diff --git a/tests/value/oracle/strings_logic.res.oracle b/tests/value/oracle/strings_logic.res.oracle
index 1b681b00f32..08a758fed24 100644
--- a/tests/value/oracle/strings_logic.res.oracle
+++ b/tests/value/oracle/strings_logic.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] computing for function reduce_by_valid_string <- main.
- Called from strings_logic.c:177.
+ Called from strings_logic.c:209.
[eva:loop-unroll:auto] strings_logic.c:30: Automatic loop unrolling.
[eva:loop-unroll:auto] strings_logic.c:36: Automatic loop unrolling.
[eva:loop-unroll:auto] strings_logic.c:41: Automatic loop unrolling.
@@ -131,6 +131,21 @@
(origin: Library function {strings_logic.c:151}) }}
[eva] Recording results for reduce_by_valid_string
[eva] Done for function reduce_by_valid_string
+[eva] computing for function reduce_by_valid_wstring <- main.
+ Called from strings_logic.c:210.
+[eva:alarm] strings_logic.c:193: Warning: assertion got status unknown.
+[eva] strings_logic.c:194:
+ Frama_C_show_each_wide_string_valid_wstring: {{ &ws1 ; &ws_zero }}
+[eva:alarm] strings_logic.c:198: Warning: assertion got status unknown.
+[eva] strings_logic.c:199:
+ Frama_C_show_each_wide_string_valid_read_wstring:
+ {{ &ws1 ; &ws_zero ; L"Wide literal" }}
+[eva:alarm] strings_logic.c:203: Warning: assertion got status unknown.
+[eva] strings_logic.c:204:
+ Frama_C_show_each_wide_string_invalid_read_wstring:
+ {{ &ws1 ; &ws_zero ; &wchar ; &ws_with_hole ; L"Wide literal" }}
+[eva] Recording results for reduce_by_valid_wstring
+[eva] Done for function reduce_by_valid_wstring
[eva] Recording results for main
[eva] Done for function main
[eva:garbled-mix:summary]
@@ -202,12 +217,41 @@
.[bits 104 to 127] ∈ UNINITIALIZED
p ∈ {0}
offset ∈ {5; 10; 20}
+[eva:final-states] Values at end of function reduce_by_valid_wstring:
+ ws1[0] ∈ {104}
+ [1] ∈ {101}
+ [2..3] ∈ {108}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ [6] ∈ {32}
+ [7] ∈ {119}
+ [8] ∈ {105}
+ [9] ∈ {100}
+ [10] ∈ {101}
+ [11] ∈ {32}
+ [12] ∈ {119}
+ [13] ∈ {111}
+ [14] ∈ {114}
+ [15] ∈ {108}
+ [16] ∈ {100}
+ [17] ∈ {33}
+ [18] ∈ {0}
+ ws_zero[0..31] ∈ {0}
+ wchar ∈ {90}
+ ws_with_hole[0][bits 0 to 7]# ∈ {104}%32, bits 0 to 7
+ [0][bits 8 to 15] ∈ {0}
+ [0][bits 16 to 31]# ∈ {104}%32, bits 16 to 31
+ [1] ∈ {105}
+ wp ∈
+ {{ &ws1[0] ; &ws_zero[0] ; &wchar ; &ws_with_hole[0] ; L"Wide literal" }} or UNINITIALIZED
[eva:final-states] Values at end of function main:
[from] Computing for function reduce_by_valid_string
[from] Computing for function garbled_mix <-reduce_by_valid_string
[from] Done for function garbled_mix
[from] Done for function reduce_by_valid_string
+[from] Computing for function reduce_by_valid_wstring
+[from] Done for function reduce_by_valid_wstring
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -216,6 +260,8 @@
\result FROM p
[from] Function reduce_by_valid_string:
NO EFFECTS
+[from] Function reduce_by_valid_wstring:
+ NO EFFECTS
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
@@ -226,6 +272,10 @@
i_3; anything{.ptr; .d; .c}; p; offset; tmp; tmp_0
[inout] Inputs for function reduce_by_valid_string:
nondet
+[inout] Out (internal) for function reduce_by_valid_wstring:
+ ws1[0..18]; ws_zero[0..31]; wchar; ws_with_hole[0..1]; wp
+[inout] Inputs for function reduce_by_valid_wstring:
+ nondet
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
diff --git a/tests/value/strings_logic.c b/tests/value/strings_logic.c
index 3fe276661fe..d0f2e58ffff 100644
--- a/tests/value/strings_logic.c
+++ b/tests/value/strings_logic.c
@@ -5,7 +5,7 @@
/* Tests the evaluation and reduction by ACSL predicate on strings. */
#include "__fc_string_axiomatic.h"
-
+#include "wchar.h"
volatile char nondet;
struct anything {
@@ -173,6 +173,39 @@ void reduce_by_valid_string (void) {
p = NULL;
}
+void reduce_by_valid_wstring (void) {
+ wchar_t ws1[] = L"hello\000 wide world!";
+ wchar_t ws_zero[32] = {0};
+ wchar_t wchar = L'Z';
+ wchar_t ws_with_hole[2] = L"hi"; // no space for L'\0'!
+ ((char*)ws_with_hole)[1] = '\0'; // valid string but not valid wide string
+
+ wchar_t *wp;
+ switch (nondet) {
+ case 0: wp = ws1; break;
+ case 1: wp = L"Wide literal"; break;
+ case 2: wp = ws_zero; break;
+ case 3: wp = &wchar; break;
+ case 4: wp = ws_with_hole; break;
+ }
+
+ if (nondet) {
+ //@ assert valid_wstring(wp);
+ Frama_C_show_each_wide_string_valid_wstring(wp);
+ }
+
+ if (nondet) {
+ //@ assert valid_read_wstring(wp);
+ Frama_C_show_each_wide_string_valid_read_wstring(wp);
+ }
+
+ if (nondet) {
+ //@ assert !valid_read_wstring(wp);
+ Frama_C_show_each_wide_string_invalid_read_wstring(wp);
+ }
+}
+
void main (void) {
reduce_by_valid_string();
+ reduce_by_valid_wstring();
}
--
GitLab