Skip to content

Commit

Permalink
Add test for instanceof String
Browse files Browse the repository at this point in the history
This checks the bug with class identifier of nondet strings was fixed.
  • Loading branch information
romainbrenguier committed Nov 21, 2017
1 parent 12ca989 commit 10d3857
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 0 deletions.
Binary file added regression/jbmc-strings/instanceof/Test.class
Binary file not shown.
9 changes: 9 additions & 0 deletions regression/jbmc-strings/instanceof/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
public class Test {

public static String check(String s) {
if (s == null)
return "null";
assert(s instanceof String);
return "non-null";
}
}
8 changes: 8 additions & 0 deletions regression/jbmc-strings/instanceof/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
Test.class
--refine-strings --string-max-length 1000 --function Test.check
^EXIT=0$
^SIGNAL=0$
assertion at file Test.java line 6 .* SUCCESS$
^VERIFICATION SUCCESSFUL$
--

0 comments on commit 10d3857

Please sign in to comment.