Skip to content

Commit a503f5c

Browse files
tautschnigtautschnig
authored
Merge pull request #5580 from tautschnig/single-quotes
Use single quotes to make regression tests work on Windows
2 parents ee3b3fb + 92e3249 commit a503f5c

File tree

115 files changed

+225
-254
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

115 files changed

+225
-254
lines changed

‎jbmc/regression/jbmc-strings/CMakeLists.txt

Lines changed: 7 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,10 @@
1-
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
2-
set(exclude_win_broken_tests -X winbug)
3-
else()
4-
set(exclude_win_broken_tests "")
5-
endif()
6-
71
add_test_pl_tests(
8-
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation" ${exclude_win_broken_tests}
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
93
)
104

11-
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
12-
message(WARNING "skipping broken jbmc-strings/ tests on windows")
13-
else()
14-
add_test_pl_profile(
15-
"jbmc-strings-symex-driven-lazy-loading"
16-
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
17-
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
18-
"CORE"
19-
)
20-
endif()
5+
add_test_pl_profile(
6+
"jbmc-strings-symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
8+
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
9+
"CORE"
10+
)

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail1:()V.assertion.1"
3+
--function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail1:()V.assertion.1'
44
^VERIFICATION FAILED$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1_vcc.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail1:()V.assertion.1" --show-vcc
3+
--function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail1:()V.assertion.1' --show-vcc
44
^EXIT=0$
55
^SIGNAL=0$
66
\{1\} false

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail2:()V.assertion.1"
3+
--function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail2:()V.assertion.1'
44
^VERIFICATION FAILED$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2_vcc.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail2:()V.assertion.1" --show-vcc
3+
--function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail2:()V.assertion.1' --show-vcc
44
^EXIT=0$
55
^SIGNAL=0$
66
\{1\} false

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail3:()V.assertion.1"
3+
--function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail3:()V.assertion.1'
44
^VERIFICATION FAILED$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3_vcc.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail3:()V.assertion.1" --show-vcc
3+
--function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail3:()V.assertion.1' --show-vcc
44
^EXIT=0$
55
^SIGNAL=0$
66
\{1\} false

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail4:()V.assertion.1"
3+
--function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail4:()V.assertion.1'
44
^VERIFICATION FAILED$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4_vcc.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail4:()V.assertion.1" --show-vcc
3+
--function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail4:()V.assertion.1' --show-vcc
44
^EXIT=0$
55
^SIGNAL=0$
66
\{1\} false

‎jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantEndsWithFail:()V.assertion.1"
3+
--function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantEndsWithFail:()V.assertion.1'
44
^VERIFICATION FAILED$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail_vcc.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantEndsWithFail:()V.assertion.1" --show-vcc
3+
--function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantEndsWithFail:()V.assertion.1' --show-vcc
44
^EXIT=0$
55
^SIGNAL=0$
66
\{1\} false

‎jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_pass.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantEndsWithPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantEndsWithPass:()V.assertion.1"
3+
--function Main.constantEndsWithPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantEndsWithPass:()V.assertion.1'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantIsEmptyFail:()V.assertion.1"
3+
--function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantIsEmptyFail:()V.assertion.1'
44
^VERIFICATION FAILED$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail_vcc.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-vcc --property "java::Main.constantIsEmptyFail:()V.assertion.1"
3+
--function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-vcc --property 'java::Main.constantIsEmptyFail:()V.assertion.1'
44
^EXIT=0$
55
^SIGNAL=0$
66
\{1\} false

‎jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_pass.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.constantIsEmptyPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantIsEmptyPass:()V.assertion.1"
3+
--function Main.constantIsEmptyPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantIsEmptyPass:()V.assertion.1'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend01/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
3+
--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2"
3+
--function Main.test1 --property 'java::Main.test1:()V.assertion.1' --property 'java::Main.test1:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2"
3+
--function Main.test2 --property 'java::Main.test2:()V.assertion.1' --property 'java::Main.test2:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2"
3+
--function Main.test3 --property 'java::Main.test3:()V.assertion.1' --property 'java::Main.test3:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation01/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
3+
--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2"
3+
--function Main.test1 --property 'java::Main.test1:()V.assertion.1' --property 'java::Main.test1:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2"
3+
--function Main.test2 --property 'java::Main.test2:()V.assertion.1' --property 'java::Main.test2:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2"
3+
--function Main.test3 --property 'java::Main.test3:()V.assertion.1' --property 'java::Main.test3:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.test1 --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1"
3+
--function Main.test1 --property 'java::Main.test1:(Ljava/lang/String;)V.assertion.1'
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.test2 --property "java::Main.test2:(Ljava/lang/String;)V.assertion.1"
3+
--function Main.test2 --property 'java::Main.test2:(Ljava/lang/String;)V.assertion.1'
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.test3 --property "java::Main.test3:(Ljava/lang/String;)V.assertion.1"
3+
--function Main.test3 --property 'java::Main.test3:(Ljava/lang/String;)V.assertion.1'
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test --property "java::Main.test:()V.assertion.1" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function Main.test --property 'java::Main.test:()V.assertion.1' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
3+
--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE winbug
1+
CORE
22
Main
3-
--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
3+
--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;)V.assertion.1"
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;)V.assertion.1'
44
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.1" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.1' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.10" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.10' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.11" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.11' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.12" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.12' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.2" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.2' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.3" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.3' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.4" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.4' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.5" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.5' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.6" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.6' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.7" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.7' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.8" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.8' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE symex-driven-lazy-loading-expected-failure winbug
1+
CORE symex-driven-lazy-loading-expected-failure
22
Main
3-
--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.9" --show-vcc
3+
--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.9' --show-vcc
44
^Generated 1 VCC\(s\), 1 remaining after simplification$
55
^EXIT=0$
66
^SIGNAL=0$

0 commit comments

Comments
 (0)