Skip to content
Snippets Groups Projects
Commit 267a2df5 authored by Bouillaguet Quentin's avatar Bouillaguet Quentin Committed by David Bühler
Browse files

[Eva] Check and update oracles 

Verified by comparing pre and post rebase generated dots.
Inversion of generated nodes seems to be the result of now different
order of calling assume (with true or false).
parent 4296e658
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
tests/value/traces/oracle/test1.res.oracle
+ 58
− 56
View file @ 267a2df5
[kernel] Parsing tests/value/traces/test1.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
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
entropy_source ∈ [--..--]
g ∈ {42}
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
g ∈ {5; 45}
tmp ∈ {5; 45}
[value:d-traces] Trace domains:
[eva:d-traces] Trace domains:
start: 0; globals = g, entropy_source; main_formals = c;
{[ 0 -> initialize variable: entropy_source -> 1
1 -> initialize variable using type Library_Global
......@@ -22,64 +22,66 @@ entropy_source -> 2
c -> 5
5 -> EnterScope: tmp -> 6
6 -> Assign: tmp = 0 -> 7
7 -> Assume: c false -> 8; Assume: c true -> 9
8 -> Assign: tmp = 2 -> 12
9 -> Assign: tmp = g -> 11
11 -> EnterScope: i -> 17
12 -> EnterScope: i -> 14
14 -> initialize variable: i -> 15
15 -> Assign: i = 0 -> 16
16 -> enter_loop -> 22
17 -> initialize variable: i -> 18
18 -> Assign: i = 0 -> 19
19 -> enter_loop -> 21
21 -> Assume: i < 3 true -> 24
22 -> Assume: i < 3 true -> 25
24 -> Assign: tmp = tmp + 1 -> 27
25 -> Assign: tmp = tmp + 1 -> 26
26 -> Assign: i = i + 1 -> 28
27 -> Assign: i = i + 1 -> 29
28 -> Assume: i < 3 true -> 34
29 -> Assume: i < 3 true -> 33
33 -> Assign: tmp = tmp + 1 -> 36
34 -> Assign: tmp = tmp + 1 -> 35
35 -> Assign: i = i + 1 -> 38
36 -> Assign: i = i + 1 -> 37
37 -> Assume: i < 3 true -> 44
38 -> Assume: i < 3 true -> 43
43 -> Assign: tmp = tmp + 1 -> 46
44 -> Assign: tmp = tmp + 1 -> 45
45 -> Assign: i = i + 1 -> 48
46 -> Assign: i = i + 1 -> 47
47 -> Assume: i < 3 false -> 54
48 -> Assume: i < 3 false -> 53
53 -> LeaveScope: i -> 55
54 -> LeaveScope: i -> 56
55 -> Assign: g = tmp -> 58
56 -> Assign: g = tmp -> 57
57 -> join -> 59
58 -> join -> 59 ]} at 59
7 -> Assume: c true -> 8; Assume: c false -> 10
8 -> Assign: tmp = g -> 9
9 -> EnterScope: i -> 15
10 -> Assign: tmp = 2 -> 11
11 -> EnterScope: i -> 12
12 -> initialize variable: i -> 13
13 -> Assign: i = 0 -> 14
14 -> enter_loop -> 19
15 -> initialize variable: i -> 16
16 -> Assign: i = 0 -> 17
17 -> enter_loop -> 18
18 -> Assume: i < 3 true -> 20
19 -> Assume: i < 3 true -> 21
20 -> Assign: tmp = tmp + 1 -> 23
21 -> Assign: tmp = tmp + 1 -> 22
22 -> Assign: i = i + 1 -> 24
23 -> Assign: i = i + 1 -> 25
24 -> Assume: i < 3 true -> 27
25 -> Assume: i < 3 true -> 26
26 -> Assign: tmp = tmp + 1 -> 29
27 -> Assign: tmp = tmp + 1 -> 28
28 -> Assign: i = i + 1 -> 30
29 -> Assign: i = i + 1 -> 31
30 -> Assume: i < 3 true -> 33
31 -> Assume: i < 3 true -> 32
32 -> Assign: tmp = tmp + 1 -> 35
33 -> Assign: tmp = tmp + 1 -> 34
34 -> Assign: i = i + 1 -> 36
35 -> Assign: i = i + 1 -> 37
36 -> Assume: i < 3 false -> 39
37 -> Assume: i < 3 false -> 38
38 -> LeaveScope: i -> 40
39 -> LeaveScope: i -> 41
40 -> LeaveScope: i -> 42
41 -> LeaveScope: i -> 43
42 -> Assign: g = tmp -> 45
43 -> Assign: g = tmp -> 44
44 -> join -> 46
45 -> join -> 46 ]} at 46
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
These dependencies hold at termination for the executions that terminate:
[from] Function main:
g FROM g; c
\result FROM g; c
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
g; tmp; i
g; tmp; i
[inout] Inputs for function main:
g
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
g
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
entropy_source ∈ [--..--]
g ∈ {42}
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
g ∈ {5; 45}
__traces_domain_return ∈ {5; 45}
/* Generated by Frama-C */
......
tests/value/traces/oracle/test2.res.oracle
+ 85
− 83
View file @ 267a2df5
[kernel] Parsing tests/value/traces/test2.i (no 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
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[value] computing for function loop <- main.
Called from tests/value/traces/test2.i:18.
[value] Recording results for loop
[value] Done for function loop
[value] computing for function loop <- main.
Called from tests/value/traces/test2.i:18.
[value] Recording results for loop
[value] Done for function loop
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function loop:
[eva] computing for function loop <- main.
Called from tests/value/traces/test2.i:18.
[eva] Recording results for loop
[eva] Done for function loop
[eva] computing for function loop <- main.
Called from tests/value/traces/test2.i:18.
[eva] Recording results for loop
[eva] Done for function loop
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function loop:
j ∈ {4; 5}
[value:final-states] Values at end of function main:
[eva:final-states] Values at end of function main:
tmp ∈ {4; 5}
[value:d-traces] Trace domains:
[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
{[ 0 -> initialize variable using type Main_Formal
c -> 1
1 -> EnterScope: tmp -> 2
2 -> Assign: tmp = 0 -> 3
3 -> Assume: c false -> 4; Assume: c true -> 5
4 -> Assign: tmp = 2 -> 8
5 -> Assign: tmp = 1 -> 7
7 -> start_call: loop (true) -> 9
8 -> start_call: loop (true) -> 45
9 -> EnterScope: j -> 10
10 -> Assign: j = tmp -> 11
11 -> EnterScope: i -> 12
12 -> initialize variable: i -> 13
13 -> Assign: i = 0 -> 14
14 -> enter_loop -> 15
15 -> Assume: i < 3 true -> 16
16 -> Assign: j = j + 1 -> 17
17 -> Assign: i = i + 1 -> 18
18 -> Assume: i < 3 true -> 20
20 -> Assign: j = j + 1 -> 21
21 -> Assign: i = i + 1 -> 22
22 -> Assume: i < 3 true -> 25
25 -> Assign: j = j + 1 -> 26
26 -> Assign: i = i + 1 -> 27
27 -> Assume: i < 3 false -> 30
30 -> LeaveScope: i -> 31
31 -> EnterScope: \result<loop> -> 32
32 -> Assign: \result<loop> = j -> 33
33 -> LeaveScope: j -> 41
41 -> finalize_call: loop -> 42
42 -> Assign: tmp = \result<loop> -> 43
43 -> LeaveScope: \result<loop> -> 44
44 -> join -> 90
45 -> EnterScope: j -> 46
46 -> Assign: j = tmp -> 47
47 -> EnterScope: i -> 49
49 -> initialize variable: i -> 50
50 -> Assign: i = 0 -> 51
51 -> enter_loop -> 52
52 -> Assume: i < 3 true -> 53
53 -> Assign: j = j + 1 -> 54
54 -> Assign: i = i + 1 -> 55
55 -> Assume: i < 3 true -> 57
57 -> Assign: j = j + 1 -> 58
58 -> Assign: i = i + 1 -> 59
59 -> Assume: i < 3 true -> 62
62 -> Assign: j = j + 1 -> 63
63 -> Assign: i = i + 1 -> 64
64 -> Assume: i < 3 false -> 67
67 -> LeaveScope: i -> 68
68 -> EnterScope: \result<loop> -> 69
69 -> Assign: \result<loop> = j -> 70
70 -> LeaveScope: j -> 86
86 -> finalize_call: loop -> 87
87 -> Assign: tmp = \result<loop> -> 88
88 -> LeaveScope: \result<loop> -> 89
89 -> join -> 90 ]} at 90
3 -> Assume: c true -> 4; Assume: c false -> 6
4 -> Assign: tmp = 1 -> 5
5 -> start_call: loop (true) -> 8
6 -> Assign: tmp = 2 -> 7
7 -> start_call: loop (true) -> 40
8 -> EnterScope: j -> 9
9 -> Assign: j = tmp -> 10
10 -> EnterScope: i -> 11
11 -> initialize variable: i -> 12
12 -> Assign: i = 0 -> 13
13 -> enter_loop -> 14
14 -> Assume: i < 3 true -> 15
15 -> Assign: j = j + 1 -> 16
16 -> Assign: i = i + 1 -> 17
17 -> Assume: i < 3 true -> 18
18 -> Assign: j = j + 1 -> 19
19 -> Assign: i = i + 1 -> 20
20 -> Assume: i < 3 true -> 21
21 -> Assign: j = j + 1 -> 22
22 -> Assign: i = i + 1 -> 23
23 -> Assume: i < 3 false -> 24
24 -> LeaveScope: i -> 25
25 -> LeaveScope: i -> 26
26 -> EnterScope: \result<loop> -> 27
27 -> Assign: \result<loop> = j -> 28
28 -> LeaveScope: j -> 36
36 -> finalize_call: loop -> 37
37 -> Assign: tmp = \result<loop> -> 38
38 -> LeaveScope: \result<loop> -> 39
39 -> join -> 79
40 -> EnterScope: j -> 41
41 -> Assign: j = tmp -> 42
42 -> EnterScope: i -> 44
44 -> initialize variable: i -> 45
45 -> Assign: i = 0 -> 46
46 -> enter_loop -> 47
47 -> Assume: i < 3 true -> 48
48 -> Assign: j = j + 1 -> 49
49 -> Assign: i = i + 1 -> 50
50 -> Assume: i < 3 true -> 51
51 -> Assign: j = j + 1 -> 52
52 -> Assign: i = i + 1 -> 53
53 -> Assume: i < 3 true -> 54
54 -> Assign: j = j + 1 -> 55
55 -> Assign: i = i + 1 -> 56
56 -> Assume: i < 3 false -> 57
57 -> LeaveScope: i -> 58
58 -> LeaveScope: i -> 59
59 -> EnterScope: \result<loop> -> 60
60 -> Assign: \result<loop> = j -> 61
61 -> LeaveScope: j -> 75
75 -> finalize_call: loop -> 76
76 -> Assign: tmp = \result<loop> -> 77
77 -> LeaveScope: \result<loop> -> 78
78 -> join -> 79 ]} at 79
[from] Computing for function loop
[from] Done for function loop
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
These dependencies hold at termination for the executions that terminate:
[from] Function loop:
\result FROM j
[from] Function main:
\result FROM c
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function loop:
j; i
j; i
[inout] Inputs for function loop:
\nothing
\nothing
[inout] Out (internal) for function main:
tmp
tmp
[inout] Inputs for function main:
\nothing
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
\nothing
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__traces_domain_return ∈ {4; 5}
/* Generated by Frama-C */
int main(int c)
......
tests/value/traces/oracle/test3.res.oracle
+ 19
− 19
View file @ 267a2df5
[kernel] Parsing tests/value/traces/test3.i (no 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
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
g ∈ {0}
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
g ∈ {4}
tmp ∈ {4}
__retres ∈ {5}
[value:d-traces] Trace domains:
[eva:d-traces] Trace domains:
start: 0; globals = g; main_formals = c;
{[ 0 -> initialize variable: g -> 1
1 -> initialize variable using type Main_Formal
......@@ -26,23 +26,23 @@ c -> 2
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
These dependencies hold at termination for the executions that terminate:
[from] Function main:
g FROM \nothing
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
g; tmp; __retres
g; tmp; __retres
[inout] Inputs for function main:
g
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
g
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
g ∈ {0}
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
g ∈ {4}
__traces_domain_return ∈ {5}
/* Generated by Frama-C */
......
tests/value/traces/oracle/test4.res.oracle
+ 232
− 225
View file @ 267a2df5
[kernel] Parsing tests/value/traces/test4.i (no 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
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
tests/value/traces/test4.i:9:[value] entering loop for the first time
tests/value/traces/test4.i:11:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
tests/value/traces/test4.i:14:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
tests/value/traces/test4.i:17:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
tests/value/traces/test4.i:20:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
tests/value/traces/test4.i:23:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
tests/value/traces/test4.i:25:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
[eva] tests/value/traces/test4.i:9: starting to merge loop iterations
[eva:alarm] tests/value/traces/test4.i:11: Warning:
signed overflow. assert tmp + 1 ≤ 2147483647;
[eva:alarm] tests/value/traces/test4.i:14: Warning:
signed overflow. assert tmp + 1 ≤ 2147483647;
[eva:alarm] tests/value/traces/test4.i:17: Warning:
signed overflow. assert tmp + 1 ≤ 2147483647;
[eva:alarm] tests/value/traces/test4.i:20: Warning:
signed overflow. assert tmp + 1 ≤ 2147483647;
[eva:alarm] tests/value/traces/test4.i:23: Warning:
signed overflow. assert tmp + 1 ≤ 2147483647;
[eva:alarm] tests/value/traces/test4.i:25: Warning:
signed overflow. assert tmp + 1 ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
tmp ∈ [46..2147483647]
[value:d-traces] Trace domains:
[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
{[ 0 -> initialize variable using type Main_Formal
c -> 1
......@@ -35,233 +41,234 @@ c -> 1
13 -> Assume: i % 11 false -> 14
14 -> Assign: tmp = tmp + 1 -> 15
15 -> Assign: i = i + 1 -> 16
16 -> Assume: i < 100 true -> 18
18 -> Assume: i % 2 true -> 19
19 -> Assign: tmp = tmp + 1 -> 20
20 -> Assume: i % 3 true -> 21
21 -> Assign: tmp = tmp + 1 -> 22
22 -> Assume: i % 5 true -> 23
23 -> Assign: tmp = tmp + 1 -> 24
24 -> Assume: i % 7 true -> 25
25 -> Assign: tmp = tmp + 1 -> 26
26 -> Assume: i % 11 true -> 27
16 -> Assume: i < 100 true -> 17
17 -> Assume: i % 2 true -> 18
18 -> Assign: tmp = tmp + 1 -> 19
19 -> Assume: i % 3 true -> 20
20 -> Assign: tmp = tmp + 1 -> 21
21 -> Assume: i % 5 true -> 22
22 -> Assign: tmp = tmp + 1 -> 23
23 -> Assume: i % 7 true -> 24
24 -> Assign: tmp = tmp + 1 -> 25
25 -> Assume: i % 11 true -> 26
26 -> Assign: tmp = tmp + 1 -> 27
27 -> Assign: tmp = tmp + 1 -> 28
28 -> Assign: tmp = tmp + 1 -> 29
29 -> Assign: i = i + 1 -> 30
30 -> Assume: i < 100 true -> 33
33 -> Assume: i % 2 false -> 34
34 -> Assume: i % 3 true -> 35
35 -> Assign: tmp = tmp + 1 -> 36
36 -> Assume: i % 5 true -> 38
28 -> Assign: i = i + 1 -> 29
29 -> Assume: i < 100 true -> 30
30 -> Assume: i % 2 false -> 31
31 -> Assume: i % 3 true -> 32
32 -> Assign: tmp = tmp + 1 -> 33
33 -> Assume: i % 5 true -> 34
34 -> Assign: tmp = tmp + 1 -> 35
35 -> Assume: i % 7 true -> 36
36 -> Assign: tmp = tmp + 1 -> 37
37 -> Assume: i % 11 true -> 38
38 -> Assign: tmp = tmp + 1 -> 39
39 -> Assume: i % 7 true -> 41
41 -> Assign: tmp = tmp + 1 -> 42
42 -> Assume: i % 11 true -> 44
44 -> Assign: tmp = tmp + 1 -> 45
45 -> Assign: tmp = tmp + 1 -> 47
47 -> Assign: i = i + 1 -> 48
48 -> Assume: i < 100 true -> 51
51 -> Assume: i % 2 true -> 52
52 -> Assign: tmp = tmp + 1 -> 53
53 -> Assume: i % 3 false -> 55
55 -> Assume: i % 5 true -> 56
39 -> Assign: tmp = tmp + 1 -> 40
40 -> Assign: i = i + 1 -> 41
41 -> Assume: i < 100 true -> 42
42 -> Assume: i % 2 true -> 43
43 -> Assign: tmp = tmp + 1 -> 44
44 -> Assume: i % 3 false -> 45
45 -> Assume: i % 5 true -> 46
46 -> Assign: tmp = tmp + 1 -> 47
47 -> Assume: i % 7 true -> 48
48 -> Assign: tmp = tmp + 1 -> 49
49 -> Assume: i % 11 true -> 50
50 -> Assign: tmp = tmp + 1 -> 51
51 -> Assign: tmp = tmp + 1 -> 52
52 -> Assign: i = i + 1 -> 53
53 -> Assume: i < 100 true -> 54
54 -> Assume: i % 2 false -> 55
55 -> Assume: i % 3 true -> 56
56 -> Assign: tmp = tmp + 1 -> 57
57 -> Assume: i % 7 true -> 59
59 -> Assign: tmp = tmp + 1 -> 60
60 -> Assume: i % 11 true -> 62
57 -> Assume: i % 5 true -> 58
58 -> Assign: tmp = tmp + 1 -> 59
59 -> Assume: i % 7 true -> 60
60 -> Assign: tmp = tmp + 1 -> 61
61 -> Assume: i % 11 true -> 62
62 -> Assign: tmp = tmp + 1 -> 63
63 -> Assign: tmp = tmp + 1 -> 65
65 -> Assign: i = i + 1 -> 66
66 -> Assume: i < 100 true -> 69
69 -> Assume: i % 2 false -> 70
70 -> Assume: i % 3 true -> 71
71 -> Assign: tmp = tmp + 1 -> 72
72 -> Assume: i % 5 true -> 74
63 -> Assign: tmp = tmp + 1 -> 64
64 -> Assign: i = i + 1 -> 65
65 -> Assume: i < 100 true -> 66
66 -> Assume: i % 2 true -> 67
67 -> Assign: tmp = tmp + 1 -> 68
68 -> Assume: i % 3 true -> 69
69 -> Assign: tmp = tmp + 1 -> 70
70 -> Assume: i % 5 false -> 71
71 -> Assume: i % 7 true -> 72
72 -> Assign: tmp = tmp + 1 -> 73
73 -> Assume: i % 11 true -> 74
74 -> Assign: tmp = tmp + 1 -> 75
75 -> Assume: i % 7 true -> 77
77 -> Assign: tmp = tmp + 1 -> 78
78 -> Assume: i % 11 true -> 80
80 -> Assign: tmp = tmp + 1 -> 81
81 -> Assign: tmp = tmp + 1 -> 83
83 -> Assign: i = i + 1 -> 84
84 -> Assume: i < 100 true -> 87
87 -> Assume: i % 2 true -> 88
88 -> Assign: tmp = tmp + 1 -> 89
89 -> Assume: i % 3 true -> 91
91 -> Assign: tmp = tmp + 1 -> 92
92 -> Assume: i % 5 false -> 94
94 -> Assume: i % 7 true -> 95
95 -> Assign: tmp = tmp + 1 -> 96
96 -> Assume: i % 11 true -> 98
75 -> Assign: tmp = tmp + 1 -> 76
76 -> Assign: i = i + 1 -> 77
77 -> Assume: i < 100 true -> 78
78 -> Assume: i % 2 false -> 79
79 -> Assume: i % 3 false -> 80
80 -> Assume: i % 5 true -> 81
81 -> Assign: tmp = tmp + 1 -> 82
82 -> Assume: i % 7 true -> 83
83 -> Assign: tmp = tmp + 1 -> 84
84 -> Assume: i % 11 true -> 85
85 -> Assign: tmp = tmp + 1 -> 86
86 -> Assign: tmp = tmp + 1 -> 87
87 -> Assign: i = i + 1 -> 88
88 -> Assume: i < 100 true -> 89
89 -> Assume: i % 2 true -> 90
90 -> Assign: tmp = tmp + 1 -> 91
91 -> Assume: i % 3 true -> 92
92 -> Assign: tmp = tmp + 1 -> 93
93 -> Assume: i % 5 true -> 94
94 -> Assign: tmp = tmp + 1 -> 95
95 -> Assume: i % 7 false -> 96
96 -> Assume: i % 11 true -> 97
97 -> Assign: tmp = tmp + 1 -> 98
98 -> Assign: tmp = tmp + 1 -> 99
99 -> Assign: tmp = tmp + 1 -> 101
101 -> Assign: i = i + 1 -> 102
102 -> Assume: i < 100 true -> 105
105 -> Assume: i % 2 false -> 106
106 -> Assume: i % 3 false -> 107
107 -> Assume: i % 5 true -> 108
108 -> Assign: tmp = tmp + 1 -> 109
109 -> Assume: i % 7 true -> 111
111 -> Assign: tmp = tmp + 1 -> 112
112 -> Assume: i % 11 true -> 114
99 -> Assign: i = i + 1 -> 100
100 -> Assume: i < 100 true -> 101
101 -> Assume: i % 2 false -> 102
102 -> Assume: i % 3 true -> 103
103 -> Assign: tmp = tmp + 1 -> 104
104 -> Assume: i % 5 true -> 105
105 -> Assign: tmp = tmp + 1 -> 106
106 -> Assume: i % 7 true -> 107
107 -> Assign: tmp = tmp + 1 -> 108
108 -> Assume: i % 11 true -> 109
109 -> Assign: tmp = tmp + 1 -> 110
110 -> Assign: tmp = tmp + 1 -> 111
111 -> Assign: i = i + 1 -> 112
112 -> Assume: i < 100 true -> 113
113 -> Assume: i % 2 true -> 114
114 -> Assign: tmp = tmp + 1 -> 115
115 -> Assign: tmp = tmp + 1 -> 117
117 -> Assign: i = i + 1 -> 118
118 -> Assume: i < 100 true -> 121
121 -> Assume: i % 2 true -> 122
115 -> Assume: i % 3 false -> 116
116 -> Assume: i % 5 true -> 117
117 -> Assign: tmp = tmp + 1 -> 118
118 -> Assume: i % 7 true -> 119
119 -> Assign: tmp = tmp + 1 -> 120
120 -> Assume: i % 11 true -> 121
121 -> Assign: tmp = tmp + 1 -> 122
122 -> Assign: tmp = tmp + 1 -> 123
123 -> Assume: i % 3 true -> 125
125 -> Assign: tmp = tmp + 1 -> 126
126 -> Assume: i % 5 true -> 128
128 -> Assign: tmp = tmp + 1 -> 129
129 -> Assume: i % 7 false -> 131
131 -> Assume: i % 11 true -> 132
123 -> Assign: i = i + 1 -> 124
124 -> Assume: i < 100 true -> 125; join -> 136
125 -> Assume: i % 2 false -> 126; join -> 138
126 -> Assume: i % 3 true -> 127; join -> 143
127 -> Assign: tmp = tmp + 1 -> 128
128 -> Assume: i % 5 false -> 129; join -> 146
129 -> Assume: i % 7 true -> 130; join -> 151
130 -> Assign: tmp = tmp + 1 -> 131
131 -> Assume: i % 11 true -> 132; join -> 154
132 -> Assign: tmp = tmp + 1 -> 133
133 -> Assign: tmp = tmp + 1 -> 135
135 -> Assign: i = i + 1 -> 136
136 -> Assume: i < 100 true -> 139
139 -> Assume: i % 2 false -> 140
140 -> Assume: i % 3 true -> 141
141 -> Assign: tmp = tmp + 1 -> 142
142 -> Assume: i % 5 true -> 144
133 -> Assign: tmp = tmp + 1 -> 134; join -> 159
134 -> Assign: i = i + 1 -> 135; join -> 161
135 -> join -> 136
136 -> Assume: i < 100 true -> 137; join -> 163
137 -> join -> 138
138 -> Assume: i % 2 true -> 139; Assume: i % 2 false -> 141; join -> 165
139 -> Assign: tmp = tmp + 1 -> 140
140 -> join -> 142
141 -> join -> 142
142 -> join -> 143
143 -> Assume: i % 3 true -> 144; join -> 170
144 -> Assign: tmp = tmp + 1 -> 145
145 -> Assume: i % 7 true -> 147
145 -> join -> 146
146 -> Assume: i % 5 true -> 147; Assume: i % 5 false -> 149; join -> 175
147 -> Assign: tmp = tmp + 1 -> 148
148 -> Assume: i % 11 true -> 150
150 -> Assign: tmp = tmp + 1 -> 151
151 -> Assign: tmp = tmp + 1 -> 153
153 -> Assign: i = i + 1 -> 154
154 -> Assume: i < 100 true -> 157
157 -> Assume: i % 2 true -> 158
158 -> Assign: tmp = tmp + 1 -> 159
159 -> Assume: i % 3 false -> 161
161 -> Assume: i % 5 true -> 162
162 -> Assign: tmp = tmp + 1 -> 163
163 -> Assume: i % 7 true -> 165
165 -> Assign: tmp = tmp + 1 -> 166
166 -> Assume: i % 11 true -> 168
168 -> Assign: tmp = tmp + 1 -> 169
169 -> Assign: tmp = tmp + 1 -> 171
171 -> Assign: i = i + 1 -> 172
172 -> Assume: i < 100 true -> 175; join -> 190
175 -> Assume: i % 2 false -> 176; join -> 193
176 -> Assume: i % 3 true -> 177; join -> 199
177 -> Assign: tmp = tmp + 1 -> 178
178 -> Assume: i % 5 false -> 180; join -> 203
180 -> Assume: i % 7 true -> 181; join -> 209
181 -> Assign: tmp = tmp + 1 -> 182
182 -> Assume: i % 11 true -> 184; join -> 213
184 -> Assign: tmp = tmp + 1 -> 185
185 -> Assign: tmp = tmp + 1 -> 187; join -> 219
187 -> Assign: i = i + 1 -> 188; join -> 221
188 -> join -> 190
190 -> Assume: i < 100 true -> 192; join -> 224
148 -> join -> 150
149 -> join -> 150
150 -> join -> 151
151 -> Assume: i % 7 true -> 152; join -> 180
152 -> Assign: tmp = tmp + 1 -> 153
153 -> join -> 154
154 -> Assume: i % 11 true -> 155; Assume: i % 11 false -> 157;
join -> 183
155 -> Assign: tmp = tmp + 1 -> 156; join -> 185
156 -> join -> 158
157 -> join -> 158
158 -> join -> 159
159 -> Assign: tmp = tmp + 1 -> 160; join -> 189
160 -> join -> 161
161 -> Assign: i = i + 1 -> 162; join -> 191
162 -> join -> 163
163 -> Assume: i < 100 true -> 164; join -> 193
164 -> join -> 165
165 -> Assume: i % 2 true -> 166; Assume: i % 2 false -> 168; join -> 196
166 -> Assign: tmp = tmp + 1 -> 167
167 -> join -> 169
168 -> join -> 169
169 -> join -> 170
170 -> Assume: i % 3 true -> 171; Assume: i % 3 false -> 173; join -> 201
171 -> Assign: tmp = tmp + 1 -> 172
172 -> join -> 174
173 -> join -> 174
174 -> join -> 175
175 -> Assume: i % 5 true -> 176; Assume: i % 5 false -> 178; join -> 206
176 -> Assign: tmp = tmp + 1 -> 177
177 -> join -> 179
178 -> join -> 179
179 -> join -> 180
180 -> Assume: i % 7 true -> 181; join -> 211
181 -> Assign: tmp = tmp + 1 -> 182; join -> 213
182 -> join -> 183
183 -> Assume: i % 11 true -> 184; Assume: i % 11 false -> 187;
join -> 217
184 -> join -> 185
185 -> Assign: tmp = tmp + 1 -> 186; join -> 219
186 -> join -> 188
187 -> join -> 188
188 -> join -> 189
189 -> Assign: tmp = tmp + 1 -> 190; join -> 223
190 -> join -> 191
191 -> Assign: i = i + 1 -> 192; join -> 225
192 -> join -> 193
193 -> Assume: i % 2 false -> 194; Assume: i % 2 true -> 195; join -> 227
194 -> join -> 198
195 -> Assign: tmp = tmp + 1 -> 196
196 -> join -> 198
198 -> join -> 199
199 -> Assume: i % 3 true -> 200; join -> 233
200 -> Assign: tmp = tmp + 1 -> 201
201 -> join -> 203
203 -> Assume: i % 5 false -> 204; Assume: i % 5 true -> 205; join -> 239
204 -> join -> 208
205 -> Assign: tmp = tmp + 1 -> 206
206 -> join -> 208
208 -> join -> 209
209 -> Assume: i % 7 true -> 210; join -> 245
210 -> Assign: tmp = tmp + 1 -> 211
193 -> join -> 196
196 -> join -> 201
201 -> join -> 206
206 -> join -> 211
211 -> join -> 213
213 -> Assume: i % 11 false -> 214; Assume: i % 11 true -> 215;
join -> 249
214 -> join -> 218
215 -> Assign: tmp = tmp + 1 -> 216; join -> 252
216 -> join -> 218
218 -> join -> 219
219 -> Assign: tmp = tmp + 1 -> 220; join -> 256
220 -> join -> 221
221 -> Assign: i = i + 1 -> 222; join -> 258
222 -> join -> 224
224 -> Assume: i < 100 true -> 226; join -> 261
226 -> join -> 227
227 -> Assume: i % 2 false -> 228; Assume: i % 2 true -> 229; join -> 265
228 -> join -> 232
229 -> Assign: tmp = tmp + 1 -> 230
230 -> join -> 232
232 -> join -> 233
233 -> Assume: i % 3 false -> 234; Assume: i % 3 true -> 235; join -> 271
234 -> join -> 238
235 -> Assign: tmp = tmp + 1 -> 236
236 -> join -> 238
238 -> join -> 239
239 -> Assume: i % 5 false -> 240; Assume: i % 5 true -> 241; join -> 277
240 -> join -> 244
241 -> Assign: tmp = tmp + 1 -> 242
242 -> join -> 244
244 -> join -> 245
245 -> Assume: i % 7 true -> 246; join -> 283
246 -> Assign: tmp = tmp + 1 -> 247; join -> 286
247 -> join -> 249
249 -> Assume: i % 11 false -> 250; Assume: i % 11 true -> 251;
join -> 290
250 -> join -> 255
251 -> join -> 252
252 -> Assign: tmp = tmp + 1 -> 253; join -> 293
253 -> join -> 255
255 -> join -> 256
256 -> Assign: tmp = tmp + 1 -> 257; join -> 297
257 -> join -> 258
258 -> Assign: i = i + 1 -> 259; join -> 299
259 -> join -> 261
261 -> join -> 265
265 -> join -> 271
271 -> join -> 277
277 -> join -> 283
283 -> join -> 286
286 -> join -> 290
290 -> join -> 293
293 -> join -> 297
297 -> join -> 299
299 -> Loop(4) 262 {[ 262 -> Assume: i < 100 true -> 264
264 -> Assume: i % 2 false -> 266;
Assume: i % 2 true -> 267
266 -> join -> 270
267 -> Assign: tmp = tmp + 1 -> 268
268 -> join -> 270
270 -> Assume: i % 3 false -> 272;
Assume: i % 3 true -> 273
272 -> join -> 276
273 -> Assign: tmp = tmp + 1 -> 274
274 -> join -> 276
276 -> Assume: i % 5 false -> 278;
Assume: i % 5 true -> 279
278 -> join -> 282
279 -> Assign: tmp = tmp + 1 -> 280
280 -> join -> 282
282 -> Assume: i % 7 false -> 284;
Assume: i % 7 true -> 285
284 -> join -> 289
285 -> Assign: tmp = tmp + 1 -> 287
287 -> join -> 289
289 -> Assume: i % 11 false -> 291;
Assume: i % 11 true -> 292
291 -> join -> 296
292 -> Assign: tmp = tmp + 1 -> 294
294 -> join -> 296
296 -> Assign: tmp = tmp + 1 -> 298
298 -> Assign: i = i + 1 -> 300 ]} -> 304
304 -> Assume: i < 100 false -> 305
305 -> leave_loop -> 306
306 -> LeaveScope: i -> 312 ]} at 312
213 -> join -> 217
217 -> join -> 219
219 -> join -> 223
223 -> join -> 225
225 -> Loop(4) 194 {[ 194 -> Assume: i < 100 true -> 195
195 -> Assume: i % 2 true -> 197;
Assume: i % 2 false -> 199
197 -> Assign: tmp = tmp + 1 -> 198
198 -> join -> 200
199 -> join -> 200
200 -> Assume: i % 3 true -> 202;
Assume: i % 3 false -> 204
202 -> Assign: tmp = tmp + 1 -> 203
203 -> join -> 205
204 -> join -> 205
205 -> Assume: i % 5 true -> 207;
Assume: i % 5 false -> 209
207 -> Assign: tmp = tmp + 1 -> 208
208 -> join -> 210
209 -> join -> 210
210 -> Assume: i % 7 true -> 212;
Assume: i % 7 false -> 215
212 -> Assign: tmp = tmp + 1 -> 214
214 -> join -> 216
215 -> join -> 216
216 -> Assume: i % 11 true -> 218;
Assume: i % 11 false -> 221
218 -> Assign: tmp = tmp + 1 -> 220
220 -> join -> 222
221 -> join -> 222
222 -> Assign: tmp = tmp + 1 -> 224
224 -> Assign: i = i + 1 -> 226 ]} -> 228
228 -> Assume: i < 100 false -> 229
229 -> leave_loop -> 230
230 -> LeaveScope: i -> 231
231 -> LeaveScope: i -> 232 ]} at 232
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
These dependencies hold at termination for the executions that terminate:
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
tmp; i
tmp; i
[inout] Inputs for function main:
\nothing
\nothing
tests/value/traces/oracle/test5.res.oracle
+ 519
− 492
View file @ 267a2df5
This diff is collapsed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment