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
|
[kernel] Parsing extern_init.i (no preprocessing)
[kernel] Parsing extern_init_1.i (no preprocessing)
[kernel] Parsing extern_init_2.i (no preprocessing)
[kernel:typing:no-proto] extern_init_2.i:10: Warning:
Calling function f that is declared without prototype.
Its formals will be inferred from actual arguments
[kernel:typing:no-proto] extern_init_2.i:11: Warning:
Calling function g that is declared without prototype.
Its formals will be inferred from actual arguments
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
[3] ∈ {4}
[4] ∈ {5}
[eva] computing for function f <- main.
Called from extern_init_2.i:10.
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
Called from extern_init_2.i:11.
[eva] using specification for function g
[eva] Done for function g
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
a[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {12}
[3] ∈ {4}
[4] ∈ {5}
[eva:final-states] Values at end of function main:
a[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {12}
[3] ∈ [--..--]
[4] ∈ {5}
__retres ∈ {2}
|
