Merge pull request #7999 from NlightNFotis/cleanup_string_constantt

kroening · web-flow · commit ab2a26c9200a · 2023-12-15T19:09:17.000Z
Refactor `string_constantt::get_value` and `string_constantt::set_value` call sites.
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
@@ -184,7 +184,7 @@ unsigned custom_bitvector_analysist::get_bit_nr(
   else if(string_expr.id()==ID_index)
     return get_bit_nr(to_index_expr(string_expr).array());
   else if(string_expr.id()==ID_string_constant)
-    return bits.number(to_string_constant(string_expr).get_value());
+    return bits.number(to_string_constant(string_expr).value());
   else
     return bits.number("(unknown)");
 }
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
@@ -44,14 +44,14 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       !type_with_subtypes.subtypes().empty() &&
       type_with_subtypes.subtypes()[0].id() == ID_string_constant)
       c_storage_spec.asm_label =
-        to_string_constant(type_with_subtypes.subtypes()[0]).get_value();
+        to_string_constant(type_with_subtypes.subtypes()[0]).value();
   }
   else if(
     type.id() == ID_section && type.has_subtype() &&
     to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
     c_storage_spec.section =
-      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
+      to_string_constant(to_type_with_subtype(type).subtype()).value();
   }
   else if(type.id()==ID_const)
     c_qualifiers.is_constant=true;
@@ -227,7 +227,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
     c_storage_spec.alias =
-      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
+      to_string_constant(to_type_with_subtype(type).subtype()).value();
   }
   else if(type.id()==ID_frontend_pointer)
   {
diff --git a/src/ansi-c/c_storage_spec.cpp b/src/ansi-c/c_storage_spec.cpp
@@ -52,21 +52,19 @@ void c_storage_spect::read(const typet &type)
     type.id() == ID_alias && type.has_subtype() &&
     to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
-    alias =
-      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
+    alias = to_string_constant(to_type_with_subtype(type).subtype()).value();
   }
   else if(
     type.id() == ID_asm && !to_type_with_subtypes(type).subtypes().empty() &&
     to_type_with_subtypes(type).subtypes()[0].id() == ID_string_constant)
   {
     asm_label =
-      to_string_constant(to_type_with_subtypes(type).subtypes()[0]).get_value();
+      to_string_constant(to_type_with_subtypes(type).subtypes()[0]).value();
   }
   else if(
     type.id() == ID_section && type.has_subtype() &&
     to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
-    section =
-      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
+    section = to_string_constant(to_type_with_subtype(type).subtype()).value();
   }
 }
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -119,7 +119,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
       error().source_location = code.find_source_location();
       error() << "static assertion failed";
       if(code.op1().id() == ID_string_constant)
-        error() << ": " << to_string_constant(code.op1()).get_value();
+        error() << ": " << to_string_constant(code.op1()).value();
       error() << eom;
       throw 0;
     }
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -3960,8 +3960,7 @@ std::string expr2ct::convert_with_precedence(
   }
 
   else if(src.id()==ID_string_constant)
-    return '"' + MetaString(id2string(to_string_constant(src).get_value())) +
-           '"';
+    return '"' + MetaString(id2string(to_string_constant(src).value())) + '"';
 
   else if(src.id()==ID_struct)
     return convert_struct(src, precedence);
diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
@@ -225,7 +225,7 @@ void remove_asmt::process_instruction_gcc(
   const code_asm_gcct &code,
   goto_programt &dest)
 {
-  const irep_idt &i_str = to_string_constant(code.asm_text()).get_value();
+  const irep_idt &i_str = to_string_constant(code.asm_text()).value();
 
   std::istringstream str(id2string(i_str));
   assembler_parser.clear();
@@ -396,7 +396,7 @@ void remove_asmt::process_instruction_msc(
   const code_asmt &code,
   goto_programt &dest)
 {
-  const irep_idt &i_str = to_string_constant(code.op0()).get_value();
+  const irep_idt &i_str = to_string_constant(code.op0()).value();
 
   std::istringstream str(id2string(i_str));
   assembler_parser.clear();
diff --git a/src/cpp/cpp_typecheck_static_assert.cpp b/src/cpp/cpp_typecheck_static_assert.cpp
@@ -27,8 +27,7 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert)
     error().source_location=cpp_static_assert.source_location();
     error() << "static assertion failed";
     if(cpp_static_assert.op1().id()==ID_string_constant)
-      error() << ": "
-              << to_string_constant(cpp_static_assert.op1()).get_value();
+      error() << ": " << to_string_constant(cpp_static_assert.op1()).value();
     error() << eom;
     throw 0;
   }
diff --git a/src/cprover/axioms.cpp b/src/cprover/axioms.cpp
@@ -266,7 +266,7 @@ void axiomst::object_size()
         auto pointers_equal = same_object(a_it->address(), *b_it);
         auto size_equal = equal_exprt(
           *a_it,
-          from_integer(string_constant.get_value().size() + 1, a_it->type()));
+          from_integer(string_constant.value().size() + 1, a_it->type()));
         auto implication = implies_exprt(pointers_equal, size_equal);
         if(verbose)
           std::cout << "OBJECT_SIZE2: " << format(implication) << '\n';
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -1801,7 +1801,7 @@ bool goto_convertt::get_string_constant(
 
     if(index_op.id()==ID_string_constant)
     {
-      value = to_string_constant(index_op).get_value();
+      value = to_string_constant(index_op).value();
       return false;
     }
     else if(index_op.id()==ID_array)
@@ -1826,7 +1826,7 @@ bool goto_convertt::get_string_constant(
 
   if(expr.id()==ID_string_constant)
   {
-    value = to_string_constant(expr).get_value();
+    value = to_string_constant(expr).value();
     return false;
   }
 
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
@@ -803,7 +803,7 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
   if(object.id()==ID_string_constant)
   {
     const std::string &str_value =
-      id2string(to_string_constant(object).get_value());
+      id2string(to_string_constant(object).value());
     // make sure we handle the case of a string constant with string-terminating
     // \0 in it
     const std::size_t str_len =
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
@@ -378,7 +378,7 @@ void string_instrumentationt::do_format_string_read(
     format_token_listt token_list = parse_format_string(id2string(
       to_string_constant(
         to_index_expr(to_address_of_expr(format_arg).object()).array())
-        .get_value()));
+        .value()));
 
     std::size_t args=0;
 
@@ -472,7 +472,7 @@ void string_instrumentationt::do_format_string_write(
     format_token_listt token_list = parse_format_string(id2string(
       to_string_constant(
         to_index_expr(to_address_of_expr(format_arg).object()).array())
-        .get_value()));
+        .value()));
 
     std::size_t args=0;
 
diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp
@@ -394,7 +394,7 @@ void shadow_memoryt::symex_field_static_init_string_constant(
 
   const typet &type = index_expr.array().type();
   log.debug() << "Shadow memory: global memory "
-              << id2string(to_string_constant(index_expr.array()).get_value())
+              << id2string(to_string_constant(index_expr.array()).value())
               << " of type " << from_type(ns, "", type) << messaget::eom;
 
   initialize_shadow_memory(
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
@@ -320,12 +320,12 @@ static irep_idt get_string_argument_rec(const exprt &src)
         index_expr.index().is_zero())
       {
         const exprt &fmt_str = index_expr.array();
-        return to_string_constant(fmt_str).get_value();
+        return to_string_constant(fmt_str).value();
       }
     }
     else if(object.id() == ID_string_constant)
     {
-      return to_string_constant(object).get_value();
+      return to_string_constant(object).value();
     }
   }
 
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
@@ -178,7 +178,7 @@ proc_ident_expr: proc_ident
                | TOK_STRING
                {
                  symbol_exprt s = symbol_exprt::typeless(
-                   to_string_constant(parser_stack($$)).get_value());
+                   to_string_constant(parser_stack($$)).value());
                  parser_stack($$).swap(s);
                }
                ;
@@ -429,7 +429,7 @@ literal: TOK_IDENTIFIER
        | TOK_STRING
        {
          constant_exprt c(to_string_constant(parser_stack($$))
-           .get_value(), string_typet());
+           .value(), string_typet());
          parser_stack($$).swap(c);
        }
        | TOK_BUILTIN_LOC
diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp
@@ -365,7 +365,7 @@ string_constraint_generatort::add_axioms_for_char_literal(
   {
     const string_constantt &s = to_string_constant(
       to_binary_expr(to_unary_expr(to_unary_expr(arg).op()).op()).op0());
-    const std::string &sval = id2string(s.get_value());
+    const std::string &sval = id2string(s.value());
     CHECK_RETURN(sval.size() == 1);
     return {from_integer(unsigned(sval[0]), arg.type()), {}};
   }
diff --git a/src/statement-list/statement_list_parser.cpp b/src/statement-list/statement_list_parser.cpp
@@ -62,7 +62,7 @@ static std::string find_version(const exprt &root)
     if(op.get(ID_statement_list_type) == ID_statement_list_version)
     {
       const string_constantt &constant{to_string_constant(op)};
-      return id2string(constant.get_value());
+      return id2string(constant.value());
     }
   }
   UNREACHABLE; // Root expression should always have a version
@@ -274,10 +274,10 @@ static void find_instructions(
         code_token.add_to_operands(*op_it);
     }
 
-    if(label.get_value() == ID_nil)
+    if(label.value() == ID_nil)
       instruction.add_token(code_token);
     else
-      instruction.add_token(code_labelt{label.get_value(), code_token});
+      instruction.add_token(code_labelt{label.value(), code_token});
 
     network.add_instruction(instruction);
   }
diff --git a/src/util/format_constant.cpp b/src/util/format_constant.cpp
@@ -40,7 +40,7 @@ std::string format_constantt::operator()(const exprt &expr)
     }
   }
   else if(expr.id()==ID_string_constant)
-    return id2string(to_string_constant(expr).get_value());
+    return id2string(to_string_constant(expr).value());
 
   return "(format-constant failed: "+expr.id_string()+")";
 }
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
@@ -128,7 +128,7 @@ simplify_exprt::simplify_index(const index_exprt &expr)
   {
     const auto i = numeric_cast<mp_integer>(index);
 
-    const std::string &value = id2string(to_string_constant(array).get_value());
+    const std::string &value = id2string(to_string_constant(array).value());
 
     if(!i.has_value())
     {
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
@@ -689,7 +689,7 @@ simplify_exprt::simplify_object_size(const object_size_exprt &expr)
     {
       typet type=expr.type();
       return from_integer(
-        to_string_constant(op_object).get_value().size() + 1, type);
+        to_string_constant(op_object).value().size() + 1, type);
     }
   }
 

Original file line number	Diff line number	Diff line change
`@@ -184,7 +184,7 @@ unsigned custom_bitvector_analysist::get_bit_nr(`
`184`	`184`	`else if(string_expr.id()==ID_index)`
`185`	`185`	`return get_bit_nr(to_index_expr(string_expr).array());`
`186`	`186`	`else if(string_expr.id()==ID_string_constant)`
`187`		`- return bits.number(to_string_constant(string_expr).get_value());`
	`187`	`+ return bits.number(to_string_constant(string_expr).value());`
`188`	`188`	`else`
`189`	`189`	`return bits.number("(unknown)");`
`190`	`190`	`}`
Original file line number	Diff line number	Diff line change
`@@ -44,14 +44,14 @@ void ansi_c_convert_typet::read_rec(const typet &type)`
`44`	`44`	`!type_with_subtypes.subtypes().empty() &&`
`45`	`45`	`type_with_subtypes.subtypes()[0].id() == ID_string_constant)`
`46`	`46`	`c_storage_spec.asm_label =`
`47`		`- to_string_constant(type_with_subtypes.subtypes()[0]).get_value();`
	`47`	`+ to_string_constant(type_with_subtypes.subtypes()[0]).value();`
`48`	`48`	`}`
`49`	`49`	`else if(`
`50`	`50`	`type.id() == ID_section && type.has_subtype() &&`
`51`	`51`	`to_type_with_subtype(type).subtype().id() == ID_string_constant)`
`52`	`52`	`{`
`53`	`53`	`c_storage_spec.section =`
`54`		`- to_string_constant(to_type_with_subtype(type).subtype()).get_value();`
	`54`	`+ to_string_constant(to_type_with_subtype(type).subtype()).value();`
`55`	`55`	`}`
`56`	`56`	`else if(type.id()==ID_const)`
`57`	`57`	`c_qualifiers.is_constant=true;`
`@@ -227,7 +227,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)`
`227`	`227`	`to_type_with_subtype(type).subtype().id() == ID_string_constant)`
`228`	`228`	`{`
`229`	`229`	`c_storage_spec.alias =`
`230`		`- to_string_constant(to_type_with_subtype(type).subtype()).get_value();`
	`230`	`+ to_string_constant(to_type_with_subtype(type).subtype()).value();`
`231`	`231`	`}`
`232`	`232`	`else if(type.id()==ID_frontend_pointer)`
`233`	`233`	`{`
Original file line number	Diff line number	Diff line change
`@@ -52,21 +52,19 @@ void c_storage_spect::read(const typet &type)`
`52`	`52`	`type.id() == ID_alias && type.has_subtype() &&`
`53`	`53`	`to_type_with_subtype(type).subtype().id() == ID_string_constant)`
`54`	`54`	`{`
`55`		`- alias =`
`56`		`- to_string_constant(to_type_with_subtype(type).subtype()).get_value();`
	`55`	`+ alias = to_string_constant(to_type_with_subtype(type).subtype()).value();`
`57`	`56`	`}`
`58`	`57`	`else if(`
`59`	`58`	`type.id() == ID_asm && !to_type_with_subtypes(type).subtypes().empty() &&`
`60`	`59`	`to_type_with_subtypes(type).subtypes()[0].id() == ID_string_constant)`
`61`	`60`	`{`
`62`	`61`	`asm_label =`
`63`		`- to_string_constant(to_type_with_subtypes(type).subtypes()[0]).get_value();`
	`62`	`+ to_string_constant(to_type_with_subtypes(type).subtypes()[0]).value();`
`64`	`63`	`}`
`65`	`64`	`else if(`
`66`	`65`	`type.id() == ID_section && type.has_subtype() &&`
`67`	`66`	`to_type_with_subtype(type).subtype().id() == ID_string_constant)`
`68`	`67`	`{`
`69`		`- section =`
`70`		`- to_string_constant(to_type_with_subtype(type).subtype()).get_value();`
	`68`	`+ section = to_string_constant(to_type_with_subtype(type).subtype()).value();`
`71`	`69`	`}`
`72`	`70`	`}`
Original file line number	Diff line number	Diff line change
`@@ -119,7 +119,7 @@ void c_typecheck_baset::typecheck_code(codet &code)`
`119`	`119`	`error().source_location = code.find_source_location();`
`120`	`120`	`error() << "static assertion failed";`
`121`	`121`	`if(code.op1().id() == ID_string_constant)`
`122`		`- error() << ": " << to_string_constant(code.op1()).get_value();`
	`122`	`+ error() << ": " << to_string_constant(code.op1()).value();`
`123`	`123`	`error() << eom;`
`124`	`124`	`throw 0;`
`125`	`125`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3960,8 +3960,7 @@ std::string expr2ct::convert_with_precedence(`
`3960`	`3960`	`}`
`3961`	`3961`
`3962`	`3962`	`else if(src.id()==ID_string_constant)`
`3963`		`- return '"' + MetaString(id2string(to_string_constant(src).get_value())) +`
`3964`		`- '"';`
	`3963`	`+ return '"' + MetaString(id2string(to_string_constant(src).value())) + '"';`
`3965`	`3964`
`3966`	`3965`	`else if(src.id()==ID_struct)`
`3967`	`3966`	`return convert_struct(src, precedence);`
Original file line number	Diff line number	Diff line change
`@@ -1801,7 +1801,7 @@ bool goto_convertt::get_string_constant(`
`1801`	`1801`
`1802`	`1802`	`if(index_op.id()==ID_string_constant)`
`1803`	`1803`	`{`
`1804`		`- value = to_string_constant(index_op).get_value();`
	`1804`	`+ value = to_string_constant(index_op).value();`
`1805`	`1805`	`return false;`
`1806`	`1806`	`}`
`1807`	`1807`	`else if(index_op.id()==ID_array)`
`@@ -1826,7 +1826,7 @@ bool goto_convertt::get_string_constant(`
`1826`	`1826`
`1827`	`1827`	`if(expr.id()==ID_string_constant)`
`1828`	`1828`	`{`
`1829`		`- value = to_string_constant(expr).get_value();`
	`1829`	`+ value = to_string_constant(expr).value();`
`1830`	`1830`	`return false;`
`1831`	`1831`	`}`
`1832`	`1832`
Original file line number	Diff line number	Diff line change
`@@ -803,7 +803,7 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)`
`803`	`803`	`if(object.id()==ID_string_constant)`
`804`	`804`	`{`
`805`	`805`	`const std::string &str_value =`
`806`		`- id2string(to_string_constant(object).get_value());`
	`806`	`+ id2string(to_string_constant(object).value());`
`807`	`807`	`// make sure we handle the case of a string constant with string-terminating`
`808`	`808`	`// \0 in it`
`809`	`809`	`const std::size_t str_len =`