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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/dead_statuses.i (no preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
[value] computing for function f <- main.
Called from tests/value/dead_statuses.i:9.
[value] using specification for function f
tests/value/dead_statuses.i:5:[value] function f: precondition got status valid.
[value] Done for function f
[value] computing for function f <- main.
Called from tests/value/dead_statuses.i:11.
[value] Done for function f
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
NO EFFECTS
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
\nothing
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'Frama_C_bzero'
--------------------------------------------------------------------------------
[ Extern ] Post-condition (file share/libc/__fc_builtin_for_normalization.i, line 32)
Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/__fc_builtin_for_normalization.i, line 31)
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/__fc_builtin_for_normalization.i, line 31)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'f'
--------------------------------------------------------------------------------
[ Valid ] Pre-condition (file tests/value/dead_statuses.i, line 5)
by Call Preconditions.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------
[ Dead ] Post-condition for 'Frama_C_implicit_init' (file tests/value/dead_statuses.i, line 14) at block
Locally valid, but unreachable.
By Frama-C kernel because:
- Unreachable block (after it)
By Value because:
- Unreachable block (after it)
[ Dead ] Post-condition for 'Frama_C_implicit_init' (file tests/value/dead_statuses.i, line 14) at block
Locally valid, but unreachable.
By Frama-C kernel because:
- Unreachable block (after it)
By Value because:
- Unreachable block (after it)
[ Dead ] Pre-condition (file tests/value/dead_statuses.i, line 18) at instruction (file tests/value/dead_statuses.i, line 19)
Locally valid, but unreachable.
By Value because:
- Unreachable instruction (file tests/value/dead_statuses.i, line 19)
[ Dead ] Assigns for 'Frama_C_implicit_init' (file tests/value/dead_statuses.i, line 14) at block
Locally valid, but unreachable.
By Frama-C kernel because:
- Unreachable block (after it)
By Value because:
- Unreachable block (after it)
[ Dead ] Assertion (file tests/value/dead_statuses.i, line 15)
Locally valid, but unreachable.
By Value because:
- Unreachable program point (file tests/value/dead_statuses.i, line 15)
[ Dead ] Invariant (file tests/value/dead_statuses.i, line 16)
Locally valid, but unreachable.
By Value because:
- Unreachable loop (file tests/value/dead_statuses.i, line 17)
[ Dead ] Behavior 'Frama_C_implicit_init' at block
Locally valid, but unreachable.
By Frama-C kernel because:
- Unreachable block (after it)
[ Valid ] Default behavior at instruction (file tests/value/dead_statuses.i, line 19)
by Frama-C kernel.
[Unreachable] Unreachable call 'f' (file tests/value/dead_statuses.i, line 13)
by Value.
[Unreachable] Unreachable block (after it)
by Value.
[Unreachable] Unreachable program point (file tests/value/dead_statuses.i, line 15)
by Value.
[Unreachable] Unreachable loop (file tests/value/dead_statuses.i, line 17)
by Value.
[Unreachable] Unreachable instruction (file tests/value/dead_statuses.i, line 19)
by Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/dead_statuses.i, line 5)' at call 'f' (file tests/value/dead_statuses.i, line 9)
by Value.
[ Valid ] Instance of 'Pre-condition (file tests/value/dead_statuses.i, line 5)' at call 'f' (file tests/value/dead_statuses.i, line 11)
by Value.
[ Dead ] Instance of 'Pre-condition (file tests/value/dead_statuses.i, line 5)' at call 'f' (file tests/value/dead_statuses.i, line 13)
Locally valid, but unreachable.
By Value because:
- Unreachable call 'f' (file tests/value/dead_statuses.i, line 13)
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
6 Completely validated
4 Considered valid
8 Dead properties
5 Unreachable
23 Total
--------------------------------------------------------------------------------
|
