1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/strings.i (no preprocessing)
[value] Analyzing a complete application starting at main1
[value] Computing initial state
[value] Initial state computed
[value: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" }}
[value] computing for function u <- main1.
Called from tests/value/strings.i:39.
tests/value/strings.i:39:[kernel] warning: Neither code nor specification for function u, generating default assigns from the prototype
[value] using specification for function u
[value] Done for function u
tests/value/strings.i:39:[value] warning: out of bounds read. assert \valid_read(p - 4);
[value] computing for function u <- main1.
Called from tests/value/strings.i:42.
[value] Done for function u
tests/value/strings.i:42:[value] warning: out of bounds read. assert \valid_read(p + 12);
[value] computing for function u <- main1.
Called from tests/value/strings.i:44.
[value] Done for function u
[value] computing for function u <- main1.
Called from tests/value/strings.i:48.
[value] Done for function u
tests/value/strings.i:48:[value] warning: out of bounds read. assert \valid_read(p - 4);
[value] Call to builtin bzero(({{ (unsigned char *)&a }},{10}))
[value] computing for function u <- main1.
Called from tests/value/strings.i:53.
[value] Done for function u
[value] computing for function strcpy <- main1.
Called from tests/value/strings.i:53.
tests/value/strings.i:21:[value] warning: out of bounds write.
assert \valid(tmp_unroll_46);
(tmp_unroll_46 from ldst++)
tests/value/strings.i:21:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
[value] Recording results for strcpy
[value] Done for function strcpy
[value] computing for function strlen <- main1.
Called from tests/value/strings.i:58.
[value] Recording results for strlen
[value] Done for function strlen
[value] Recording results for main1
[value] done for function main1
tests/value/strings.i:21:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/strings.i:39:[value] assertion 'Value,mem_access' got final status invalid.
tests/value/strings.i:42:[value] assertion 'Value,mem_access' got final status invalid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function strcpy:
NON TERMINATING FUNCTION
[value:final-states] Values at end of function strlen:
s ∈ {{ &s1[6] }}
l ∈ {5}
[value: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] Computing for function Frama_C_bzero <-main1
[from] Done for function Frama_C_bzero
[from] Done for function main1
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_bzero:
a[0..9] FROM \nothing
[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
|
