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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/recol.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
s[0..99] ∈ {0}
c ∈ {0}
s_int ∈ {0}
p_int ∈ {0}
ones[0..7] ∈ {49}
[8] ∈ {0}
one23[0] ∈ {49}
[1..2] ∈ {50}
[3] ∈ {51}
[4] ∈ {0}
col_ones ∈ {0}
col_123 ∈ {0}
tests/value/recol.c:30:[value] warning: 2's complement assumed for overflow
tests/value/recol.c:47:[value] warning: 2's complement assumed for overflow
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
s[bits 0 to 15] ∈ {97}
[bits 16 to 47] ∈ {776}
[6] ∈ {-103}
[bits 56 to 71] ∈ {-26736}
[bits 72 to 103] ∈ {271697}
[13] ∈ {-104}
[bits 112 to 127] ∈ {10121}
[bits 128 to 159] ∈ {93197600}
[20] ∈ {65}
[21] ∈ {40}
[bits 176 to 191] ∈ {25465}
[bits 192 to 223] ∈ {429177008}
[bits 224 to 255] ∈ {-1290728143}
[bits 256 to 287] ∈ {-445162312}
[bits 288 to 303] ∈ {-30359}
[38] ∈ {64}
[bits 312 to 343] ∈ {1928155169}
[43] ∈ {72}
[44] ∈ {89}
[bits 360 to 391] ∈ {-67735088}
[bits 392 to 423] ∈ {-474145519}
[bits 424 to 439] ∈ {-13352}
[55] ∈ {73}
[bits 448 to 463] ∈ {1888}
[bits 464 to 495] ∈ {-257018879}
[bits 496 to 527] ∈ {-1799132056}
[66] ∈ {57}
[bits 536 to 551] ∈ {-15632}
[bits 552 to 583] ∈ {1373000945}
[bits 584 to 599] ∈ {21240}
[75] ∈ {41}
[76] ∈ {-128}
[77] ∈ {-31}
[bits 624 to 655] ∈ {-832127096}
[82] ∈ {25}
[83] ∈ {16}
[bits 672 to 703] ∈ {-1951746863}
[bits 704 to 735] ∈ {-777326056}
[bits 736 to 767] ∈ {-1146314999}
[bits 768 to 783] ∈ {22944}
[98..99] ∈ {0}
c ∈ {565729696}
s_int ∈ {-833811464}
p_int ∈ {{ (int *)&s[100] }}
col_ones ∈ {825307442}
col_123 ∈ {858927666}
p ∈ {{ &s[98] }}
__retres ∈ {0}
|
