Synchronise goto-cc command-line options to re-enable Windows regression tests

regression/goto-cc-cbmc-shared-options/CMakeLists.txt

@@ -1,11 +1,9 @@
 if(WIN32)
     set(is_windows true)
-    set(exclude_broken_windows_tests -X winbug)
 else()
     set(is_windows false)
-    set(exclude_broken_windows_tests "")
 endif()
 
 add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}" ${exclude_broken_windows_tests}
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
 )

regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc

@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 test.c
 --function main --object-bits 6
 ^EXIT=10$

regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc

@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 test.c
 --function main --object-bits 10
 ^EXIT=10$

src/goto-cc/armcc_cmdline.cpp

@@ -25,7 +25,7 @@ Author: Daniel Kroening
 /// \return none
 // see
 // http://infocenter.arm.com/help/topic/com.arm.doc.dui0472c/Cchbggjb.html
-
+// clang-format off
 static const char *options_no_arg[]=
 {
   // goto-cc-specific
@@ -44,6 +44,9 @@ static const char *options_no_arg[]=
   "--no-arch",
   "--no-library",
   "--string-abstraction",
+  "--validate-goto-model",
+  "-?",
+  "--export-file-local-symbols",
 
   // armcc
   "--help",
@@ -201,7 +204,6 @@ static const char *options_no_arg[]=
   nullptr
 };
 
-// clang-format off
 static const std::vector<std::string> options_with_prefix
 {
   "--project=",
@@ -256,6 +258,9 @@ static const std::vector<std::string> options_with_arg
   // goto-cc specific
   "--verbosity",
   "--function",
+  "--print-rejected-preprocessed-source",
+  "--mangle-suffix",
+  "--object-bits",
 
   // armcc-specific
   "-D",

src/goto-cc/bcc_cmdline.cpp

@@ -16,6 +16,7 @@ Author: Michael Tautschnig
 
 #include <util/prefix.h>
 
+// clang-format off
 // non-bcc options
 const char *goto_bcc_options_with_argument[]=
 {
@@ -24,6 +25,8 @@ const char *goto_bcc_options_with_argument[]=
   "--native-compiler",
   "--native-linker",
   "--print-rejected-preprocessed-source",
+  "--mangle-suffix",
+  "--object-bits",
   nullptr
 };
 
@@ -66,6 +69,7 @@ const char *bcc_options_with_argument[]=
   "-t",
   nullptr
 };
+// clang-format on
 
 bool bcc_cmdlinet::parse(int argc, const char **argv)
 {

src/goto-cc/ms_cl_cmdline.cpp

@@ -48,6 +48,7 @@ const char *non_ms_cl_options[]=
   "--validate-goto-model",
   "--export-file-local-symbols",
   "--mangle-suffix",
+  "--object-bits",
   nullptr
 };
 // clang-format on
@@ -63,7 +64,7 @@ bool ms_cl_cmdlinet::parse(const std::vector<std::string> &arguments)
 
       if(
         arguments[i] == "--verbosity" || arguments[i] == "--function" ||
-        arguments[i] == "--mangle-suffix")
+        arguments[i] == "--mangle-suffix" || arguments[i] == "--object-bits")
       {
         if(i < arguments.size() - 1)
         {

src/goto-cc/ms_link_cmdline.cpp

@@ -19,14 +19,17 @@ Author: Daniel Kroening
 
 #include <util/unicode.h>
 
+// clang-format off
 /// parses the command line options into a cmdlinet
 /// \par parameters: argument count, argument strings
 /// \return none
 const char *non_ms_link_options[]=
 {
   "--help",
-  "--verbosity"
+  "--verbosity",
+  "--validate-goto-model"
 };
+// clang-format on
 
 bool ms_link_cmdlinet::parse(const std::vector<std::string> &arguments)
 {