Skip to content

Commit 91e4706

Browse files
author
martin
committed
Check the logging output generated from ai_baset et al.
This does not check whether the debug output is actually sensible or useful, just whether it is present at the different --verbosity levels.
1 parent f558258 commit 91e4706

File tree

5 files changed

+121
-0
lines changed

5 files changed

+121
-0
lines changed

‎regression/goto-analyzer/logging/main.c

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
#include <assert.h>
2+
3+
int global;
4+
5+
int f00(int x)
6+
{
7+
return global + x;
8+
}
9+
10+
int main(void)
11+
{
12+
int local;
13+
unsigned int nondet;
14+
15+
local = 1;
16+
global = 1;
17+
18+
assert(local == global);
19+
20+
if(nondet)
21+
{
22+
local = 2;
23+
}
24+
if(nondet)
25+
{
26+
global = 2;
27+
}
28+
29+
assert(local == global);
30+
31+
do
32+
{
33+
local = 3;
34+
global = 3;
35+
} while(nondet-- > 0);
36+
37+
assert(local == global);
38+
39+
local = 4;
40+
global = 4;
41+
42+
local = f00(1);
43+
global = f00(1);
44+
45+
assert(local == global);
46+
47+
return 0;
48+
}

‎regression/goto-analyzer/logging/test-recursive-interprocedural-10.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.c
3+
--verify --recursive-interprocedural --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 10
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
7+
^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
8+
^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
9+
^\[main\.assertion\.4] line \d+ assertion local == global: UNKNOWN$
10+
^ai_baset::visit \d+ in main$
11+
^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
12+
^ai_baset::visit_function_call at \d+$
13+
^ai_baset::visit_end_function main$
14+
^ai_recursive_interproceduralt::visit_edge_function_call from \d+ to \d+$
15+
^p = local_control_flow_history : location \d+
16+
^global \(\) -> 0 @ \[\d+\]$
17+
--
18+
^warning: ignoring

‎regression/goto-analyzer/logging/test-recursive-interprocedural-8.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.c
3+
--verify --recursive-interprocedural --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 8
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
7+
^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
8+
^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
9+
^\[main\.assertion\.4] line \d+ assertion local == global: UNKNOWN$
10+
--
11+
^warning: ignoring
12+
^p = local_control_flow_history : location \d+
13+
^global \(\) -> 0 @ \[\d+\]$
14+
^ai_baset::visit \d+ in main$
15+
^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
16+
^ai_baset::visit_function_call at \d+$
17+
^ai_baset::visit_end_function main$
18+
^ai_recursive_interproceduralt::visit_edge_function_call from \d+ to \d+$

‎regression/goto-analyzer/logging/test-recursive-interprocedural-9.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.c
3+
--verify --recursive-interprocedural --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 9
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
7+
^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
8+
^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
9+
^\[main\.assertion\.4] line \d+ assertion local == global: UNKNOWN$
10+
^ai_baset::visit \d+ in main$
11+
^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
12+
^ai_baset::visit_function_call at \d+$
13+
^ai_baset::visit_end_function main$
14+
^ai_recursive_interproceduralt::visit_edge_function_call from \d+ to \d+$
15+
--
16+
^warning: ignoring
17+
^p = local_control_flow_history : location \d+
18+
^global \(\) -> 0 @ \[\d+\]$

‎regression/goto-analyzer/logging/test-three-way-merge-10.desc

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE
2+
main.c
3+
--verify --three-way-merge --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 10
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
7+
^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
8+
^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
9+
^\[main\.assertion\.4] line \d+ assertion local == global: SUCCESS$
10+
^ai_baset::visit \d+ in main$
11+
^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
12+
^ai_baset::visit_function_call at \d+$
13+
^ai_baset::visit_end_function main$
14+
^ai_three_way_merget::visit_edge_function_call from \d+ to \d+$
15+
^ai_three_way_merget::visit_edge_function_call edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. three way merge\.\.\. merging\.\.\. result queued\.$
16+
^p = local_control_flow_history : location \d+
17+
^global \(\) -> 0 @ \[\d+\]$
18+
--
19+
^warning: ignoring

0 commit comments

Comments
 (0)