From 575d386a4d01d0f10c0ea2898741cf79aa3d2a06 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 6 May 2019 22:31:04 +0000
Subject: [PATCH] C front-end: Do not lose comments in type checking

In case of declarations and function calls we need to carry over
comments from the statement's source location into individual
subexpressions as the source location of those subexpressions will be
used when generating the goto program instruction.
---
 regression/cbmc/pragma_cprover2/main.c    | 24 +++++++++++++++++++++++
 regression/cbmc/pragma_cprover2/test.desc | 11 +++++++++++
 src/ansi-c/c_typecheck_code.cpp           |  9 +++++++++
 src/ansi-c/c_typecheck_expr.cpp           |  4 ++++
 4 files changed, 48 insertions(+)
 create mode 100644 regression/cbmc/pragma_cprover2/main.c
 create mode 100644 regression/cbmc/pragma_cprover2/test.desc

diff --git a/regression/cbmc/pragma_cprover2/main.c b/regression/cbmc/pragma_cprover2/main.c
new file mode 100644
index 00000000000..14f1d8ee805
--- /dev/null
+++ b/regression/cbmc/pragma_cprover2/main.c
@@ -0,0 +1,24 @@
+int foo(int x)
+{
+  return x;
+}
+
+int main()
+{
+  int n;
+
+#pragma CPROVER check push
+#pragma CPROVER check disable "signed-overflow"
+  // do not generate assertions for the following statements
+  int x = n + n;
+  ++n;
+  n++;
+  n += 1;
+  foo(x + n);
+  // pop all annotations
+#pragma CPROVER check pop
+  // but do generate assertions for these
+  x = n + n;
+  foo(x + n);
+  return x;
+}
diff --git a/regression/cbmc/pragma_cprover2/test.desc b/regression/cbmc/pragma_cprover2/test.desc
new file mode 100644
index 00000000000..fc1f888dfcf
--- /dev/null
+++ b/regression/cbmc/pragma_cprover2/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--signed-overflow-check
+^\[main.overflow\.1\] line 21 arithmetic overflow on signed \+ in n \+ n: FAILURE$
+^\[main.overflow\.2\] line 22 arithmetic overflow on signed \+ in x \+ n: FAILURE$
+^\*\* 2 of 2 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 9e042a0bedd..f8104ffb0cc 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -243,7 +243,16 @@ void c_typecheck_baset::typecheck_decl(codet &code)
   }
 
   ansi_c_declarationt declaration;
+  irep_idt comment = code.source_location().get_comment();
   declaration.swap(code.op0());
+  if(!comment.empty())
+  {
+    for(auto &d : declaration.declarators())
+    {
+      if(d.source_location().get_comment().empty())
+        d.add_source_location().set_comment(comment);
+    }
+  }
 
   if(declaration.get_is_static_assert())
   {
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index bca4267c727..7fb21e6ac62 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2019,6 +2019,10 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
     throw 0;
   }
 
+  irep_idt comment = expr.source_location().get_comment();
+  if(!comment.empty() && f_op.source_location().get_comment().empty())
+    f_op.add_source_location().set_comment(comment);
+
   const code_typet &code_type=to_code_type(f_op.type());
 
   expr.type()=code_type.return_type();