File tree Expand file tree Collapse file tree 5 files changed +121
-0
lines changed
regression/goto-analyzer/logging Expand file tree Collapse file tree 5 files changed +121
-0
lines changed Original file line number Diff line number Diff line change 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+ }
Original file line number Diff line number Diff line change 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
Original file line number Diff line number Diff line change 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+$
Original file line number Diff line number Diff line change 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+\]$
Original file line number Diff line number Diff line change 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
You can’t perform that action at this time.
0 commit comments