Cleaning the initialization of string expressions from constants

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -13,29 +13,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 /*******************************************************************\
 
-Function: string_constraint_generatort::extract_java_string
-
-  Inputs: a symbol expression representing a java literal
-
- Outputs: a string constant
-
- Purpose: extract java string from symbol expression when they are encoded
-          inside the symbol name
-
-\*******************************************************************/
-
-irep_idt string_constraint_generatort::extract_java_string(
-  const symbol_exprt &s)
-{
-  std::string tmp=id2string(s.get_identifier());
-  std::string prefix("java::java.lang.String.Literal.");
-  assert(has_prefix(tmp, prefix));
-  std::string value=tmp.substr(prefix.length());
-  return irep_idt(value);
-}
-
-/*******************************************************************\
-
 Function: string_constraint_generatort::add_axioms_for_constant
 
   Inputs: a string constant
@@ -107,7 +84,9 @@ string_exprt string_constraint_generatort::add_axioms_for_empty_string(
 
 Function: string_constraint_generatort::add_axioms_from_literal
 
-  Inputs: function application with an argument which is a string literal
+  Inputs:
+    f - function application with an argument which is a string literal
+        that is a constant with a string value.
 
  Outputs: string expression
 
@@ -123,28 +102,7 @@ string_exprt string_constraint_generatort::add_axioms_from_literal(
   assert(args.size()==1); // Bad args to string literal?
 
   const exprt &arg=args[0];
-  irep_idt sval;
-
-  assert(arg.operands().size()==1);
-  if(arg.op0().operands().size()==2 &&
-     arg.op0().op0().id()==ID_string_constant)
-  {
-    // C string constant
-    const exprt &s=arg.op0().op0();
-    sval=to_string_constant(s).get_value();
-  }
-  else
-  {
-    // Java string constant
-    assert(false); // TODO: Check if used. On the contrary, discard else.
-    assert(arg.id()==ID_symbol);
-    const exprt &s=arg.op0();
-
-    // It seems the value of the string is lost,
-    // we need to recover it from the identifier
-    sval=extract_java_string(to_symbol_expr(s));
-  }
-
+  irep_idt sval=to_constant_expr(arg).get_value();
   const refined_string_typet &ref_type=to_refined_string_type(f.type());
   return add_axioms_for_constant(sval, ref_type);
 }