Skip to content
Snippets Groups Projects
Commit c12b257a authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[Eva] Reorganizes strings.i test to only perform one Eva run.

parent 27598ddf
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/oracle/strings.0.res.oracle deleted 100644 → 0
+ 0
− 152
View file @ 27598ddf
[kernel] Parsing tests/value/strings.i (no preprocessing)
[eva] Analyzing a complete application starting at main1
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
s1[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {32}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
s2[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
s5 ∈ {0}
s6 ∈ {0}
cc ∈ {97}
Q ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0}
Y ∈ {0}
Z ∈ {0}
s3 ∈ {{ "tutu" }}
s4 ∈ {{ "tutu" }}
s7 ∈ {{ "hello\000 world" }}
s8 ∈ {{ "hello" }}
[eva] computing for function u <- main1.
Called from tests/value/strings.i:39.
[kernel:annot:missing-spec] tests/value/strings.i:39: Warning:
Neither code nor specification for function u, generating default assigns from the prototype
[eva] using specification for function u
[eva] Done for function u
[eva:alarm] tests/value/strings.i:39: Warning:
out of bounds read. assert \valid_read(p - 4);
[eva] computing for function u <- main1.
Called from tests/value/strings.i:42.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:42: Warning:
out of bounds read. assert \valid_read(p + 12);
[eva] computing for function u <- main1.
Called from tests/value/strings.i:44.
[eva] Done for function u
[eva] computing for function u <- main1.
Called from tests/value/strings.i:48.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:48: Warning:
out of bounds read. assert \valid_read(p - 4);
[eva] computing for function u <- main1.
Called from tests/value/strings.i:53.
[eva] Done for function u
[eva] computing for function strcpy <- main1.
Called from tests/value/strings.i:53.
[eva:alarm] tests/value/strings.i:21: Warning:
out of bounds write.
assert \valid(tmp_unroll_46);
(tmp_unroll_46 from ldst++)
[kernel] tests/value/strings.i:21: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for strcpy
[eva] Done for function strcpy
[eva] computing for function strlen <- main1.
Called from tests/value/strings.i:58.
[eva] Recording results for strlen
[eva] Done for function strlen
[eva] Recording results for main1
[eva] done for function main1
[eva] tests/value/strings.i:21:
assertion 'Eva,mem_access' got final status invalid.
[eva] tests/value/strings.i:39:
assertion 'Eva,mem_access' got final status invalid.
[eva] tests/value/strings.i:42:
assertion 'Eva,mem_access' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function strcpy:
NON TERMINATING FUNCTION
[eva:final-states] Values at end of function strlen:
s ∈ {{ &s1[6] }}
l ∈ {5}
[eva:final-states] Values at end of function main1:
s1[0] ∈ {104}
[1] ∈ {101}
[2] ∈ {108}
[3] ∈ {97}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {97}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0; 101}
p ∈ {{ &s1[5] ; &s2[3] }}
__retres ∈ {5}
[from] Computing for function strcpy
[from] Non-terminating function strcpy (no dependencies)
[from] Done for function strcpy
[from] Computing for function strlen
[from] Done for function strlen
[from] Computing for function main1
[from] Computing for function u <-main1
[from] Done for function u
[from] Done for function main1
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function strcpy:
NON TERMINATING - NO EFFECTS
[from] Function strlen:
\result FROM s1[0..4]; s
[from] Function u:
\result FROM \nothing
[from] Function main1:
s1{[3]; [6]} FROM cc
R FROM \nothing (and SELF)
S FROM \nothing (and SELF)
T FROM s1[1] (and SELF)
\result FROM s1{[0..2]; [4]}; cc
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function strcpy:
src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
[inout] Inputs for function strcpy:
a[0..5]
[inout] Out (internal) for function strlen:
s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
tmp_unroll_118; tmp_unroll_121
[inout] Inputs for function strlen:
s1[0..5]
[inout] Out (internal) for function main1:
s1{[3]; [6]}; R; S; T; p; tmp; tmp_0; tmp_1; tmp_2; a[0..9]; b[0..4];
tmp_3; tmp_4; __retres
[inout] Inputs for function main1:
s1[0..5]; cc
tests/value/oracle/strings.1.res.oracle deleted 100644 → 0
+ 0
− 145
View file @ 27598ddf
[kernel] Parsing tests/value/strings.i (no preprocessing)
[eva] Analyzing a complete application starting at main6
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
s1[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {32}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
s2[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
s5 ∈ {0}
s6 ∈ {0}
cc ∈ {97}
Q ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0}
Y ∈ {0}
Z ∈ {0}
s3 ∈ {{ "tutu" }}
s4 ∈ {{ "tutu" }}
s7 ∈ {{ "hello\000 world" }}
s8 ∈ {{ "hello" }}
[eva] computing for function u <- main6.
Called from tests/value/strings.i:72.
[kernel:annot:missing-spec] tests/value/strings.i:72: Warning:
Neither code nor specification for function u, generating default assigns from the prototype
[eva] using specification for function u
[eva] Done for function u
[eva:alarm] tests/value/strings.i:73: Warning:
pointer comparison. assert \pointer_comparable((void *)s3, (void *)s4);
[eva] computing for function u <- main6.
Called from tests/value/strings.i:74.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:76.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:78.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:79: Warning:
pointer comparison. assert \pointer_comparable((void *)s7, (void *)s8);
[eva] computing for function u <- main6.
Called from tests/value/strings.i:80.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:82.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:83: Warning:
pointer comparison.
assert \pointer_comparable((void *)(s7 + 1), (void *)(s8 + 1));
[eva] computing for function u <- main6.
Called from tests/value/strings.i:84.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:86.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:87.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:88.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:89.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:89.
[eva] Done for function u
[eva] computing for function u <- main6.
Called from tests/value/strings.i:90.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:91: Warning:
pointer comparison. assert \pointer_comparable((void *)s5, (void *)s6);
[eva] computing for function u <- main6.
Called from tests/value/strings.i:92.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:93: Warning:
pointer comparison.
assert \pointer_comparable((void *)("oh, hello" + 4), (void *)s7);
[eva] Recording results for main6
[eva] done for function main6
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main6:
s5 ∈ {{ "tutu" ; "hello" }}
s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
cc ∈ {116}
Q ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0; 1}
Y ∈ {0; 1}
Z ∈ {0; 1}
s ∈ {{ "toto" }}
__retres ∈ {116}
[from] Computing for function main6
[from] Computing for function u <-main6
[from] Done for function u
[from] Done for function main6
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function u:
\result FROM \nothing
[from] Function main6:
s5 FROM s3; s8
s6 FROM s3; s4; s8
cc FROM "toto"[bits 0 to 7]
Q FROM s7 (and SELF)
R FROM s3; s4 (and SELF)
S FROM \nothing (and SELF)
T FROM s3 (and SELF)
U FROM s7; s8 (and SELF)
V FROM s4; s7 (and SELF)
W FROM s7; s8 (and SELF)
X FROM s3 (and SELF)
Y FROM s3; s8 (and SELF)
Z FROM s3; s4; s8 (and SELF)
\result FROM "toto"[bits 0 to 7]
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main6:
s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z; s; tmp; tmp_0; tmp_1; tmp_2;
tmp_3; tmp_4; tmp_5; tmp_6; tmp_7; tmp_8; tmp_9; tmp_10; tmp_11; tmp_12;
tmp_13; tmp_14; __retres
[inout] Inputs for function main6:
s5; s6; cc; s3; s4; s7; s8; "toto"[bits 0 to 7]
tests/value/oracle/strings.2.res.oracle deleted 100644 → 0
+ 0
− 69
View file @ 27598ddf
[kernel] Parsing tests/value/strings.i (no preprocessing)
[eva] Analyzing a complete application starting at main7
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
s1[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {32}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
s2[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
s5 ∈ {0}
s6 ∈ {0}
cc ∈ {97}
Q ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0}
Y ∈ {0}
Z ∈ {0}
s3 ∈ {{ "tutu" }}
s4 ∈ {{ "tutu" }}
s7 ∈ {{ "hello\000 world" }}
s8 ∈ {{ "hello" }}
[eva:alarm] tests/value/strings.i:101: Warning:
out of bounds write. assert \valid(tmp);
(tmp from f?s5 + 2:& c)
[eva:alarm] tests/value/strings.i:103: Warning:
out of bounds write. assert \valid(s5);
[eva:alarm] tests/value/strings.i:105: Warning:
out of bounds write. assert \valid(s6);
[eva] Recording results for main7
[eva] done for function main7
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main7:
s5 ∈ {{ &c }}
s6 ∈ {{ &c }}
R ∈ {84}
c ∈ {116}
__retres ∈ {116}
[from] Computing for function main7
[from] Done for function main7
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function main7:
s5 FROM s3; d
s6 FROM s3; e
R FROM s3; d; f
\result FROM s4; "tutu"[bits 0 to 7]
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main7:
s5; s6; R; c; tmp; __retres
[inout] Inputs for function main7:
s5; s6; cc; s3; s4; "tutu"[bits 0 to 7]
tests/value/oracle/strings.3.res.oracle deleted 100644 → 0
+ 0
− 114
View file @ 27598ddf
[kernel] Parsing tests/value/strings.i (no preprocessing)
[eva] Analyzing a complete application starting at main8
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
s1[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {32}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
s2[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
s5 ∈ {0}
s6 ∈ {0}
cc ∈ {97}
Q ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0}
Y ∈ {0}
Z ∈ {0}
s3 ∈ {{ "tutu" }}
s4 ∈ {{ "tutu" }}
s7 ∈ {{ "hello\000 world" }}
s8 ∈ {{ "hello" }}
[eva] computing for function assigns <- main8.
Called from tests/value/strings.i:127.
[eva] using specification for function assigns
[eva] tests/value/strings.i:121: Warning:
no \from part for clause 'assigns *(p + (0 .. s - 1));'
[eva] Done for function assigns
[eva] computing for function strcmp <- main8.
Called from tests/value/strings.i:128.
[eva:alarm] tests/value/strings.i:114: Warning:
out of bounds read. assert \valid_read(tmp_0);
(tmp_0 from s2_0++)
[eva] Recording results for strcmp
[eva] Done for function strcmp
[eva] Recording results for main8
[eva] done for function main8
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function strcmp:
s1_0 ∈ {{ &long_chain + [0..29] }}
s2_0 ∈ {{ &tc + [0..29] }}
__retres ∈ [-223..121]
[eva:final-states] Values at end of function main8:
tc[0..29] ∈ [--..--]
long_chain[0] ∈ {114}
[1] ∈ {101}
[2] ∈ {97}
[3..4] ∈ {108}
[5] ∈ {121}
[6] ∈ {32}
[7] ∈ {114}
[8] ∈ {101}
[9] ∈ {97}
[10..11] ∈ {108}
[12] ∈ {121}
[13] ∈ {32}
[14] ∈ {114}
[15] ∈ {101}
[16] ∈ {97}
[17..18] ∈ {108}
[19] ∈ {121}
[20] ∈ {32}
[21] ∈ {108}
[22] ∈ {111}
[23] ∈ {110}
[24] ∈ {103}
[25] ∈ {32}
[26] ∈ {99}
[27] ∈ {104}
[28] ∈ {97}
[29] ∈ {105}
[30] ∈ {110}
[31] ∈ {0}
x ∈ [-223..121]
[from] Computing for function strcmp
[from] Done for function strcmp
[from] Computing for function main8
[from] Computing for function assigns <-main8
[from] Done for function assigns
[from] Done for function main8
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function assigns:
tc[0..29] FROM ANYTHING(origin:Unknown) (and SELF)
[from] Function strcmp:
\result FROM s1_0; s2_0; tc[0..29]; long_chain[0..30]
[from] Function main8:
\result FROM ANYTHING(origin:Unknown)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function strcmp:
s1_0; s2_0; tmp; tmp_0; __retres
[inout] Inputs for function strcmp:
tc[0..29]; long_chain[0..30]
[inout] Out (internal) for function main8:
tc[0..29]; long_chain[0..31]; x
[inout] Inputs for function main8:
ANYTHING(origin:Unknown)
tests/value/oracle/strings.res.oracle 0 → 100644
+ 407
− 0
View file @ c12b257a
[kernel] Parsing tests/value/strings.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
s1[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {32}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
s2[0] ∈ {104}
[1] ∈ {101}
[2..3] ∈ {108}
[4] ∈ {111}
[5] ∈ {0}
s3 ∈ {{ "tutu" }}
s4 ∈ {{ "tutu" }}
s5 ∈ {0}
s6 ∈ {0}
s7 ∈ {{ "hello\000 world" }}
s8 ∈ {{ "hello" }}
cc ∈ {97}
Q ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0}
Y ∈ {0}
Z ∈ {0}
[eva] computing for function string_reads <- main.
Called from tests/value/strings.i:127.
[eva] computing for function u <- string_reads <- main.
Called from tests/value/strings.i:39.
[kernel:annot:missing-spec] tests/value/strings.i:39: Warning:
Neither code nor specification for function u, generating default assigns from the prototype
[eva] using specification for function u
[eva] Done for function u
[eva:alarm] tests/value/strings.i:39: Warning:
out of bounds read. assert \valid_read(p - 4);
[eva] computing for function u <- string_reads <- main.
Called from tests/value/strings.i:42.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:42: Warning:
out of bounds read. assert \valid_read(p + 12);
[eva] computing for function u <- string_reads <- main.
Called from tests/value/strings.i:44.
[eva] Done for function u
[eva] computing for function u <- string_reads <- main.
Called from tests/value/strings.i:48.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:48: Warning:
out of bounds read. assert \valid_read(p - 4);
[eva] computing for function u <- string_reads <- main.
Called from tests/value/strings.i:53.
[eva] Done for function u
[eva] computing for function strcpy <- string_reads <- main.
Called from tests/value/strings.i:53.
[eva:alarm] tests/value/strings.i:23: Warning:
out of bounds write.
assert \valid(tmp_unroll_46);
(tmp_unroll_46 from ldst++)
[kernel] tests/value/strings.i:23: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for strcpy
[eva] Done for function strcpy
[eva] computing for function strlen <- string_reads <- main.
Called from tests/value/strings.i:58.
[eva] Recording results for strlen
[eva] Done for function strlen
[eva] Recording results for string_reads
[eva] Done for function string_reads
[eva] computing for function string_writes <- main.
Called from tests/value/strings.i:128.
[eva:alarm] tests/value/strings.i:64: Warning:
out of bounds write. assert \valid(tmp);
(tmp from nondet?s5 + 2:& c)
[eva:alarm] tests/value/strings.i:66: Warning:
out of bounds write. assert \valid(s5);
[eva:alarm] tests/value/strings.i:68: Warning:
out of bounds write. assert \valid(s6);
[eva] Recording results for string_writes
[eva] Done for function string_writes
[eva:locals-escaping] tests/value/strings.i:128: Warning:
locals {c} escaping the scope of string_writes through s5
[eva:locals-escaping] tests/value/strings.i:128: Warning:
locals {c} escaping the scope of string_writes through s6
[eva] computing for function string_comparison <- main.
Called from tests/value/strings.i:129.
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:78.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:79: Warning:
pointer comparison. assert \pointer_comparable((void *)s3, (void *)s4);
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:80.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:82.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:84.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:85: Warning:
pointer comparison. assert \pointer_comparable((void *)s7, (void *)s8);
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:86.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:88.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:89: Warning:
pointer comparison.
assert \pointer_comparable((void *)(s7 + 1), (void *)(s8 + 1));
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:90.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:92.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:93.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:94.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:95.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:95.
[eva] Done for function u
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:96.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:97: Warning:
pointer comparison. assert \pointer_comparable((void *)s5, (void *)s6);
[eva] computing for function u <- string_comparison <- main.
Called from tests/value/strings.i:98.
[eva] Done for function u
[eva:alarm] tests/value/strings.i:99: Warning:
pointer comparison.
assert \pointer_comparable((void *)("oh, hello" + 4), (void *)s7);
[eva] Recording results for string_comparison
[eva] Done for function string_comparison
[eva] computing for function long_chain <- main.
Called from tests/value/strings.i:130.
[eva] computing for function assigns <- long_chain <- main.
Called from tests/value/strings.i:120.
[eva] using specification for function assigns
[eva] tests/value/strings.i:114: Warning:
no \from part for clause 'assigns *(p + (0 .. s - 1));'
[eva] Done for function assigns
[eva] computing for function strcmp <- long_chain <- main.
Called from tests/value/strings.i:121.
[eva:alarm] tests/value/strings.i:108: Warning:
out of bounds read. assert \valid_read(tmp_0);
(tmp_0 from s2_0++)
[eva] Recording results for strcmp
[eva] Done for function strcmp
[eva] Recording results for long_chain
[eva] Done for function long_chain
[eva] Recording results for main
[eva] done for function main
[eva] tests/value/strings.i:23:
assertion 'Eva,mem_access' got final status invalid.
[eva] tests/value/strings.i:39:
assertion 'Eva,mem_access' got final status invalid.
[eva] tests/value/strings.i:42:
assertion 'Eva,mem_access' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function strcmp:
s1_0 ∈ {{ &long_chain_0 + [0..29] }}
s2_0 ∈ {{ &tc + [0..29] }}
__retres ∈ [-223..121]
[eva:final-states] Values at end of function long_chain:
tc[0..29] ∈ [--..--]
long_chain_0[0] ∈ {114}
[1] ∈ {101}
[2] ∈ {97}
[3..4] ∈ {108}
[5] ∈ {121}
[6] ∈ {32}
[7] ∈ {114}
[8] ∈ {101}
[9] ∈ {97}
[10..11] ∈ {108}
[12] ∈ {121}
[13] ∈ {32}
[14] ∈ {114}
[15] ∈ {101}
[16] ∈ {97}
[17..18] ∈ {108}
[19] ∈ {121}
[20] ∈ {32}
[21] ∈ {108}
[22] ∈ {111}
[23] ∈ {110}
[24] ∈ {103}
[25] ∈ {32}
[26] ∈ {99}
[27] ∈ {104}
[28] ∈ {97}
[29] ∈ {105}
[30] ∈ {110}
[31] ∈ {0}
x ∈ [-223..121]
[eva:final-states] Values at end of function strcpy:
NON TERMINATING FUNCTION
[eva:final-states] Values at end of function string_writes:
s5 ∈ {{ &c }}
s6 ∈ {{ &c }}
R ∈ {84}
c ∈ {116}
__retres ∈ {116}
[eva:final-states] Values at end of function strlen:
s ∈ {{ &s1[6] }}
l ∈ {5}
[eva:final-states] Values at end of function string_comparison:
s5 ∈ {{ "tutu" ; "hello" }}
s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
cc ∈ {116}
Q ∈ {0}
R ∈ {0; 84}
S ∈ {0}
T ∈ {0; 101}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0; 1}
Y ∈ {0; 1}
Z ∈ {0; 1}
s ∈ {{ "toto" }}
__retres ∈ {116}
[eva:final-states] Values at end of function string_reads:
s1[0] ∈ {104}
[1] ∈ {101}
[2] ∈ {108}
[3] ∈ {97}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {97}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
R ∈ {0}
S ∈ {0}
T ∈ {0; 101}
p ∈ {{ &s1[5] ; &s2[3] }}
__retres ∈ {5}
[eva:final-states] Values at end of function main:
s1[0] ∈ {104}
[1] ∈ {101}
[2] ∈ {108}
[3] ∈ {97}
[4] ∈ {111}
[5] ∈ {0}
[6] ∈ {97}
[7] ∈ {119}
[8] ∈ {111}
[9] ∈ {114}
[10] ∈ {108}
[11] ∈ {100}
[12] ∈ {0}
s5 ∈ {{ "tutu" ; "hello" }}
s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
cc ∈ {116}
Q ∈ {0}
R ∈ {0; 84}
S ∈ {0}
T ∈ {0; 101}
U ∈ {0}
V ∈ {0}
W ∈ {0}
X ∈ {0; 1}
Y ∈ {0; 1}
Z ∈ {0; 1}
[from] Computing for function strcmp
[from] Done for function strcmp
[from] Computing for function long_chain
[from] Computing for function assigns <-long_chain
[from] Done for function assigns
[from] Done for function long_chain
[from] Computing for function strcpy
[from] Non-terminating function strcpy (no dependencies)
[from] Done for function strcpy
[from] Computing for function string_writes
[from] Done for function string_writes
[from] Computing for function strlen
[from] Done for function strlen
[from] Computing for function string_comparison
[from] Computing for function u <-string_comparison
[from] Done for function u
[from] Done for function string_comparison
[from] Computing for function string_reads
[from] Done for function string_reads
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function assigns:
tc[0..29] FROM ANYTHING(origin:Unknown) (and SELF)
[from] Function strcmp:
\result FROM s1_0; s2_0; tc[0..29]; long_chain_0[0..30]
[from] Function long_chain:
\result FROM ANYTHING(origin:Unknown)
[from] Function strcpy:
NON TERMINATING - NO EFFECTS
[from] Function string_writes:
s5 FROM nondet; s3
s6 FROM nondet; s3
R FROM nondet; s3
\result FROM s4; "tutu"[bits 0 to 7]
[from] Function strlen:
\result FROM s1[0..4]; s
[from] Function u:
\result FROM \nothing
[from] Function string_comparison:
s5 FROM s3; s8
s6 FROM s3; s4; s8
cc FROM "toto"[bits 0 to 7]
Q FROM s7 (and SELF)
R FROM s3; s4 (and SELF)
S FROM \nothing (and SELF)
T FROM s3 (and SELF)
U FROM s7; s8 (and SELF)
V FROM s4; s7 (and SELF)
W FROM s7; s8 (and SELF)
X FROM s3 (and SELF)
Y FROM s3; s8 (and SELF)
Z FROM s3; s4; s8 (and SELF)
\result FROM "toto"[bits 0 to 7]
[from] Function string_reads:
s1{[3]; [6]} FROM cc
R FROM \nothing (and SELF)
S FROM \nothing (and SELF)
T FROM s1[1] (and SELF)
\result FROM s1{[0..2]; [4]}; cc
[from] Function main:
s1{[3]; [6]} FROM cc
s5 FROM s3; s8
s6 FROM s3; s4; s8
cc FROM "toto"[bits 0 to 7]
Q FROM s7 (and SELF)
R FROM nondet; s3; s4
S FROM \nothing (and SELF)
T FROM s1[1]; s3 (and SELF)
U FROM s7; s8 (and SELF)
V FROM s4; s7 (and SELF)
W FROM s7; s8 (and SELF)
X FROM s3 (and SELF)
Y FROM s3; s8 (and SELF)
Z FROM s3; s4; s8 (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function strcmp:
s1_0; s2_0; tmp; tmp_0; __retres
[inout] Inputs for function strcmp:
tc[0..29]; long_chain_0[0..30]
[inout] Out (internal) for function long_chain:
tc[0..29]; long_chain_0[0..31]; x
[inout] Inputs for function long_chain:
ANYTHING(origin:Unknown)
[inout] Out (internal) for function strcpy:
src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
[inout] Inputs for function strcpy:
a[0..5]
[inout] Out (internal) for function string_writes:
s5; s6; R; c; tmp; __retres
[inout] Inputs for function string_writes:
nondet; s3; s4; s5; s6; cc; "tutu"[bits 0 to 7]
[inout] Out (internal) for function strlen:
s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
tmp_unroll_118; tmp_unroll_121
[inout] Inputs for function strlen:
s1[0..5]
[inout] Out (internal) for function string_comparison:
s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z; s; tmp; tmp_0; tmp_1; tmp_2;
tmp_3; tmp_4; tmp_5; tmp_6; tmp_7; tmp_8; tmp_9; tmp_10; tmp_11; tmp_12;
tmp_13; tmp_14; __retres
[inout] Inputs for function string_comparison:
s3; s4; s5; s6; s7; s8; cc; "toto"[bits 0 to 7]
[inout] Out (internal) for function string_reads:
s1{[3]; [6]}; R; S; T; p; tmp; tmp_0; tmp_1; tmp_2; a[0..9]; b[0..4];
tmp_3; tmp_4; __retres
[inout] Inputs for function string_reads:
s1[0..5]; cc
[inout] Out (internal) for function main:
s1{[3]; [6]}; s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z
[inout] Inputs for function main:
ANYTHING(origin:Unknown)
tests/value/strings.i
+ 41
− 40
View file @ c12b257a
/* run.config* /* run.config*
GCC: STDOPT: #"-eva-no-builtins-auto -eva-slevel-function strcmp:50"
STDOPT: #"-main main1 -eva-no-builtins-auto"
STDOPT: #"-main main6 -eva-no-builtins-auto"
STDOPT: #"-main main7 -eva-no-builtins-auto"
STDOPT: #"-main main8 -slevel-function strcmp:50 -eva-no-builtins-auto"
*/ */
volatile int nondet;
char s1[]="hello\000 world"; char s1[]="hello\000 world";
char s2[]="hello"; char s2[]="hello";
char *s3="tutu";
char *s4="tutu";
char *s5, *s6; char *s5, *s6;
char *s7="hello\x00 world";
char *s8="hello";
int u(void); int u(void);
char cc = 'a'; char cc = 'a';
char Q, R, S, T, U, V, W, X, Y, Z; char Q, R, S, T, U, V, W, X, Y, Z;
char *strcpy(char*dst, char*src) char *strcpy(char*dst, char*src) {
{
char* ldst=dst; char* ldst=dst;
/*@ loop pragma UNROLL 20; */ /*@ loop pragma UNROLL 20; */
while (*ldst++ = *src++) while (*ldst++ = *src++)
...@@ -23,8 +25,7 @@ char *strcpy(char*dst, char*src) ...@@ -23,8 +25,7 @@ char *strcpy(char*dst, char*src)
return dst; return dst;
} }
unsigned int strlen(char *s) unsigned int strlen(char *s) {
{
unsigned int l=0; unsigned int l=0;
/*@ loop pragma UNROLL 20; */ /*@ loop pragma UNROLL 20; */
while(*s++ != 0) while(*s++ != 0)
...@@ -32,8 +33,7 @@ unsigned int strlen(char *s) ...@@ -32,8 +33,7 @@ unsigned int strlen(char *s)
return l; return l;
} }
int main1(void) int string_reads() {
{
char *p; char *p;
p = &s1[3]; p = &s1[3];
if (u()) R=*(p-4); if (u()) R=*(p-4);
...@@ -48,24 +48,30 @@ int main1(void) ...@@ -48,24 +48,30 @@ int main1(void)
if (u()) T=*(p-4); if (u()) T=*(p-4);
{ {
char a[10] = "Not ok"; char a[10] = "Not ok";
char b [5]; char b [5];
if (u()) strcpy(b,a); if (u()) strcpy(b,a);
} }
s1[3]=cc; s1[3]=cc;
s1[6]=cc; s1[6]=cc;
return strlen(s1); return strlen(s1);
} }
int string_writes() {
char c=-1;
if (nondet) s5 = s3; else s5 = &c;
*(nondet ? s5 + 2 : &c) = 'T';
R=c;
*s5=' ';
if (nondet) s6 = s3+1; else s6 = &c;
*s6=cc;
c=*s4;
return c;
}
char *s3="tutu";
char *s4="tutu";
char *s7="hello\x00 world";
char *s8="hello";
int main6(void) int string_comparison() {
{
char *s; char *s;
s = "toto"; s = "toto";
cc = *s; cc = *s;
...@@ -82,30 +88,18 @@ int main6(void) ...@@ -82,30 +88,18 @@ int main6(void)
if (u()) if (u())
W = (s7 + 1 == s8 + 1); W = (s7 + 1 == s8 + 1);
if (u()) if (u())
X = (s3 == s3); X = (s3 == s3);
s5 = (u()?s3:s8); s5 = (u()?s3:s8);
if (u()) if (u())
Y = ((u()?s3:s8) == s5); Y = ((u()?s3:s8) == s5);
s6 = (u()?(u()?s3:s8):s4); s6 = (u()?(u()?s3:s8):s4);
if (u()) if (u())
Z = (s5 == s6); Z = (s5 == s6);
if (u()) if (u())
Q = ("oh, hello"+4 == s7); Q = ("oh, hello"+4 == s7);
return cc; return cc;
} }
int main7(int d, int e, int f)
{
char c=-1;
if (d) s5 = s3; else s5 = &c;
*(f ? s5 + 2 : &c) = 'T';
R=c;
*s5=' ';
if (e) s6 = s3+1; else s6 = &c;
*s6=cc;
c=*s4;
return c;
}
int strcmp(const char *s1, const char *s2) int strcmp(const char *s1, const char *s2)
{ {
...@@ -117,14 +111,21 @@ int strcmp(const char *s1, const char *s2) ...@@ -117,14 +111,21 @@ int strcmp(const char *s1, const char *s2)
return (*(unsigned char *)s1 - *(unsigned char *)--s2); return (*(unsigned char *)s1 - *(unsigned char *)--s2);
} }
//@ assigns p[0..s-1]; ensures \initialized(&p[0..s-1]); //@ assigns p[0..s-1]; ensures \initialized(&p[0..s-1]);
void assigns(char *p, unsigned int s); void assigns(char *p, unsigned int s);
int main8() { int long_chain() {
char tc[30]; char tc[30];
char long_chain[] = "really really really long chain"; char long_chain[] = "really really really long chain";
assigns(&tc[0],30); assigns(&tc[0],30);
int x = strcmp(long_chain, tc); int x = strcmp(long_chain, tc);
return x; return x;
} }
void main() {
string_reads ();
string_writes ();
string_comparison ();
long_chain ();
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment