From ea9dc15f36ec553fe256b030f442e970e0abb9c8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 6 Jul 2018 13:55:36 +0000
Subject: [PATCH] goto-gcc: run original compiler even when output is /dev/null

---
 regression/goto-gcc/dev_null1/main.c    | 4 ++++
 regression/goto-gcc/dev_null1/test.desc | 8 ++++++++
 src/goto-cc/gcc_mode.cpp                | 2 +-
 3 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 regression/goto-gcc/dev_null1/main.c
 create mode 100644 regression/goto-gcc/dev_null1/test.desc

diff --git a/regression/goto-gcc/dev_null1/main.c b/regression/goto-gcc/dev_null1/main.c
new file mode 100644
index 00000000000..9dfa23ff198
--- /dev/null
+++ b/regression/goto-gcc/dev_null1/main.c
@@ -0,0 +1,4 @@
+void fails(void)
+{
+  asm volatile ( ".if (0 == 0); .error \"asm error\";.endif" );
+}
diff --git a/regression/goto-gcc/dev_null1/test.desc b/regression/goto-gcc/dev_null1/test.desc
new file mode 100644
index 00000000000..215049ec4f0
--- /dev/null
+++ b/regression/goto-gcc/dev_null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+-o /dev/null
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index 229b8804b5e..373ddb21411 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -914,7 +914,7 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
   if(output_files.empty() ||
      (output_files.size()==1 &&
       output_files.front()=="/dev/null"))
-    return EX_OK;
+    return run_gcc(compiler);
 
   debug() << "Running " << native_tool_name
           << " to generate hybrid binary" << eom;