Use irep_idt() instead of ""

Constructing a dstringt from a C string requires a string table lookup, while
the default constructor for a dstringt just zero-initialises an unsigned.

Author: tautschnig

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -298,9 +298,9 @@ void java_object_factoryt::gen_pointer_target_init(
   gen_nondet_init(
     assignments,
     init_expr,
-    false, // is_sub
-    "",    // class_identifier
-    false, // skip_classid
+    false,      // is_sub
+    irep_idt(), // class_identifier
+    false,      // skip_classid
     lifetime,
     {}, // no override type
     depth + 1,
@@ -751,9 +751,9 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   gen_nondet_init(
     assignments,
     new_symbol.symbol_expr(),
-    false, // is_sub
-    "",    // class_identifier
-    false, // skip_classid
+    false,      // is_sub
+    irep_idt(), // class_identifier
+    false,      // skip_classid
     lifetime,
     {}, // no override_type
     depth,
@@ -1555,9 +1555,9 @@ exprt object_factory(
   state.gen_nondet_init(
     assignments,
     object,
-    false, // is_sub
-    "",    // class_identifier
-    false, // skip_classid
+    false,      // is_sub
+    irep_idt(), // class_identifier
+    false,      // skip_classid
     lifetime,
     {}, // no override_type
     1,  // initial depth
@@ -1626,8 +1626,8 @@ void gen_nondet_init(
   state.gen_nondet_init(
     assignments,
     expr,
-    false, // is_sub
-    "",    // class_identifier
+    false,      // is_sub
+    irep_idt(), // class_identifier
     skip_classid,
     lifetime,
     {}, // no override_type

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -41,7 +41,7 @@ static irep_idt get_tag(const typet &type)
   else if(type.id() == ID_struct)
     return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
   else
-    return "";
+    return irep_idt();
 }
 
 /// \param type: a type

src/analyses/ai.h

@@ -157,7 +157,7 @@ class ai_baset
     const goto_functionst::goto_functiont &goto_function,
     std::ostream &out) const
   {
-    output(ns, "", goto_function.body, out);
+    output(ns, irep_idt(), goto_function.body, out);
   }
 
   /// Output the abstract states for the whole program as JSON
@@ -178,15 +178,15 @@ class ai_baset
     const namespacet &ns,
     const goto_programt &goto_program) const
   {
-    return output_json(ns, "", goto_program);
+    return output_json(ns, irep_idt(), goto_program);
   }
 
   /// Output the abstract states for a single function as JSON
   jsont output_json(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function) const
   {
-    return output_json(ns, "", goto_function.body);
+    return output_json(ns, irep_idt(), goto_function.body);
   }
 
   /// Output the abstract states for the whole program as XML
@@ -207,15 +207,15 @@ class ai_baset
     const namespacet &ns,
     const goto_programt &goto_program) const
   {
-    return output_xml(ns, "", goto_program);
+    return output_xml(ns, irep_idt(), goto_program);
   }
 
   /// Output the abstract states for a single function as XML
   xmlt output_xml(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function) const
   {
-    return output_xml(ns, "", goto_function.body);
+    return output_xml(ns, irep_idt(), goto_function.body);
   }
 
 protected:

src/analyses/goto_rw.cpp

@@ -671,7 +671,7 @@ void guarded_range_domaint::output(
     out << itr->first << ":" << itr->second.first;
     // we don't know what mode (language) we are in, so we rely on the default
     // language to be reasonable for from_expr
-    out << " if " << from_expr(ns, "", itr->second.second);
+    out << " if " << from_expr(ns, irep_idt(), itr->second.second);
   }
   out << "]";
 }

src/analyses/invariant_set.cpp

@@ -136,7 +136,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
   // we don't know what mode (language) we are in, so we rely on the default
   // language to be reasonable for from_expr
   if(is_constant_address(expr))
-    return from_expr(ns, "", expr);
+    return from_expr(ns, irep_idt(), expr);
 
   if(expr.id()==ID_member)
   {
@@ -390,8 +390,8 @@ void invariant_sett::strengthen_rec(const exprt &expr)
     throw "non-Boolean argument to strengthen()";
 
   #if 0
-  std::cout << "S: " << from_expr(*ns, "", expr) << '\n';
-  #endif
+  std::cout << "S: " << from_expr(*ns, irep_idt(), expr) << '\n';
+#endif
 
   if(is_false)
   {
@@ -593,8 +593,8 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
     throw "implies: non-Boolean expression";
 
   #if 0
-  std::cout << "I: " << from_expr(*ns, "", expr) << '\n';
-  #endif
+  std::cout << "I: " << from_expr(*ns, irep_idt(), expr) << '\n';
+#endif
 
   if(is_false) // can't get any stronger
     return tvt(true);

src/analyses/local_bitvector_analysis.cpp

@@ -347,7 +347,7 @@ void local_bitvector_analysist::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, "", out, *i_it);
+    goto_function.body.output_instruction(ns, irep_idt(), out, *i_it);
     out << "\n";
 
     l++;

src/analyses/local_may_alias.cpp

@@ -470,7 +470,7 @@ void local_may_aliast::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, "", out, *i_it);
+    goto_function.body.output_instruction(ns, irep_idt(), out, *i_it);
     out << "\n";
 
     l++;

src/analyses/local_safe_pointers.cpp

@@ -207,7 +207,7 @@ void local_safe_pointerst::output(
     }
 
     out << '\n';
-    goto_program.output_instruction(ns, "", out, *i_it);
+    goto_program.output_instruction(ns, irep_idt(), out, *i_it);
     out << '\n';
   }
 }
@@ -258,7 +258,7 @@ void local_safe_pointerst::output_safe_dereferences(
     }
 
     out << '\n';
-    goto_program.output_instruction(ns, "", out, *i_it);
+    goto_program.output_instruction(ns, irep_idt(), out, *i_it);
     out << '\n';
   }
 }

src/analyses/static_analysis.h

@@ -155,7 +155,7 @@ class static_analysis_baset
     const goto_programt &goto_program,
     std::ostream &out) const
   {
-    output(goto_program, "", out);
+    output(goto_program, irep_idt(), out);
   }
 
   virtual bool has_location(locationt l) const=0;

src/ansi-c/c_preprocess.cpp

@@ -200,9 +200,9 @@ static void error_parse_line(
     if(state==2)
     {
       saved_error_location.set_file(file);
-      saved_error_location.set_function("");
+      saved_error_location.set_function(irep_idt());
       saved_error_location.set_line(line_no);
-      saved_error_location.set_column("");
+      saved_error_location.set_column(irep_idt());
     }
   }
 

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -157,7 +157,7 @@ bool acceleration_utilst::check_inductive(
 
 #ifdef DEBUG
   std::cout << "Checking following program for inductiveness:\n";
-  program.output(ns, "", std::cout);
+  program.output(ns, irep_idt(), std::cout);
 #endif
 
   try
@@ -441,7 +441,7 @@ bool acceleration_utilst::do_assumptions(
 
 #ifdef DEBUG
   std::cout << "Checking following program for monotonicity:\n";
-  program.output(ns, "", std::cout);
+  program.output(ns, irep_idt(), std::cout);
 #endif
 
   try

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -403,7 +403,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
 
 #ifdef DEBUG
   std::cout << "Fitting polynomial with program:\n";
-  program.output(ns, "", std::cout);
+  program.output(ns, irep_idt(), std::cout);
 #endif
 
   // Now do an ASSERT(false) to grab a counterexample
@@ -699,7 +699,7 @@ bool polynomial_acceleratort::check_inductive(
 
 #ifdef DEBUG
   std::cout << "Checking following program for inductiveness:\n";
-  program.output(ns, "", std::cout);
+  program.output(ns, irep_idt(), std::cout);
 #endif
 
   try

src/goto-instrument/wmm/cycle_collection.cpp

@@ -89,8 +89,17 @@ void event_grapht::graph_explorert::collect_cycles(
   {
     event_idt source=*st_it;
     egraph.message.debug() << "explore " << egraph[source].id << messaget::eom;
-    backtrack(set_of_cycles, source, source,
-      false, max_po_trans, false, false, false, "", model);
+    backtrack(
+      set_of_cycles,
+      source,
+      source,
+      false,
+      max_po_trans,
+      false,
+      false,
+      false,
+      irep_idt(),
+      model);
 
     while(!marked_stack.empty())
     {
@@ -452,18 +461,17 @@ bool event_grapht::graph_explorert::backtrack(
           f=true;
         }
         else if(!mark[w])
-          f|=
-            backtrack(
-              set_of_cycles,
-              source,
-              w,
-              unsafe_met_updated,
-              po_trans,
-              false,
-              false,
-              false,
-              "",
-              model);
+          f |= backtrack(
+            set_of_cycles,
+            source,
+            w,
+            unsafe_met_updated,
+            po_trans,
+            false,
+            false,
+            false,
+            irep_idt(),
+            model);
       }
     }
 

src/goto-programs/goto_inline_class.cpp

@@ -327,7 +327,7 @@ void goto_inlinet::expand_function_call(
 
 #ifdef DEBUG
   std::cout << "Expanding call:\n";
-  dest.output_instruction(ns, "", std::cout, *target);
+  dest.output_instruction(ns, irep_idt(), std::cout, *target);
 #endif
 
   exprt lhs;

src/goto-programs/goto_program.h

@@ -725,7 +725,7 @@ class goto_programt
   /// Output goto-program to given stream
   std::ostream &output(std::ostream &out) const
   {
-    return output(namespacet(symbol_tablet()), "", out);
+    return output(namespacet(symbol_tablet()), irep_idt(), out);
   }
 
   /// Output a single instruction

src/goto-symex/symex_builtin_functions.cpp

@@ -295,7 +295,7 @@ irep_idt get_string_argument_rec(const exprt &src)
     }
   }
 
-  return "";
+  return irep_idt();
 }
 
 irep_idt get_string_argument(const exprt &src, const namespacet &ns)

src/goto-symex/symex_dereference_state.cpp

@@ -91,15 +91,15 @@ void symex_dereference_statet::get_value_set(
 #endif
 
 #if 0
-  std::cout << "E: " << from_expr(goto_symex.ns, "", expr) << '\n';
+  std::cout << "E: " << from_expr(goto_symex.ns, irep_idt(), expr) << '\n';
 #endif
 
 #if 0
   std::cout << "**************************\n";
   for(value_setst::valuest::const_iterator it=value_set.begin();
       it!=value_set.end();
       it++)
-    std::cout << from_expr(goto_symex.ns, "", *it) << '\n';
+    std::cout << from_expr(goto_symex.ns, irep_idt(), *it) << '\n';
   std::cout << "**************************\n";
 #endif
 }

src/jsil/jsil_language.cpp

@@ -134,7 +134,7 @@ bool jsil_languaget::to_expr(
   // parsing
 
   jsil_parser.clear();
-  jsil_parser.set_file("");
+  jsil_parser.set_file(irep_idt());
   jsil_parser.in=&instream;
   jsil_parser.set_message_handler(get_message_handler());
   jsil_scanner_init();

src/langapi/language_util.cpp

@@ -59,13 +59,13 @@ std::string type_to_name(
 std::string from_expr(const exprt &expr)
 {
   symbol_tablet symbol_table;
-  return from_expr(namespacet(symbol_table), "", expr);
+  return from_expr(namespacet(symbol_table), irep_idt(), expr);
 }
 
 std::string from_type(const typet &type)
 {
   symbol_tablet symbol_table;
-  return from_type(namespacet(symbol_table), "", type);
+  return from_type(namespacet(symbol_table), irep_idt(), type);
 }
 
 exprt to_expr(
@@ -91,5 +91,5 @@ exprt to_expr(
 std::string type_to_name(const typet &type)
 {
   symbol_tablet symbol_table;
-  return type_to_name(namespacet(symbol_table), "", type);
+  return type_to_name(namespacet(symbol_table), irep_idt(), type);
 }

src/linking/linking.cpp

@@ -358,8 +358,8 @@ void linkingt::detailed_conflict_report_rec(
   if(!msg.empty())
   {
     error() << '\n';
-    error() << "reason for conflict at " << expr_to_string("", conflict_path)
-            << ": " << msg << '\n';
+    error() << "reason for conflict at "
+            << expr_to_string(irep_idt(), conflict_path) << ": " << msg << '\n';
 
     error() << '\n';
     error() << type_to_string_verbose(old_symbol, t1) << '\n';

src/util/expr_initializer.cpp

@@ -242,7 +242,7 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
     if(!found)
     {
       // stupid empty union
-      union_exprt value("", nil_exprt(), type);
+      union_exprt value(irep_idt(), nil_exprt(), type);
       value.add_source_location() = source_location;
       return std::move(value);
     }