From 774abc17e046eda470abcb4b07ea858ef027530c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 13 Nov 2020 02:07:58 +0000
Subject: [PATCH] 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.
---
 regression/goto-cc-cbmc-shared-options/CMakeLists.txt    | 4 +---
 .../object-bits/fewer_bits.desc                          | 2 +-
 .../object-bits/more_bits.desc                           | 2 +-
 src/goto-cc/armcc_cmdline.cpp                            | 9 +++++++--
 src/goto-cc/bcc_cmdline.cpp                              | 4 ++++
 src/goto-cc/ms_cl_cmdline.cpp                            | 3 ++-
 src/goto-cc/ms_link_cmdline.cpp                          | 5 ++++-
 7 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/regression/goto-cc-cbmc-shared-options/CMakeLists.txt b/regression/goto-cc-cbmc-shared-options/CMakeLists.txt
index b29f1a50349..53647ddb692 100644
--- a/regression/goto-cc-cbmc-shared-options/CMakeLists.txt
+++ b/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 --git a/regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc b/regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc
index 32723acdbbb..ed34ce893c4 100644
--- a/regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc
+++ b/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 --git a/regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc b/regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc
index a0f25c0b4aa..cabc3e744d2 100644
--- a/regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc
+++ b/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 --git a/src/goto-cc/armcc_cmdline.cpp b/src/goto-cc/armcc_cmdline.cpp
index be1d2c19c67..61a0d2f1e57 100644
--- a/src/goto-cc/armcc_cmdline.cpp
+++ b/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",
diff --git a/src/goto-cc/bcc_cmdline.cpp b/src/goto-cc/bcc_cmdline.cpp
index f4c0626b142..aaf8e767f66 100644
--- a/src/goto-cc/bcc_cmdline.cpp
+++ b/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)
 {
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp
index 7b2dcc21036..03e390decf8 100644
--- a/src/goto-cc/ms_cl_cmdline.cpp
+++ b/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 --git a/src/goto-cc/ms_link_cmdline.cpp b/src/goto-cc/ms_link_cmdline.cpp
index be75c57d343..ca643d6092b 100644
--- a/src/goto-cc/ms_link_cmdline.cpp
+++ b/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)
 {