Skip to content

Commit 6d6d9d6

Browse files
Joel Allredromainbrenguier
Joel Allred
authored andcommitted
Add first fixed_bugs test
For bug diffblue#95
1 parent 00f5d7f commit 6d6d9d6

File tree

4 files changed

+26
-0
lines changed

4 files changed

+26
-0
lines changed
+9
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.
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+
--
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)