Go to the documentation of this file.
39 str=utf8_to_utf16_little_endian(c_str);
44 for(std::size_t i=0; i<str.size(); i++)
69 constraints.existential.push_back(
88 if(
const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
90 const and_exprt guard_true(guard, if_expr->cond());
94 fresh_symbol, res, if_expr->true_case(), guard_true),
96 fresh_symbol, res, if_expr->false_case(), guard_false));
98 else if(
const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
std::pair< exprt, string_constraintst > add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
const typet & subtype() const
The type of an expression, extends irept.
Correspondance between arrays and pointers string representations.
Base class for all expressions.
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Collection of constraints of different types: existential formulas, universal formulas,...
bitvector_typet index_type()
exprt::operandst argumentst
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
std::pair< exprt, string_constraintst > add_axioms_for_cprover_string(symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
typet & type()
Return the type of the expression.
Generation of fresh symbols of a given type.
const std::string & id2string(const irep_idt &d)
Application of (mathematical) function.
std::wstring widen(const char *s)
signedbv_typet get_return_code_type()
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard)
Add axioms ensuring that the provided string expression and constant are equal.
bitvector_typet char_type()
std::pair< exprt, string_constraintst > add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
String corresponding to an internal cprover string.
The Boolean constant true.
std::vector< exprt > existential