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 09724a8 commit bb28bf8Copy full SHA for bb28bf8
jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.class
820 Bytes
jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.java
@@ -0,0 +1,11 @@
1
+public class Main {
2
+
3
+ public void constantIndexOf() {
4
+ String s1 = "abcabc";
5
+ Character b = 'b';
6
+ assert s1.indexOf(b) == 1;
7
+ assert s1.indexOf(b, -10) == 1;
8
+ assert s1.indexOf(b, 3) == 4;
9
+ assert s1.indexOf(b, 10) == -1;
10
+ }
11
+}
jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/test-models-library.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
0 commit comments