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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/abstract_struct_1.c (with preprocessing)
[kernel] Parsing tests/value/abstract_struct_2.c (with preprocessing)
[value] Analyzing an incomplete application starting at main
[value] Computing initial state
tests/value/abstract_struct_1.c:10:[value] warning: during initialization of variable 'repositories', size of
type 'struct abstracttype' cannot be computed
(abstract type 'struct abstracttype')
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
repositories ∈ {{ NULL ; &S_repositories[0] }}
S_repositories[0].data ∈
{{ NULL ; (struct abstracttype *)&S_data_0_S_repositories }}
[1].data ∈
{{ NULL ; (struct abstracttype *)&S_data_1_S_repositories }}
S_data_0_S_repositories[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
S_data_1_S_repositories[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
[value] computing for function calloc <- main.
Called from tests/value/abstract_struct_1.c:13.
tests/value/abstract_struct_1.c:13:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[value] using specification for function calloc
share/libc/stdlib.h:159:[value] function calloc: precondition got status valid.
[value] Done for function calloc
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
repositories ∈
{{ NULL + [--..--] ;
&alloced_return_calloc + [0..2147483647] }}
[from] Computing for function main
[from] Computing for function calloc <-main
[from] Done for function calloc
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function calloc:
\result FROM nmemb; size
[from] Function main:
repositories FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
repositories
[inout] Inputs for function main:
\nothing
|
