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$

0 commit comments

Comments
 (0)