Exclude bugged jbmc/regression/jbmc/ tests on windows

Author: NlightNFotis

jbmc/regression/jbmc/CMakeLists.txt

@@ -1,5 +1,11 @@
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+  set(exclude_win_broken_tests -X winbug)
+else()
+  set(exclude_win_broken_tests "")
+endif()
+
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace" ${exclude_win_broken_tests}
 )
 
 if(DEFINED BDD_GUARDS)
@@ -8,12 +14,14 @@ if(DEFINED BDD_GUARDS)
             "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace --symex-driven-lazy-loading"
             "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
             "CORE"
+            ${exclude_win_broken_tests}
     )
 else()
     add_test_pl_profile(
             "jbmc-symex-driven-lazy-loading"
             "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace --symex-driven-lazy-loading"
             "-C;-X;symex-driven-lazy-loading-expected-failure;-X;bdd-expected-timeout;-s;symex-driven-loading"
             "CORE"
+            ${exclude_win_broken_tests}
     )
 endif()

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc

@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Test
 --function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.2" --static-values static-values.json
 Generated 0 VCC[(]s[)], 0 remaining after simplification

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc

@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Test
 --function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.1"
 Generated 0 VCC[(]s[)], 0 remaining after simplification

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc

@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Test
 --function Test.charArray --property "java::Test.charArray:()[C.assertion.2" --static-values static-values.json
 Generated 0 VCC[(]s[)], 0 remaining after simplification

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc

@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Test
 --function Test.charArray --property "java::Test.charArray:()[C.assertion.1"
 Generated 0 VCC[(]s[)], 0 remaining after simplification

jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc

@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 My
 --function My.intervalUnion --java-assume-inputs-interval [3:3] --property "java::My.intervalUnion:(I)V.assertion.1" --property "java::My.intervalUnion:(I)V.assertion.2" --property "java::My.intervalUnion:(I)V.assertion.3" --property "java::My.intervalUnion:(I)V.assertion.4" --property "java::My.intervalUnion:(I)V.assertion.6"
 ^EXIT=0$

jbmc/regression/jbmc/enum/test_enum_switch.desc

@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Foo
 --trace --depth 1024 --java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 10 --function "Foo.foo" --java-unwind-enum-static
 assertion at file Foo.java line 6 .*: FAILURE

jbmc/regression/jbmc/nondet-array-size/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 TestClass
 --function "TestClass.minimalJbmc" --unwind 5 --max-nondet-string-length 10 --java-unwind-enum-static --trace --json-ui
 ^EXIT=10$

jbmc/regression/jbmc/nondet-static/test.desc

@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 My
 --function "My.<init>" --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$

jbmc/regression/jbmc/parameter-annotation-not-null/test_kotlin.desc

@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 MainKotlin
 --function "MainKotlin.<init>" --show-properties
 ^EXIT=0$