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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/bitwise_or.c (with 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
Frama_C_entropy_source ∈ [--..--]
or1 ∈ {0}
or2 ∈ {0}
or3 ∈ {0}
or4 ∈ {0}
or5 ∈ {0}
and1 ∈ {0}
and2 ∈ {0}
and3 ∈ {0}
and4 ∈ {0}
xor1 ∈ {0}
xor2 ∈ {0}
uand1 ∈ {0}
uand2 ∈ {0}
uand3 ∈ {0}
uand4 ∈ {0}
uand5 ∈ {0}
a ∈ {0}
b ∈ {0}
c ∈ {0}
d ∈ {0}
e ∈ {0}
s ∈ [--..--]
[value] computing for function Frama_C_interval <- main.
Called from tests/value/bitwise_or.c:13.
[value] using specification for function Frama_C_interval
share/libc/__fc_builtin.h:50:[value] function Frama_C_interval: precondition got status valid.
[value] Done for function Frama_C_interval
[value] computing for function Frama_C_interval <- main.
Called from tests/value/bitwise_or.c:14.
[value] Done for function Frama_C_interval
[value] computing for function Frama_C_interval <- main.
Called from tests/value/bitwise_or.c:15.
[value] Done for function Frama_C_interval
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
or1 ∈ [--..--]
or2 ∈ [13..31]
or3 ∈ [--..--]
and1 ∈ [0..17]
and2 ∈ [0..17]
and3 ∈ [0..27]
xor1 ∈ [0..31]
xor2 ∈ [--..--]
uand4 ∈ [8..24]
a ∈ [3..17]
b ∈ [-3..17]
c ∈ [13..27]
i1 ∈ [0..0x1FFFE],0%2
i2 ∈ [0..0x3FFFC],0%4
v1 ∈ [0..0x1FFFE],0%2
v2 ∈ [0..0x3FFFF]
mask07 ∈ {5}
mask0f ∈ {13}
mask1f ∈ {13; 29}
__retres ∈ {0}
|
