Merge pull request #4622 from tautschnig/maintain-comments

C front-end: Do not lose comments in type checking

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