From d2159ad0408efb4361a2e45b4f114f71543d26c8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 22 May 2017 09:07:48 +0200
Subject: [PATCH] [Eva] fix str builtins for negative offsets
Each call to fold_itv must be preceded by a check of the actual validity of
the offsets (since fold_itv will take the intersection). In the case of an
exact offset, the right side is already taken into account, so we only have
to check the left (negative) bounds.
---
.../value/domains/cvalue/builtins_string.ml | 53 +++++----
tests/non-free/oracle/strlen.res.oracle | 91 +++++++++++++---
tests/non-free/oracle/strnlen2.res.oracle | 101 +++++++++++++++---
tests/non-free/strlen.c | 26 +++++
tests/non-free/strnlen2.c | 26 +++++
5 files changed, 249 insertions(+), 48 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 11ea3c4b8c3..612559fa56f 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -783,6 +783,8 @@ module Search_single_offset = struct
(instead of relative ones) during the fold, and only at the end
they are converted into relative bounds. *)
try
+ if Int.(lt offset zero) then
+ raise (Bottom_val (None, false, IS.bottom, offset));
let acc =
Bytecharmap.fold_itv ~direction:`LTR ~entire:false
(fun (range_start, range_end) bs acc ->
@@ -1194,8 +1196,6 @@ module Search_ranges = struct
or [max_offset + max_n] for strnlen.
For strnlen, max_byte_to_look may be adjusted by Search_single.search_and_acc
to a more precise value. *)
- (* [base] is only used to obtain the maximum validity, when the result is
- imprecise *)
let search bytecharmap ~ret_rel_offs base offset_ival offset_start offset_end ?n_len last_byte_to_look =
fpf "@[by_offset_ival: offset_ival: %a, offset_start: %a, offset_end: %a, \
last_byte_to_look: %a@]" Ival.pretty offset_ival Int.pretty offset_start
@@ -1226,25 +1226,40 @@ module Search_ranges = struct
search_init bytecharmap ?n_len last_byte_to_look offset_end
in
fpf "search_init returned init_acc = %a" pp_acc init_acc;
- let res_acc =
- Bytecharmap.fold_itv ~direction:`RTL ~entire:false
- (fun (range_start, range_end) bs acc ->
- search_rtl range_start range_end bs ?n_len acc
- ) (offset_start, (I.pred offset_end)) bytecharmap init_acc
+ let validity_alarm, valid_itv =
+ Tr_offset.trim_by_validity
+ Ival.(mul (of_int 8) offset_ival)
+ Int.eight (*sizeof(char)*) (Base.validity base)
in
- fpf "res_acc = %a" pp_acc res_acc;
- match res_acc.best_min, res_acc.best_max with
- | Some _, Some _ ->
- (* for strnlen, adjust bounds according to the [n] argument *)
- let (adj_min, adj_max) =
- adjust_bounds res_acc.best_min res_acc.best_max n_len
+ fpf "trim_by_validity (%a, %a) returned = %b, %a"
+ Int.pretty offset_start Int.pretty offset_end
+ validity_alarm Tr_offset.pretty valid_itv;
+ match valid_itv with
+ | Tr_offset.Invalid -> (* no valid interval *)
+ let is = { init_acc.is with IS.maybe_indet = true } in
+ Never_ok is, Not_imprecise
+ | _ ->
+ let res_acc =
+ Bytecharmap.fold_itv ~direction:`RTL ~entire:false
+ (fun (range_start, range_end) bs acc ->
+ search_rtl range_start range_end bs ?n_len acc
+ ) (offset_start, (I.pred offset_end)) bytecharmap init_acc
in
- Maybe_ok (Ival.inject_range adj_min adj_max,
- (*abs_offs not used by caller*)Ival.top,
- (*fs not used by caller*)FS.Top, res_acc.maybe_not_found,
- res_acc.best_es, res_acc.is), Not_imprecise
- | _, _ ->
- Never_ok (res_acc.is), Not_imprecise
+ fpf "res_acc = %a" pp_acc res_acc;
+ match res_acc.best_min, res_acc.best_max with
+ | Some _, Some _ ->
+ (* for strnlen, adjust bounds according to the [n] argument *)
+ let (adj_min, adj_max) =
+ adjust_bounds res_acc.best_min res_acc.best_max n_len
+ in
+ let maybe_indet = res_acc.is.IS.maybe_indet || validity_alarm in
+ Maybe_ok (Ival.inject_range adj_min adj_max,
+ (*abs_offs not used by caller*)Ival.top,
+ (*fs not used by caller*)FS.Top, res_acc.maybe_not_found,
+ res_acc.best_es, { res_acc.is with IS.maybe_indet }),
+ Not_imprecise
+ | _, _ ->
+ Never_ok (res_acc.is), Not_imprecise
end
in
res
diff --git a/tests/non-free/oracle/strlen.res.oracle b/tests/non-free/oracle/strlen.res.oracle
index 9869e40a9df..c1f907990e1 100644
--- a/tests/non-free/oracle/strlen.res.oracle
+++ b/tests/non-free/oracle/strlen.res.oracle
@@ -32,7 +32,7 @@
[11] ∈ {100}
nondet ∈ [--..--]
[value] computing for function small_sets <- main.
- Called from tests/non-free/strlen.c:309.
+ Called from tests/non-free/strlen.c:334.
tests/non-free/strlen.c:60:[value] Call to builtin Frama_C_strlen(({{ "abc" + {0; 1} }}))
tests/non-free/strlen.c:61:[value] assertion got status valid.
tests/non-free/strlen.c:65:[value] Call to builtin Frama_C_strlen(({{ "\000bc" + {0; 1} }}))
@@ -47,7 +47,7 @@ tests/non-free/strlen.c:82:[value] assertion got status valid.
[value] Recording results for small_sets
[value] Done for function small_sets
[value] computing for function zero_termination <- main.
- Called from tests/non-free/strlen.c:310.
+ Called from tests/non-free/strlen.c:335.
tests/non-free/strlen.c:89:[value] Call to builtin Frama_C_strlen(({{ &empty_or_non_terminated[0] }}))
tests/non-free/strlen.c:89:[value] warning: builtin Frama_C_strlen: possibly reading indeterminate data
tests/non-free/strlen.c:90:[value] assertion got status valid.
@@ -58,7 +58,7 @@ tests/non-free/strlen.c:97:[value] warning: builtin Frama_C_strlen: reading inde
[value] Recording results for zero_termination
[value] Done for function zero_termination
[value] computing for function strlen_initialization <- main.
- Called from tests/non-free/strlen.c:311.
+ Called from tests/non-free/strlen.c:336.
[value] computing for function my_strlen <- strlen_initialization <- main.
Called from tests/non-free/strlen.c:105.
tests/non-free/strlen.c:54:[value] Call to builtin Frama_C_strlen(({{ &empty_or_uninitialized[0] }}))
@@ -86,7 +86,7 @@ tests/non-free/strlen.c:125:[value] assertion got status valid.
[value] Recording results for strlen_initialization
[value] Done for function strlen_initialization
[value] computing for function strlen_large <- main.
- Called from tests/non-free/strlen.c:312.
+ Called from tests/non-free/strlen.c:337.
[value] computing for function init_array_nondet <- strlen_large <- main.
Called from tests/non-free/strlen.c:168.
tests/non-free/strlen.c:161:[value] Call to builtin memset(({{ (void *)&a }},{1; 2},{100}))
@@ -147,7 +147,7 @@ tests/non-free/strlen.c:190:[value] assertion got status valid.
[value] Recording results for strlen_large
[value] Done for function strlen_large
[value] computing for function strlen_large_uninit <- main.
- Called from tests/non-free/strlen.c:313.
+ Called from tests/non-free/strlen.c:338.
[value] computing for function init_array_nondet <- strlen_large_uninit <- main.
Called from tests/non-free/strlen.c:197.
tests/non-free/strlen.c:161:[value] Call to builtin memset(({{ (void *)&a }},{1; 2},{40}))
@@ -188,7 +188,7 @@ tests/non-free/strlen.c:213:[value] assertion got status valid.
[value] Recording results for strlen_large_uninit
[value] Done for function strlen_large_uninit
[value] computing for function misc <- main.
- Called from tests/non-free/strlen.c:314.
+ Called from tests/non-free/strlen.c:339.
tests/non-free/strlen.c:241:[value] Call to builtin Frama_C_strlen(({{ &unterminated_string[0] }}))
tests/non-free/strlen.c:241:[value] warning: builtin Frama_C_strlen: reading indeterminate data
tests/non-free/strlen.c:244:[value] Call to builtin Frama_C_strlen(({{ "Hello World\n" ; "Bonjour Monde\n" }}))
@@ -229,19 +229,19 @@ tests/non-free/strlen.c:278:[value] assertion got status valid.
[value] Recording results for misc
[value] Done for function misc
[value] computing for function bitfields <- main.
- Called from tests/non-free/strlen.c:315.
+ Called from tests/non-free/strlen.c:340.
tests/non-free/strlen.c:140:[value] Call to builtin Frama_C_strlen(({{ (char const *)&s }}))
tests/non-free/strlen.c:140:[value] warning: builtin Frama_C_strlen: reading indeterminate data
[value] Recording results for bitfields
[value] Done for function bitfields
[value] computing for function bitfields2 <- main.
- Called from tests/non-free/strlen.c:316.
+ Called from tests/non-free/strlen.c:341.
tests/non-free/strlen.c:155:[value] Call to builtin Frama_C_strlen(({{ (char const *)&s }}))
tests/non-free/strlen.c:156:[value] assertion got status valid.
[value] Recording results for bitfields2
[value] Done for function bitfields2
[value] computing for function escaping <- main.
- Called from tests/non-free/strlen.c:317.
+ Called from tests/non-free/strlen.c:342.
tests/non-free/strlen.c:222:[value] warning: locals {x} escaping the scope of a block of escaping through s
tests/non-free/strlen.c:225:[value] Call to builtin Frama_C_strlen(({{ &s[0] }}))
tests/non-free/strlen.c:225:[value] warning: builtin Frama_C_strlen: possible escaping addresses
@@ -251,7 +251,7 @@ tests/non-free/strlen.c:229:[value] assertion got status valid.
[value] Recording results for escaping
[value] Done for function escaping
[value] computing for function big_array <- main.
- Called from tests/non-free/strlen.c:318.
+ Called from tests/non-free/strlen.c:343.
tests/non-free/strlen.c:287:[value] warning: out of bounds write. assert \valid(p);
tests/non-free/strlen.c:289:[value] warning: out of bounds write. assert \valid(p);
tests/non-free/strlen.c:291:[value] warning: out of bounds write. assert \valid(p);
@@ -281,6 +281,49 @@ tests/non-free/strlen.c:304:[value] warning: builtin Frama_C_strlen:
tests/non-free/strlen.c:305:[value] Frama_C_show_each: {0; 1; 2; 3}, [0..800], [0..3999996]
[value] Recording results for big_array
[value] Done for function big_array
+[value] computing for function negative_offsets <- main.
+ Called from tests/non-free/strlen.c:344.
+tests/non-free/strlen.c:310:[value] entering loop for the first time
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strlen.c:314.
+[value] Done for function Frama_C_interval
+tests/non-free/strlen.c:315:[value] Call to builtin Frama_C_strlen(({{ &buf{[-10], [-9], [-8]} }}))
+tests/non-free/strlen.c:315:[value] warning: builtin Frama_C_strlen: reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strlen.c:318.
+[value] Done for function Frama_C_interval
+tests/non-free/strlen.c:319:[value] Call to builtin Frama_C_strlen(({{ &buf{[-2], [-1]} }}))
+tests/non-free/strlen.c:319:[value] warning: builtin Frama_C_strlen: reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strlen.c:321.
+[value] Done for function Frama_C_interval
+tests/non-free/strlen.c:322:[value] Call to builtin Frama_C_strlen(({{ &buf{[-1], [0]} }}))
+tests/non-free/strlen.c:322:[value] warning: builtin Frama_C_strlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strlen.c:323.
+[value] Done for function Frama_C_interval
+tests/non-free/strlen.c:324:[value] Call to builtin Frama_C_strlen(({{ &buf{[-1], [0], [1], [2]} }}))
+tests/non-free/strlen.c:324:[value] warning: builtin Frama_C_strlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strlen.c:325.
+[value] Done for function Frama_C_interval
+tests/non-free/strlen.c:326:[value] Call to builtin Frama_C_strlen(({{ &buf + [-4..7] }}))
+tests/non-free/strlen.c:326:[value] warning: builtin Frama_C_strlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strlen.c:327.
+[value] Done for function Frama_C_interval
+tests/non-free/strlen.c:329:[value] Call to builtin Frama_C_strlen(({{ &buf + [-10..0] }}))
+tests/non-free/strlen.c:329:[value] warning: builtin Frama_C_strlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] Recording results for negative_offsets
+[value] Done for function negative_offsets
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
@@ -348,6 +391,21 @@ tests/non-free/strlen.c:305:[value] Frama_C_show_each: {0; 1; 2; 3}, [0..800], [
[1] ∈ {0}
[value:final-states] Values at end of function my_strlen:
__retres ∈ [0..54]
+[value:final-states] Values at end of function negative_offsets:
+ Frama_C_entropy_source ∈ [--..--]
+ buf[0..98] ∈ {65} or UNINITIALIZED
+ [99] ∈ {0}
+ len1 ∈ UNINITIALIZED
+ len2 ∈ UNINITIALIZED
+ len3 ∈ {99}
+ len4 ∈ {97; 98; 99}
+ len5 ∈ {92; 93; 94; 95; 96; 97; 98; 99}
+ len6 ∈ {99}
+ offset3 ∈ {-1; 0}
+ offset4 ∈ {-1; 0; 1; 2}
+ offset5 ∈ [-4..7]
+ offset6 ∈ [-10..0]
+ p ∈ {{ &buf + [-10..0] }}
[value:final-states] Values at end of function small_sets:
s ∈ {{ "b\000c" }}
p ∈ {{ "b\000c" + {0; 2} }}
@@ -426,6 +484,8 @@ tests/non-free/strlen.c:305:[value] Frama_C_show_each: {0; 1; 2; 3}, [0..800], [
[from] Done for function misc
[from] Computing for function my_strlen
[from] Done for function my_strlen
+[from] Computing for function negative_offsets
+[from] Done for function negative_offsets
[from] Computing for function small_sets
[from] Done for function small_sets
[from] Computing for function strlen_initialization
@@ -453,7 +513,7 @@ tests/non-free/strlen.c:305:[value] Frama_C_show_each: {0; 1; 2; 3}, [0..800], [
non_terminated2[2..3]; empty_or_uninitialized[0];
uninitialized[0]; s[0..1]; t[0..3]; s; s; a[3..99]; a[3..99];
s[0..3]; loc_char_array[0..4]; x; maybe_init[0..1];
- t[0..999999]; u[0..199]; r[0..200];
+ t[0..999999]; u[0..199]; r[0..200]; buf[0..99];
"Hello World\n"[bits 0 to 103];
"abc\000\000\000abc"[bits 0 to 79]; ""[bits 0 to 7];
"a"[bits 0 to 15]; "aa"[bits 0 to 23]; "aaa";
@@ -492,6 +552,8 @@ tests/non-free/strlen.c:305:[value] Frama_C_show_each: {0; 1; 2; 3}, [0..800], [
"Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
"efg"[bits 8 to 31]; "EFGH"[bits 8 to 39];
"mno\000pqr"[bits 0 to 63]; "MNOP\000QRS"[bits 0 to 71]
+[from] Function negative_offsets:
+ Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
[from] Function small_sets:
NO EFFECTS
[from] Function strlen_initialization:
@@ -503,7 +565,7 @@ tests/non-free/strlen.c:305:[value] Frama_C_show_each: {0; 1; 2; 3}, [0..800], [
[from] Function zero_termination:
NO EFFECTS
[from] Function main:
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function big_array:
@@ -546,6 +608,11 @@ tests/non-free/strlen.c:305:[value] Frama_C_show_each: {0; 1; 2; 3}, [0..800], [
[inout] Inputs for function my_strlen:
empty_or_uninitialized[0]; uninitialized[0]; s[0..1]; t[0..3]; a[0..99];
a[0..99]
+[inout] Out (internal) for function negative_offsets:
+ Frama_C_entropy_source; buf[0..99]; i; len1; len2; len3; len4; len5;
+ len6; offset1; offset2; offset3; offset4; offset5; offset6; p
+[inout] Inputs for function negative_offsets:
+ Frama_C_entropy_source; nondet
[inout] Out (internal) for function small_sets:
s; p; tmp; z1; tmp_0; z2; tmp_1; z3; tmp_2; z4; tmp_3; t[0..3]; z5; tmp_4
[inout] Inputs for function small_sets:
diff --git a/tests/non-free/oracle/strnlen2.res.oracle b/tests/non-free/oracle/strnlen2.res.oracle
index e6ca5c2a224..d1fb216242b 100644
--- a/tests/non-free/oracle/strnlen2.res.oracle
+++ b/tests/non-free/oracle/strnlen2.res.oracle
@@ -32,7 +32,7 @@
[11] ∈ {100}
nondet ∈ [--..--]
[value] computing for function small_sets <- main.
- Called from tests/non-free/strnlen2.c:488.
+ Called from tests/non-free/strnlen2.c:513.
tests/non-free/strnlen2.c:45:[value] Call to builtin Frama_C_strnlen(({{ "abc" + {0; 1} }},{3}))
tests/non-free/strnlen2.c:46:[value] assertion got status valid.
tests/non-free/strnlen2.c:49:[value] Call to builtin Frama_C_strnlen(({{ "\000bc" + {0; 1} }},{2}))
@@ -46,7 +46,7 @@ tests/non-free/strnlen2.c:62:[value] assertion got status valid.
[value] Recording results for small_sets
[value] Done for function small_sets
[value] computing for function zero_termination <- main.
- Called from tests/non-free/strnlen2.c:489.
+ Called from tests/non-free/strnlen2.c:514.
tests/non-free/strnlen2.c:68:[value] Call to builtin Frama_C_strnlen(({{ &empty_or_non_terminated[0] }},{1}))
tests/non-free/strnlen2.c:69:[value] assertion got status valid.
tests/non-free/strnlen2.c:73:[value] Call to builtin Frama_C_strnlen(({{ &non_terminated[0] }},{2}))
@@ -56,7 +56,7 @@ tests/non-free/strnlen2.c:79:[value] warning: builtin Frama_C_strnlen: reading i
[value] Recording results for zero_termination
[value] Done for function zero_termination
[value] computing for function initialization <- main.
- Called from tests/non-free/strnlen2.c:491.
+ Called from tests/non-free/strnlen2.c:516.
tests/non-free/strnlen2.c:85:[value] Call to builtin Frama_C_strnlen(({{ &empty_or_uninitialized[0] }},{1}))
tests/non-free/strnlen2.c:85:[value] warning: builtin Frama_C_strnlen: possible uninitialized values
tests/non-free/strnlen2.c:86:[value] assertion got status valid.
@@ -71,7 +71,7 @@ tests/non-free/strnlen2.c:102:[value] assertion got status valid.
[value] Recording results for initialization
[value] Done for function initialization
[value] computing for function large <- main.
- Called from tests/non-free/strnlen2.c:492.
+ Called from tests/non-free/strnlen2.c:517.
[value] computing for function init_array_nondet <- large <- main.
Called from tests/non-free/strnlen2.c:144.
tests/non-free/strnlen2.c:138:[value] Call to builtin memset(({{ (void *)&a }},{1; 2},{100}))
@@ -114,7 +114,7 @@ tests/non-free/strnlen2.c:166:[value] assertion got status valid.
[value] Recording results for large
[value] Done for function large
[value] computing for function large_uninit <- main.
- Called from tests/non-free/strnlen2.c:493.
+ Called from tests/non-free/strnlen2.c:518.
[value] computing for function init_array_nondet <- large_uninit <- main.
Called from tests/non-free/strnlen2.c:171.
tests/non-free/strnlen2.c:138:[value] Call to builtin memset(({{ (void *)&a }},{1; 2},{40}))
@@ -148,7 +148,7 @@ tests/non-free/strnlen2.c:187:[value] assertion got status valid.
[value] Recording results for large_uninit
[value] Done for function large_uninit
[value] computing for function misc <- main.
- Called from tests/non-free/strnlen2.c:494.
+ Called from tests/non-free/strnlen2.c:519.
tests/non-free/strnlen2.c:215:[value] Call to builtin Frama_C_strnlen(({{ &unterminated_string[0] }},{13}))
tests/non-free/strnlen2.c:215:[value] warning: builtin Frama_C_strnlen: reading indeterminate data
tests/non-free/strnlen2.c:218:[value] Call to builtin Frama_C_strnlen(({{ "Hello World\n" ; "Bonjour Monde\n" }},
@@ -193,19 +193,19 @@ tests/non-free/strnlen2.c:252:[value] assertion got status valid.
[value] Recording results for misc
[value] Done for function misc
[value] computing for function bitfields <- main.
- Called from tests/non-free/strnlen2.c:495.
+ Called from tests/non-free/strnlen2.c:520.
tests/non-free/strnlen2.c:117:[value] Call to builtin Frama_C_strnlen(({{ (char const *)&s }},{3}))
tests/non-free/strnlen2.c:117:[value] warning: builtin Frama_C_strnlen: reading indeterminate data
[value] Recording results for bitfields
[value] Done for function bitfields
[value] computing for function bitfields2 <- main.
- Called from tests/non-free/strnlen2.c:496.
+ Called from tests/non-free/strnlen2.c:521.
tests/non-free/strnlen2.c:132:[value] Call to builtin Frama_C_strnlen(({{ (char const *)&s }},{3}))
tests/non-free/strnlen2.c:133:[value] assertion got status valid.
[value] Recording results for bitfields2
[value] Done for function bitfields2
[value] computing for function escaping <- main.
- Called from tests/non-free/strnlen2.c:497.
+ Called from tests/non-free/strnlen2.c:522.
tests/non-free/strnlen2.c:196:[value] warning: locals {x} escaping the scope of a block of escaping through s
tests/non-free/strnlen2.c:199:[value] Call to builtin Frama_C_strnlen(({{ &s[0] }},{4}))
tests/non-free/strnlen2.c:199:[value] warning: builtin Frama_C_strnlen: possible escaping addresses
@@ -215,7 +215,7 @@ tests/non-free/strnlen2.c:203:[value] assertion got status valid.
[value] Recording results for escaping
[value] Done for function escaping
[value] computing for function big_array <- main.
- Called from tests/non-free/strnlen2.c:498.
+ Called from tests/non-free/strnlen2.c:523.
tests/non-free/strnlen2.c:261:[value] warning: out of bounds write. assert \valid(p);
tests/non-free/strnlen2.c:263:[value] warning: out of bounds write. assert \valid(p);
tests/non-free/strnlen2.c:265:[value] warning: out of bounds write. assert \valid(p);
@@ -297,7 +297,7 @@ tests/non-free/strnlen2.c:314:[value] Frama_C_show_each: [0..799], [0..803], [0.
[value] Recording results for big_array
[value] Done for function big_array
[value] computing for function no_zero_but_ok <- main.
- Called from tests/non-free/strnlen2.c:500.
+ Called from tests/non-free/strnlen2.c:525.
tests/non-free/strnlen2.c:325:[value] Call to builtin Frama_C_strnlen(({{ &s[0] }},{5}))
tests/non-free/strnlen2.c:326:[value] assertion got status valid.
tests/non-free/strnlen2.c:327:[value] Call to builtin Frama_C_strnlen(({{ &s[0] }},{10}))
@@ -312,7 +312,7 @@ tests/non-free/strnlen2.c:337:[value] assertion got status valid.
[value] Recording results for no_zero_but_ok
[value] Done for function no_zero_but_ok
[value] computing for function small_sets_n <- main.
- Called from tests/non-free/strnlen2.c:501.
+ Called from tests/non-free/strnlen2.c:526.
tests/non-free/strnlen2.c:345:[value] Call to builtin Frama_C_strnlen(({{ "abcde" + {0; 1} }},{2; 5}))
tests/non-free/strnlen2.c:346:[value] assertion got status valid.
tests/non-free/strnlen2.c:351:[value] Call to builtin Frama_C_strnlen(({{ "\000bcdef" + {0; 1} }},{1; 4}))
@@ -326,7 +326,7 @@ tests/non-free/strnlen2.c:367:[value] assertion got status valid.
[value] Recording results for small_sets_n
[value] Done for function small_sets_n
[value] computing for function large_n <- main.
- Called from tests/non-free/strnlen2.c:502.
+ Called from tests/non-free/strnlen2.c:527.
[value] computing for function init_array_nondet <- large_n <- main.
Called from tests/non-free/strnlen2.c:372.
tests/non-free/strnlen2.c:138:[value] Call to builtin memset(({{ (void *)&a }},{1; 2},{100}))
@@ -386,7 +386,7 @@ tests/non-free/strnlen2.c:415:[value] assertion got status valid.
[value] Recording results for large_n
[value] Done for function large_n
[value] computing for function unbounded_n <- main.
- Called from tests/non-free/strnlen2.c:504.
+ Called from tests/non-free/strnlen2.c:529.
tests/non-free/strnlen2.c:423:[value] Call to builtin Frama_C_strnlen(({{ "abc" }},[0..2147483647]))
tests/non-free/strnlen2.c:424:[value] assertion got status valid.
tests/non-free/strnlen2.c:426:[value] Call to builtin Frama_C_strnlen(({{ "abc" + {0; 1} }},[0..2147483647]))
@@ -396,7 +396,7 @@ tests/non-free/strnlen2.c:430:[value] assertion got status valid.
[value] Recording results for unbounded_n
[value] Done for function unbounded_n
[value] computing for function intervals <- main.
- Called from tests/non-free/strnlen2.c:505.
+ Called from tests/non-free/strnlen2.c:530.
[value] computing for function init_array_nondet <- intervals <- main.
Called from tests/non-free/strnlen2.c:435.
tests/non-free/strnlen2.c:138:[value] Call to builtin memset(({{ (void *)&a }},{0; 1},{10}))
@@ -516,6 +516,49 @@ tests/non-free/strnlen2.c:483:[value] warning: builtin Frama_C_strnlen:
tests/non-free/strnlen2.c:484:[value] assertion got status valid.
[value] Recording results for intervals
[value] Done for function intervals
+[value] computing for function negative_offsets <- main.
+ Called from tests/non-free/strnlen2.c:532.
+tests/non-free/strnlen2.c:489:[value] entering loop for the first time
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strnlen2.c:493.
+[value] Done for function Frama_C_interval
+tests/non-free/strnlen2.c:494:[value] Call to builtin Frama_C_strnlen(({{ &buf{[-10], [-9], [-8]} }},{100}))
+tests/non-free/strnlen2.c:494:[value] warning: builtin Frama_C_strnlen: reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strnlen2.c:497.
+[value] Done for function Frama_C_interval
+tests/non-free/strnlen2.c:498:[value] Call to builtin Frama_C_strnlen(({{ &buf{[-2], [-1]} }},{100}))
+tests/non-free/strnlen2.c:498:[value] warning: builtin Frama_C_strnlen: reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strnlen2.c:500.
+[value] Done for function Frama_C_interval
+tests/non-free/strnlen2.c:501:[value] Call to builtin Frama_C_strnlen(({{ &buf{[-1], [0]} }},{100}))
+tests/non-free/strnlen2.c:501:[value] warning: builtin Frama_C_strnlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strnlen2.c:502.
+[value] Done for function Frama_C_interval
+tests/non-free/strnlen2.c:503:[value] Call to builtin Frama_C_strnlen(({{ &buf{[-1], [0], [1], [2]} }},{100}))
+tests/non-free/strnlen2.c:503:[value] warning: builtin Frama_C_strnlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strnlen2.c:504.
+[value] Done for function Frama_C_interval
+tests/non-free/strnlen2.c:505:[value] Call to builtin Frama_C_strnlen(({{ &buf + [-4..7] }},{100}))
+tests/non-free/strnlen2.c:505:[value] warning: builtin Frama_C_strnlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] computing for function Frama_C_interval <- negative_offsets <- main.
+ Called from tests/non-free/strnlen2.c:506.
+[value] Done for function Frama_C_interval
+tests/non-free/strnlen2.c:508:[value] Call to builtin Frama_C_strnlen(({{ &buf + [-10..0] }},{100}))
+tests/non-free/strnlen2.c:508:[value] warning: builtin Frama_C_strnlen:
+ possible uninitialized values
+ possibly reading indeterminate data
+[value] Recording results for negative_offsets
+[value] Done for function negative_offsets
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
@@ -661,6 +704,21 @@ tests/non-free/strnlen2.c:484:[value] assertion got status valid.
s2 ∈ {{ "efg" + {1; 2} ; "EFGH" + {1; 2} }}
maybe_init[0] ∈ {65} or UNINITIALIZED
[1] ∈ {0}
+[value:final-states] Values at end of function negative_offsets:
+ Frama_C_entropy_source ∈ [--..--]
+ buf[0..98] ∈ {65} or UNINITIALIZED
+ [99] ∈ {0}
+ len1 ∈ UNINITIALIZED
+ len2 ∈ UNINITIALIZED
+ len3 ∈ {99}
+ len4 ∈ {97; 98; 99}
+ len5 ∈ {92; 93; 94; 95; 96; 97; 98; 99}
+ len6 ∈ {99}
+ offset3 ∈ {-1; 0}
+ offset4 ∈ {-1; 0; 1; 2}
+ offset5 ∈ [-4..7]
+ offset6 ∈ [-10..0]
+ p ∈ {{ &buf + [-10..0] }}
[value:final-states] Values at end of function no_zero_but_ok:
s[0..9] ∈ {1}
[10] ∈ {0}
@@ -738,6 +796,8 @@ tests/non-free/strnlen2.c:484:[value] assertion got status valid.
[from] Done for function large_uninit
[from] Computing for function misc
[from] Done for function misc
+[from] Computing for function negative_offsets
+[from] Done for function negative_offsets
[from] Computing for function no_zero_but_ok
[from] Done for function no_zero_but_ok
[from] Computing for function small_sets
@@ -771,7 +831,7 @@ tests/non-free/strnlen2.c:484:[value] assertion got status valid.
uninitialized[0]; s[0..1]; t[0..3]; s; s; a[3..99]; a[3..99];
s[0..3]; loc_char_array[0..4]; x; maybe_init[0..1]; u[0..199];
r[0..200]; t[0..999999]; s[0..19]; a[0..99]; a[0..99];
- "Hello World\n"[bits 0 to 103];
+ buf[0..99]; "Hello World\n"[bits 0 to 103];
"abc\000\000\000abc"[bits 0 to 79]; ""[bits 0 to 7];
"a"[bits 0 to 15]; "aa"[bits 0 to 23]; "aaa";
"aaaa"[bits 0 to 39]; "aaaaa"[bits 0 to 47];
@@ -812,6 +872,8 @@ tests/non-free/strnlen2.c:484:[value] assertion got status valid.
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function misc:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function negative_offsets:
+ Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
[from] Function no_zero_but_ok:
NO EFFECTS
[from] Function small_sets:
@@ -823,7 +885,7 @@ tests/non-free/strnlen2.c:484:[value] assertion got status valid.
[from] Function zero_termination:
NO EFFECTS
[from] Function main:
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function bitfields:
@@ -888,6 +950,11 @@ tests/non-free/strnlen2.c:484:[value] assertion got status valid.
"Bonjour Monde\n"[bits 0 to 119]; "abc"; "ABCD"[bits 0 to 39];
"efg"[bits 8 to 31]; "EFGH"[bits 8 to 39]; "mno\000pqr"[bits 0 to 63];
"MNOP\000QRS"[bits 0 to 71]
+[inout] Out (internal) for function negative_offsets:
+ Frama_C_entropy_source; buf[0..99]; i; len1; len2; len3; len4; len5;
+ len6; offset1; offset2; offset3; offset4; offset5; offset6; p
+[inout] Inputs for function negative_offsets:
+ Frama_C_entropy_source; nondet
[inout] Out (internal) for function no_zero_but_ok:
s[0..19]; z1; tmp; z2; tmp_0; p; tmp_1; z3; tmp_2; z4; tmp_3; z5; tmp_4
[inout] Inputs for function no_zero_but_ok:
diff --git a/tests/non-free/strlen.c b/tests/non-free/strlen.c
index 887f163f6ea..f45980a6d36 100644
--- a/tests/non-free/strlen.c
+++ b/tests/non-free/strlen.c
@@ -305,6 +305,31 @@ void big_array () {
Frama_C_show_each(len_u, len_r, len_t);
}
+void negative_offsets() {
+ char buf[100];
+ for (int i = 0; i < 100; i++) buf[i] = 'A'; //avoid memset due to C++ oracles
+ buf[99] = 0;
+ unsigned len1, len2, len3, len4, len5, len6;
+ if (nondet) {
+ int offset1 = Frama_C_interval(-10, -8);
+ len1 = strlen(buf + offset1);
+ }
+ if (nondet) {
+ int offset2 = Frama_C_interval(-2, -1);
+ len2 = strlen(buf + offset2);
+ }
+ int offset3 = Frama_C_interval(-1, -0);
+ len3 = strlen(buf + offset3);
+ int offset4 = Frama_C_interval(-1, 2);
+ len4 = strlen(buf + offset4);
+ int offset5 = Frama_C_interval(-4, 7);
+ len5 = strlen(buf + offset5);
+ int offset6 = Frama_C_interval(-10, 0);
+ char *p = buf + offset6;
+ len6 = strlen(p);
+ char dest[100 * 2];
+}
+
int main (int c) {
small_sets();
zero_termination();
@@ -316,5 +341,6 @@ int main (int c) {
bitfields2();
escaping();
big_array();
+ negative_offsets();
return 0;
}
diff --git a/tests/non-free/strnlen2.c b/tests/non-free/strnlen2.c
index 375dcf63561..dd3a006258b 100644
--- a/tests/non-free/strnlen2.c
+++ b/tests/non-free/strnlen2.c
@@ -484,6 +484,31 @@ void intervals() {
//@ assert z9 >= 0 && z9 <= 9;
}
+void negative_offsets() {
+ char buf[100];
+ for (int i = 0; i < 100; i++) buf[i] = 'A'; //avoid memset due to C++ oracles
+ buf[99] = 0;
+ unsigned len1, len2, len3, len4, len5, len6;
+ if (nondet) {
+ int offset1 = Frama_C_interval(-10, -8);
+ len1 = strnlen(buf + offset1, 100);
+ }
+ if (nondet) {
+ int offset2 = Frama_C_interval(-2, -1);
+ len2 = strnlen(buf + offset2, 100);
+ }
+ int offset3 = Frama_C_interval(-1, -0);
+ len3 = strnlen(buf + offset3, 100);
+ int offset4 = Frama_C_interval(-1, 2);
+ len4 = strnlen(buf + offset4, 100);
+ int offset5 = Frama_C_interval(-4, 7);
+ len5 = strnlen(buf + offset5, 100);
+ int offset6 = Frama_C_interval(-10, 0);
+ char *p = buf + offset6;
+ len6 = strnlen(p, 100);
+ char dest[100 * 2];
+}
+
int main (int c) {
small_sets();
zero_termination();
@@ -504,5 +529,6 @@ int main (int c) {
unbounded_n();
intervals();
+ negative_offsets();
return 0;
}
--
GitLab