Skip to content

Commit 4f3d61a

Browse files
author
Joel Allred
committed
Add first fixed_bugs test
For bug diffblue#95
1 parent 9140665 commit 4f3d61a

File tree

4 files changed

+26
-0
lines changed

4 files changed

+26
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
2+
test:
3+
@../../test.pl -c ../../../../src/cbmc/cbmc
4+
5+
testfuture:
6+
@../../test.pl -c ../../../../src/cbmc/cbmc -CF
7+
8+
testall:
9+
@../../test.pl -c ../../../../src/cbmc/cbmc -CFTK
Binary file not shown.
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
test.class
3+
--string-refine
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
public class test
2+
{
3+
public static void main(String[] args)
4+
{
5+
StringBuilder sb = new StringBuilder(args[0]);
6+
sb.append("Z");
7+
String s = sb.toString();
8+
assert(s.equals("fg"));
9+
}
10+
}

0 commit comments

Comments
 (0)