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
150
151
152
153
154
155
156
157
158
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/undefined_sequence2.i (no preprocessing)
tests/value/undefined_sequence2.i:11:[kernel] warning: Unspecified sequence with side effect:
/* *x <- x */
tmp = 0;
*x = tmp;
/* *x <- x */
tmp_0 = 0;
*x = tmp_0;
tests/value/undefined_sequence2.i:18:[kernel] warning: Unspecified sequence with side effect:
/* i <- */
i ++;
/* i <- */
i ++;
tests/value/undefined_sequence2.i:26:[kernel] warning: Unspecified sequence with side effect:
/* <- */
tmp = i;
/* i <- */
i ++;
/* a[tmp] <- tmp i */
a[tmp] = i;
tests/value/undefined_sequence2.i:34:[kernel] warning: Unspecified sequence with side effect:
/* *x <- x */
tmp = 0;
*x = tmp;
/* *y <- y */
tmp_0 = 0;
*y = tmp_0;
tests/value/undefined_sequence2.i:47:[kernel] warning: Unspecified sequence with side effect:
/* *x <- x */
tmp = 0;
*x = tmp;
/* *y <- y */
tmp_0 = 0;
*y = tmp_0;
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
a[0..1] ∈ {0}
foo ∈ [--..--]
[value] computing for function multiple_update_wrong_1 <- main.
Called from tests/value/undefined_sequence2.i:56.
tests/value/undefined_sequence2.i:11:[value] warning: undefined multiple accesses in expression. assert \separated(x, x);
[value] Recording results for multiple_update_wrong_1
[value] Done for function multiple_update_wrong_1
[value] computing for function multiple_update_wrong_2 <- main.
Called from tests/value/undefined_sequence2.i:58.
tests/value/undefined_sequence2.i:18:[value] warning: undefined multiple accesses in expression. assert \separated(&i, &i);
[value] Recording results for multiple_update_wrong_2
[value] Done for function multiple_update_wrong_2
[value] computing for function multiple_update_wrong_3 <- main.
Called from tests/value/undefined_sequence2.i:60.
tests/value/undefined_sequence2.i:26:[value] warning: undefined multiple accesses in expression. assert \separated(&i, &i);
[value] Recording results for multiple_update_wrong_3
[value] Done for function multiple_update_wrong_3
[value] computing for function multiple_update_unsafe <- main.
Called from tests/value/undefined_sequence2.i:62.
[value] Recording results for multiple_update_unsafe
[value] Done for function multiple_update_unsafe
[value] Called Frama_C_show_each_passed4()
[value] computing for function multiple_update_unsafe <- main.
Called from tests/value/undefined_sequence2.i:64.
tests/value/undefined_sequence2.i:34:[value] warning: undefined multiple accesses in expression. assert \separated(x, y);
[value] Recording results for multiple_update_unsafe
[value] Done for function multiple_update_unsafe
[value] computing for function multiple_update_safe <- main.
Called from tests/value/undefined_sequence2.i:66.
[value] Recording results for multiple_update_safe
[value] Done for function multiple_update_safe
[value] Called Frama_C_show_each_passed6()
[value] computing for function multiple_update_safe <- main.
Called from tests/value/undefined_sequence2.i:68.
[value] Recording results for multiple_update_safe
[value] Done for function multiple_update_safe
[value] Called Frama_C_show_each_passed7()
[value] Recording results for main
[value] done for function main
tests/value/undefined_sequence2.i:11:[value] assertion 'Value,separation' got final status invalid.
tests/value/undefined_sequence2.i:18:[value] assertion 'Value,separation' got final status invalid.
tests/value/undefined_sequence2.i:26:[value] assertion 'Value,separation' got final status invalid.
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function multiple_update_safe:
b ∈ {0}
c ∈ {0}
__retres ∈ {0}
[value:final-states] Values at end of function multiple_update_unsafe:
b ∈ {0}
c ∈ {0}
__retres ∈ {0}
[value:final-states] Values at end of function multiple_update_wrong_1:
NON TERMINATING FUNCTION
[value:final-states] Values at end of function multiple_update_wrong_2:
NON TERMINATING FUNCTION
[value:final-states] Values at end of function multiple_update_wrong_3:
NON TERMINATING FUNCTION
[value:final-states] Values at end of function main:
b ∈ {0}
c ∈ {0}
__retres ∈ {0}
[from] Computing for function multiple_update_safe
[from] Done for function multiple_update_safe
[from] Computing for function multiple_update_unsafe
[from] Done for function multiple_update_unsafe
[from] Computing for function multiple_update_wrong_1
[from] Non-terminating function multiple_update_wrong_1 (no dependencies)
[from] Done for function multiple_update_wrong_1
[from] Computing for function multiple_update_wrong_2
[from] Non-terminating function multiple_update_wrong_2 (no dependencies)
[from] Done for function multiple_update_wrong_2
[from] Computing for function multiple_update_wrong_3
[from] Non-terminating function multiple_update_wrong_3 (no dependencies)
[from] Done for function multiple_update_wrong_3
[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 multiple_update_safe:
b FROM x; y (and SELF)
c FROM x; y (and SELF)
\result FROM x; y
[from] Function multiple_update_unsafe:
b FROM x
c FROM y
\result FROM \nothing
[from] Function multiple_update_wrong_1:
NON TERMINATING - NO EFFECTS
[from] Function multiple_update_wrong_2:
NON TERMINATING - NO EFFECTS
[from] Function multiple_update_wrong_3:
NON TERMINATING - NO EFFECTS
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function multiple_update_safe:
tmp; tmp_0; b; c; __retres
[inout] Inputs for function multiple_update_safe:
\nothing
[inout] Out (internal) for function multiple_update_unsafe:
tmp; tmp_0; b; c; __retres
[inout] Inputs for function multiple_update_unsafe:
\nothing
[inout] Out (internal) for function multiple_update_wrong_1:
\nothing
[inout] Inputs for function multiple_update_wrong_1:
\nothing
[inout] Out (internal) for function multiple_update_wrong_2:
\nothing
[inout] Inputs for function multiple_update_wrong_2:
\nothing
[inout] Out (internal) for function multiple_update_wrong_3:
\nothing
[inout] Inputs for function multiple_update_wrong_3:
\nothing
[inout] Out (internal) for function main:
b; c; __retres
[inout] Inputs for function main:
foo
|
