From 4d4f9e7d182643f8474b69a9d8493a32650cc304 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 19 Feb 2022 12:54:55 +0000
Subject: [PATCH] Remove ID_C_bounds_check special-case in goto_check_ct

The C front-end can safely use the pragma-based approach that is more
general.
---
 src/analyses/goto_check_c.cpp            |  7 -------
 src/ansi-c/ansi_c_entry_point.cpp        | 14 +++++++-------
 src/goto-programs/string_abstraction.cpp |  3 ---
 3 files changed, 7 insertions(+), 17 deletions(-)

diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp
index e3ab5331d2f..e6cd9e9c5ee 100644
--- a/src/analyses/goto_check_c.cpp
+++ b/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(
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index fb1e74f0d49..6c10396e08e 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/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());
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 4200839d9a6..508f4572471 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/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);
     }