From 645bf8ddf47473eeb31dfb8d4e56791f1774c482 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 24 Aug 2017 14:57:49 +0100
Subject: [PATCH] disable source output in ASM

---
 src/goto-cc/gcc_mode.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index db33ac5b194..0804dacdd6d 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -1022,6 +1022,9 @@ int gcc_modet::asm_output(
       output_files.begin()->second=="/dev/null"))
     return EX_OK;
 
+  #if 0
+  // The below disturbs some scripts that rummage through assembly
+  // output.
   debug()
     << "Appending preprocessed sources to generate hybrid asm output"
     << eom;
@@ -1053,6 +1056,7 @@ int gcc_modet::asm_output(
       os << comment << comment << line << '\n';
     }
   }
+  #endif
 
   return EX_OK;
 }