Merge pull request #6684 from tautschnig/cleanup/pragma-instead-of-C_bounds_check

Remove ID_C_bounds_check special-case in goto_check_ct

Author: tautschnig

src/analyses/goto_check_c.cpp

@@ -1505,13 +1505,6 @@ void goto_check_ct::bounds_check(const exprt &expr, const guardt &guard)
   if(!enable_bounds_check)
     return;
 
-  if(
-    expr.find(ID_C_bounds_check).is_not_nil() &&
-    !expr.get_bool(ID_C_bounds_check))
-  {
-    return;
-  }
-
   if(expr.id() == ID_index)
     bounds_check_index(to_index_expr(expr), guard);
   else if(

src/ansi-c/ansi_c_entry_point.cpp

@@ -410,10 +410,10 @@ bool generate_ansi_c_start_function(
         index_exprt index_expr(
           argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
 
-        // disable bounds check on that one
-        index_expr.set(ID_C_bounds_check, false);
-
         init_code.add(code_frontend_assignt(index_expr, null));
+        // disable bounds check on that one
+        init_code.statements().back().add_source_location().add_pragma(
+          "disable:bounds-check");
       }
 
       if(parameters.size()==3)
@@ -427,12 +427,13 @@ bool generate_ansi_c_start_function(
 
         index_exprt index_expr(
           envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
-        // disable bounds check on that one
-        index_expr.set(ID_C_bounds_check, false);
 
         equal_exprt is_null(std::move(index_expr), std::move(null));
 
         init_code.add(code_assumet(is_null));
+        // disable bounds check on that one
+        init_code.statements().back().add_source_location().add_pragma(
+          "disable:bounds-check");
       }
 
       {
@@ -452,9 +453,8 @@ bool generate_ansi_c_start_function(
         {
           index_exprt index_expr(
             argv_symbol.symbol_expr(), from_integer(0, c_index_type()));
-
           // disable bounds check on that one
-          index_expr.set(ID_C_bounds_check, false);
+          index_expr.add_source_location().add_pragma("disable:bounds-check");
 
           const pointer_typet &pointer_type =
             to_pointer_type(parameters[1].type());

src/goto-programs/string_abstraction.cpp

@@ -568,9 +568,6 @@ void string_abstractiont::abstract_function_call(
         "argument array type differs from formal parameter pointer type");
 
       index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
-      // disable bounds check on that one
-      idx.set(ID_C_bounds_check, false);
-
       str_args.back()=address_of_exprt(idx);
     }