Skip to content

Commit 8cce1c5

Browse files
author
martin
committed
Test case for the evaluation of (false && x) in the variable sensitivity domain.
1 parent 8d6a842 commit 8cce1c5

File tree

2 files changed

+35
-0
lines changed
  • regression/goto-analyzer/variable-sensitivity-annihiliator-test

2 files changed

+35
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
extern int g_in1;
2+
extern int g_in2;
3+
4+
int g_out;
5+
6+
void func(void);
7+
8+
void main(void)
9+
{
10+
g_in1 = 1;
11+
12+
func();
13+
}
14+
15+
void func(void)
16+
{
17+
if (g_in1 == 0)
18+
g_out = 1; // unreachable.
19+
20+
if (g_in2 == 0)
21+
g_out = 2;
22+
23+
if (g_in1 == 0 && g_in2 == 0)
24+
g_out = 3; // unreachable, but not .
25+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --pointers --arrays --structs --unreachable-instructions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 18 function func
7+
g_out = 1;
8+
line 24 function func
9+
g_out = 3;
10+
--

0 commit comments

Comments
 (0)