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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/impact/alias.i (no preprocessing)
[impact] beginning analysis
[value] Analyzing an incomplete application starting at f
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
P ∈ [--..--]
c ∈ [--..--]
tests/impact/alias.i:7:[value] warning: function f: precondition got status unknown.
tests/impact/alias.i:11:[value] warning: out of bounds write. assert \valid(y);
tests/impact/alias.i:12:[value] warning: out of bounds read. assert \valid_read(x + 1);
tests/impact/alias.i:13:[value] warning: out of bounds write. assert \valid(y);
tests/impact/alias.i:15:[value] warning: out of bounds read. assert \valid_read(x + 1);
tests/impact/alias.i:18:[value] warning: out of bounds read. assert \valid_read(y);
[value] Recording results for f
[value] done for function f
tests/impact/alias.i:18:[value] assertion 'Value,mem_access' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[pdg] computing for function f
[pdg] done for function f
[impact] impacted statements of stmt(s) 2 are:
tests/impact/alias.i:10 (sid 4): y = x + 1;
tests/impact/alias.i:11 (sid 5): *y = 4;
tests/impact/alias.i:12 (sid 7): a = *(x + 1) + 2;
tests/impact/alias.i:13 (sid 8): *y = 2;
tests/impact/alias.i:15 (sid 12): __retres = *(x + 1);
tests/impact/alias.i:14 (sid 19): return_label: return __retres;
[impact] analysis done
|
