26 std::string prefix(
"java::java.lang.String.Literal.");
28 std::string value=tmp.substr(prefix.length());
52 for(std::size_t i=0; i<str.size(); i++)
75 axioms.push_back(res.axiom_for_has_length(0));
88 assert(
args.size()==1);
93 assert(arg.operands().size()==1);
94 if(arg.op0().operands().size()==2 &&
95 arg.op0().op0().id()==ID_string_constant)
string_exprt add_axioms_from_literal(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the string literal ...
Generates string constraints to link results from string functions with their arguments.
const std::string & id2string(const irep_idt &d)
application of (mathematical) function
std::wstring widen(const char *s)
const typet & get_char_type() const
const irep_idt & get_identifier() const
equal_exprt axiom_for_has_length(const exprt &rhs) const
string_exprt add_axioms_for_empty_string(const function_application_exprt &f)
add axioms to say that the returned string expression is empty
string_exprt fresh_string(const refined_string_typet &type)
construct a string expression whose length and content are new variables
static bool is_unrefined_string_type(const typet &type)
exprt::operandst argumentst
const refined_string_typet & to_refined_string_type(const typet &type)
std::list< exprt > axioms
const typet & get_index_type() const
bool has_prefix(const std::string &s, const std::string &prefix)
std::wstring utf8_to_utf16_little_endian(const std::string &in)
string_exprt add_axioms_for_constant(irep_idt sval, const refined_string_typet &ref_type)
add axioms saying the returned string expression should be equal to the string constant ...
const string_constantt & to_string_constant(const exprt &expr)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Expression to hold a symbol (variable)
const irep_idt & get_value() const
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
static irep_idt extract_java_string(const symbol_exprt &s)
extract java string from symbol expression when they are encoded inside the symbol name ...