Skip to content

Commit 7525710

Browse files
author
Joel Allred
committed
Regression test for cbmc#2497
This example does not terminate without the fix provided in #2497. Infinite loop in simplify_expr.
1 parent ccda412 commit 7525710

File tree

3 files changed

+21
-0
lines changed

3 files changed

+21
-0
lines changed
Binary file not shown.
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.class
3+
--function test.check
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
Checks that a non-termination bug no longer occurs in simplify_byte_extract
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class test {
2+
3+
public static int check()
4+
{
5+
boolean[] assigned = new boolean[3];
6+
if (assigned[0] == false) {
7+
assert false;
8+
}
9+
return 1;
10+
}
11+
}

0 commit comments

Comments
 (0)