We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 12ca989 commit 10d3857Copy full SHA for 10d3857
regression/jbmc-strings/instanceof/Test.class
602 Bytes
regression/jbmc-strings/instanceof/Test.java
@@ -0,0 +1,9 @@
1
+public class Test {
2
+
3
+ public static String check(String s) {
4
+ if (s == null)
5
+ return "null";
6
+ assert(s instanceof String);
7
+ return "non-null";
8
+ }
9
+}
regression/jbmc-strings/instanceof/test.desc
@@ -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 commit comments