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.

Author: tautschnig

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;
+}

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

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())
   {

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();