Skip to content

Commit bcc5f8c

Browse files
committed
Add classpath option to float to string test and mark it as KNOWNBUG
The test previously passed by accident as it did not specify the models jar via the classpath option of jbmc. Thus, the models were not loaded and the string operations were nondet'ed, and verification failed as required by the test.
1 parent 779d11d commit bcc5f8c

File tree

1 file changed

+2
-2
lines changed
  • jbmc/regression/jbmc-strings/StringValueOf09

1 file changed

+2
-2
lines changed

jbmc/regression/jbmc-strings/StringValueOf09/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE
1+
KNOWNBUG
22
StringValueOf09.class
3-
--max-nondet-string-length 1000
3+
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion\.1\] .* line 7 .* FAILURE$

0 commit comments

Comments
 (0)