Make sure pragmas propagate to all source locations

regression/cbmc/pragma_cprover2/main.c

@@ -5,12 +5,12 @@ int foo(int x)
 
 int main()
 {
-  int n;
+  int m, n;
 
 #pragma CPROVER check push
 #pragma CPROVER check disable "signed-overflow"
   // do not generate assertions for the following statements
-  int x = n + n;
+  int x = m = n + n;
   ++n;
   n++;
   n += 1;

src/analyses/goto_check.cpp

@@ -29,7 +29,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
-#include <util/string_utils.h>
 
 #include <langapi/language.h>
 #include <langapi/mode.h>
@@ -1805,35 +1804,31 @@ void goto_checkt::goto_check(
     goto_programt::instructiont &i=*it;
 
     flag_resett flag_resetter;
-    if(!i.source_location.get_comment().empty())
+    const auto &pragmas = i.source_location.get_pragmas();
+    for(const auto &d : pragmas)
     {
-      auto disabled_checks = split_string(
-        id2string(i.source_location.get_comment()), ',', true, true);
-      for(const auto &d : disabled_checks)
-      {
-        if(d == "disable:bounds-check")
-          flag_resetter.set_flag(enable_bounds_check, false);
-        else if(d == "disable:pointer-check")
-          flag_resetter.set_flag(enable_pointer_check, false);
-        else if(d == "disable:memory-leak-check")
-          flag_resetter.set_flag(enable_memory_leak_check, false);
-        else if(d == "disable:div-by-zero-check")
-          flag_resetter.set_flag(enable_div_by_zero_check, false);
-        else if(d == "disable:signed-overflow-check")
-          flag_resetter.set_flag(enable_signed_overflow_check, false);
-        else if(d == "disable:unsigned-overflow-check")
-          flag_resetter.set_flag(enable_unsigned_overflow_check, false);
-        else if(d == "disable:pointer-overflow-check")
-          flag_resetter.set_flag(enable_pointer_overflow_check, false);
-        else if(d == "disable:float-overflow-check")
-          flag_resetter.set_flag(enable_float_overflow_check, false);
-        else if(d == "disable:conversion-check")
-          flag_resetter.set_flag(enable_conversion_check, false);
-        else if(d == "disable:undefined-shift-check")
-          flag_resetter.set_flag(enable_undefined_shift_check, false);
-        else if(d == "disable:nan-check")
-          flag_resetter.set_flag(enable_nan_check, false);
-      }
+      if(d.first == "disable:bounds-check")
+        flag_resetter.set_flag(enable_bounds_check, false);
+      else if(d.first == "disable:pointer-check")
+        flag_resetter.set_flag(enable_pointer_check, false);
+      else if(d.first == "disable:memory-leak-check")
+        flag_resetter.set_flag(enable_memory_leak_check, false);
+      else if(d.first == "disable:div-by-zero-check")
+        flag_resetter.set_flag(enable_div_by_zero_check, false);
+      else if(d.first == "disable:signed-overflow-check")
+        flag_resetter.set_flag(enable_signed_overflow_check, false);
+      else if(d.first == "disable:unsigned-overflow-check")
+        flag_resetter.set_flag(enable_unsigned_overflow_check, false);
+      else if(d.first == "disable:pointer-overflow-check")
+        flag_resetter.set_flag(enable_pointer_overflow_check, false);
+      else if(d.first == "disable:float-overflow-check")
+        flag_resetter.set_flag(enable_float_overflow_check, false);
+      else if(d.first == "disable:conversion-check")
+        flag_resetter.set_flag(enable_conversion_check, false);
+      else if(d.first == "disable:undefined-shift-check")
+        flag_resetter.set_flag(enable_undefined_shift_check, false);
+      else if(d.first == "disable:nan-check")
+        flag_resetter.set_flag(enable_nan_check, false);
     }
 
     new_code.clear();

src/ansi-c/ansi_c_parser.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANSI_C_ANSI_C_PARSER_H
 
 #include <cassert>
+#include <set>
 
 #include <util/parser.h>
 #include <util/expr.h>
@@ -69,7 +70,7 @@ class ansi_c_parsert:public parsert
   unsigned parenthesis_counter;
   std::string string_literal;
   std::list<exprt> pragma_pack;
-  std::list<irep_idt> pragma_cprover;
+  std::list<std::set<irep_idt>> pragma_cprover;
 
   typedef configt::ansi_ct::flavourt modet;
   modet mode;
@@ -145,6 +146,16 @@ class ansi_c_parsert:public parsert
     lookup(base_name, identifier, false, true);
     return identifier;
   }
+
+  void set_pragma_cprover()
+  {
+    source_location.remove(ID_pragma);
+    for(const auto &pragma_set : pragma_cprover)
+    {
+      for(const auto &pragma : pragma_set)
+        source_location.add_pragma(pragma);
+    }
+  }
 };
 
 extern ansi_c_parsert ansi_c_parser;

src/ansi-c/c_typecheck_code.cpp

@@ -243,16 +243,7 @@ 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,10 +2019,6 @@ 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();

src/ansi-c/expr2c.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/string_constant.h>
+#include <util/string_utils.h>
 #include <util/suffix.h>
 #include <util/symbol.h>
 
@@ -2796,11 +2797,31 @@ std::string expr2ct::convert_code(
 {
   static bool comment_done=false;
 
-  if(!comment_done && !src.source_location().get_comment().empty())
+  if(
+    !comment_done && (!src.source_location().get_comment().empty() ||
+                      !src.source_location().get_pragmas().empty()))
   {
     comment_done=true;
-    std::string dest=indent_str(indent);
-    dest+="/* "+id2string(src.source_location().get_comment())+" */\n";
+    std::string dest;
+    if(!src.source_location().get_comment().empty())
+    {
+      dest += indent_str(indent);
+      dest += "/* " + id2string(src.source_location().get_comment()) + " */\n";
+    }
+    if(!src.source_location().get_pragmas().empty())
+    {
+      std::ostringstream oss;
+      oss << indent_str(indent) << "/* ";
+      const auto &pragmas = src.source_location().get_pragmas();
+      join_strings(
+        oss,
+        pragmas.begin(),
+        pragmas.end(),
+        ',',
+        [](const std::pair<irep_idt, irept> &p) { return p.first; });
+      oss << " */\n";
+      dest += oss.str();
+    }
     dest+=convert_code(src, indent);
     comment_done=false;
     return dest;

src/ansi-c/parser.y

@@ -24,10 +24,6 @@ extern char *yyansi_ctext;
 
 #include "literals/convert_integer_literal.h"
 
-#include <util/string_utils.h>
-
-#include <sstream>
-
 #include "ansi_c_y.tab.h"
 
 #ifdef _MSC_VER
@@ -2310,38 +2306,10 @@ statement_list:
           statement
         {
           init($$);
-          if(!PARSER.pragma_cprover.empty())
-          {
-            std::ostringstream oss;
-            join_strings(
-              oss,
-              PARSER.pragma_cprover.begin(),
-              PARSER.pragma_cprover.end(),
-              ',');
-            parser_stack($1).add_source_location().set_comment(oss.str());
-            Forall_operands(it, parser_stack($1))
-            {
-              it->add_source_location().set_comment(oss.str());
-            }
-          }
           mto($$, $1);
         }
         | statement_list statement
         {
-          if(!PARSER.pragma_cprover.empty())
-          {
-            std::ostringstream oss;
-            join_strings(
-              oss,
-              PARSER.pragma_cprover.begin(),
-              PARSER.pragma_cprover.end(),
-              ',');
-            parser_stack($2).add_source_location().set_comment(oss.str());
-            Forall_operands(it, parser_stack($2))
-            {
-              it->add_source_location().set_comment(oss.str());
-            }
-          }
           mto($$, $2);
         }
         ;

src/ansi-c/scanner.l

@@ -402,11 +402,14 @@ void ansi_c_scanner_init()
 
                 /* CProver specific pragmas: hint to disable named checks */
 <CPROVER_PRAGMA>{ws}"check"{ws}"push" {
-                  PARSER.pragma_cprover.push_back(irep_idt{});
+                  PARSER.pragma_cprover.push_back({});
                 }
 <CPROVER_PRAGMA>{ws}"check"{ws}"pop" {
                   if(!PARSER.pragma_cprover.empty())
+                  {
                     PARSER.pragma_cprover.pop_back();
+                    PARSER.set_pragma_cprover();
+                  }
                 }
 <CPROVER_PRAGMA>{ws}"check"{ws}"disable"{ws}{named_check} {
                   std::string tmp(yytext);
@@ -416,16 +419,10 @@ void ansi_c_scanner_init()
                     std::string(tmp, p, tmp.size() - p - 1) +
                     std::string("-check");
                   if(PARSER.pragma_cprover.empty())
-                    PARSER.pragma_cprover.push_back(value);
+                    PARSER.pragma_cprover.push_back({value});
                   else
-                  {
-                    if(!PARSER.pragma_cprover.back().empty())
-                    {
-                      value =
-                        id2string(PARSER.pragma_cprover.back()) + "," + value;
-                    }
-                    PARSER.pragma_cprover.back() = value;
-                  }
+                    PARSER.pragma_cprover.back().insert(value);
+                  PARSER.set_pragma_cprover();
                 }
 
 <CPROVER_PRAGMA>. {

src/util/irep_ids.def

@@ -724,6 +724,7 @@ IREP_ID_ONE(clear_may)
 IREP_ID_ONE(get_must)
 IREP_ID_ONE(set_must)
 IREP_ID_ONE(clear_must)
+IREP_ID_ONE(pragma)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/source_location.h

@@ -192,6 +192,16 @@ class source_locationt:public irept
 
   optionalt<std::string> full_path() const;
 
+  void add_pragma(const irep_idt &pragma)
+  {
+    add(ID_pragma).add(pragma);
+  }
+
+  const irept::named_subt &get_pragmas() const
+  {
+    return find(ID_pragma).get_named_sub();
+  }
+
 protected:
   std::string as_string(bool print_cwd) const;
 };