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

object-bits was not supported by all of goto-cc's command-line front-end
variants. While at it, also make other options consistently available.

Author: tautschnig

Diff for: 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}"
 )

Diff for: 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$

Diff for: 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$

Diff for: src/goto-cc/armcc_cmdline.cpp

@@ -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",
@@ -256,6 +259,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",

Diff for: src/goto-cc/bcc_cmdline.cpp

@@ -24,6 +24,8 @@ const char *goto_bcc_options_with_argument[]=
   "--native-compiler",
   "--native-linker",
   "--print-rejected-preprocessed-source",
+  "--mangle-suffix",
+  "--object-bits",
   nullptr
 };
 

Diff for: 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)
         {

Diff for: src/goto-cc/ms_link_cmdline.cpp

@@ -25,7 +25,8 @@ Author: Daniel Kroening
 const char *non_ms_link_options[]=
 {
   "--help",
-  "--verbosity"
+  "--verbosity",
+  "--validate-goto-model"
 };
 
 bool ms_link_cmdlinet::parse(const std::vector<std::string> &arguments)