Replace "bounds_check" by ID_C_bounds_check

Replaces the hard-coded string by a dstringt to avoid typos, and also
changes it to a comment: the annotation (communicating from the
front-end to goto_checkt) does not change the semantics of the
expression that has been annotated.

Author: tautschnig

src/analyses/goto_check.cpp

@@ -1317,9 +1317,12 @@ void goto_checkt::bounds_check(
   if(!enable_bounds_check)
     return;
 
-  if(expr.find("bounds_check").is_not_nil() &&
-     !expr.get_bool("bounds_check"))
+  if(
+    expr.find(ID_C_bounds_check).is_not_nil() &&
+    !expr.get_bool(ID_C_bounds_check))
+  {
     return;
+  }
 
   typet array_type = expr.array().type();
 

src/ansi-c/ansi_c_entry_point.cpp

@@ -407,7 +407,7 @@ bool generate_ansi_c_start_function(
           argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
 
         // disable bounds check on that one
-        index_expr.set("bounds_check", false);
+        index_expr.set(ID_C_bounds_check, false);
 
         init_code.add(code_assignt(index_expr, null));
       }
@@ -423,7 +423,7 @@ 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("bounds_check", false);
+        index_expr.set(ID_C_bounds_check, false);
 
         equal_exprt is_null(std::move(index_expr), std::move(null));
 
@@ -449,7 +449,7 @@ bool generate_ansi_c_start_function(
             argv_symbol.symbol_expr(), from_integer(0, index_type()));
 
           // disable bounds check on that one
-          index_expr.set("bounds_check", false);
+          index_expr.set(ID_C_bounds_check, false);
 
           const pointer_typet &pointer_type =
             to_pointer_type(parameters[1].type());

src/goto-programs/string_abstraction.cpp

@@ -567,7 +567,7 @@ void string_abstractiont::abstract_function_call(
 
       index_exprt idx(str_args.back(), from_integer(0, index_type()));
       // disable bounds check on that one
-      idx.set("bounds_check", false);
+      idx.set(ID_C_bounds_check, false);
 
       str_args.back()=address_of_exprt(idx);
     }

src/util/irep_ids.def

@@ -841,6 +841,8 @@ IREP_ID_ONE(statement_list_instructions)
 IREP_ID_ONE(max)
 IREP_ID_ONE(min)
 IREP_ID_ONE(constant_interval)
+IREP_ID_TWO(C_bounds_check, #bounds_check)
+IREP_ID_ONE(count_leading_zeros)
 
 // 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