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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/narrow_behaviors.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
nondet ∈ [--..--]
[value] computing for function f1 <- main.
Called from tests/value/narrow_behaviors.i:56.
[value] using specification for function f1
[value] Done for function f1
[value] DUMPING STATE of file tests/value/narrow_behaviors.i line 56
nondet ∈ [--..--]
p{.x; .y} ∈ {1; 2}
q ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
=END OF DUMP==
[value] computing for function f2 <- main.
Called from tests/value/narrow_behaviors.i:57.
[value] using specification for function f2
[value] Done for function f2
[value] DUMPING STATE of file tests/value/narrow_behaviors.i line 57
nondet ∈ [--..--]
p{.x; .y} ∈ {1; 2}
q{.x; .y} ∈ {1; 2}
__retres ∈ UNINITIALIZED
=END OF DUMP==
tests/value/narrow_behaviors.i:61:[value] warning: assertion got status unknown.
[value] computing for function f1 <- main.
Called from tests/value/narrow_behaviors.i:62.
tests/value/narrow_behaviors.i:62:[value] function f1, behavior a: assumes got status invalid; behavior not evaluated.
tests/value/narrow_behaviors.i:62:[value] function f1, behavior d: assumes got status invalid; behavior not evaluated.
[value] Done for function f1
[value] computing for function f1 <- main.
Called from tests/value/narrow_behaviors.i:62.
tests/value/narrow_behaviors.i:62:[value] function f1, behavior b: assumes got status invalid; behavior not evaluated.
tests/value/narrow_behaviors.i:62:[value] function f1, behavior c: assumes got status invalid; behavior not evaluated.
[value] Done for function f1
[value] DUMPING STATE of file tests/value/narrow_behaviors.i line 62
nondet ∈ {1}
r{.x; .y} ∈ {2}
s ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
=END OF DUMP==
[value] DUMPING STATE of file tests/value/narrow_behaviors.i line 62
nondet ∈ {0}
r{.x; .y} ∈ {1}
s ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
=END OF DUMP==
[value] computing for function f2 <- main.
Called from tests/value/narrow_behaviors.i:63.
tests/value/narrow_behaviors.i:63:[value] function f2, behavior a: assumes got status invalid; behavior not evaluated.
tests/value/narrow_behaviors.i:63:[value] function f2, behavior d: assumes got status invalid; behavior not evaluated.
tests/value/narrow_behaviors.i:39:[value] warning: function f2, behavior b: this postcondition evaluates to false in this
context. If it is valid, either a precondition was not verified for this
call, or some assigns/from clauses are incomplete (or incorrect).
tests/value/narrow_behaviors.i:40:[value] function f2, behavior b: no state left in which to evaluate postcondition, status not computed.
[value] Done for function f2
[value] computing for function f2 <- main.
Called from tests/value/narrow_behaviors.i:63.
tests/value/narrow_behaviors.i:63:[value] function f2, behavior b: assumes got status invalid; behavior not evaluated.
tests/value/narrow_behaviors.i:63:[value] function f2, behavior c: assumes got status invalid; behavior not evaluated.
[value] Done for function f2
[value] DUMPING STATE of file tests/value/narrow_behaviors.i line 63
nondet ∈ {0}
r{.x; .y} ∈ {1}
s.x ∈ {1; 2}
.y ∈ {1}
__retres ∈ UNINITIALIZED
=END OF DUMP==
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
__retres ∈ {0}
[from] Computing for function main
[from] Computing for function f1 <-main
[from] Done for function f1
[from] Computing for function Frama_C_dump_each <-main
[from] Done for function Frama_C_dump_each
[from] Computing for function f2 <-main
[from] Done for function f2
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f1:
\result FROM nondet
[from] Function f2:
\result FROM nondet
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
p; q; r; s; __retres
[inout] Inputs for function main:
nondet
|
