add_axioms_for_char_at(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_char_literal(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_char_set(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_characters_in_integer_string(const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul) | string_constraint_generatort | private |
add_axioms_for_code_point(const array_string_exprt &res, const exprt &code_point) | string_constraint_generatort | private |
add_axioms_for_code_point_at(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_code_point_before(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_code_point_count(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_compare_to(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) | string_constraint_generatort | |
add_axioms_for_concat(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, const exprt &c) | string_constraint_generatort | |
add_axioms_for_concat_char(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_code_point(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index) | string_constraint_generatort | |
add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt()) | string_constraint_generatort | private |
add_axioms_for_constrain_characters(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_contains(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_copy(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_correct_number_format(const exprt &input_int, const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting) | string_constraint_generatort | private |
add_axioms_for_cprover_string(const array_string_exprt &res, const exprt &arg, const exprt &guard) | string_constraint_generatort | private |
add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) | string_constraint_generatort | private |
add_axioms_for_delete(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_delete_char_at(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_empty_string(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_equals(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_equals_ignore_case(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_format(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_format(const array_string_exprt &res, const std::string &s, const exprt::operandst &args) | string_constraint_generatort | private |
add_axioms_for_format_specifier(const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type) | string_constraint_generatort | private |
add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &i, size_t max_size) | string_constraint_generatort | private |
add_axioms_for_function_application(const function_application_exprt &expr) | string_constraint_generatort | |
add_axioms_for_hash_code(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_index_of(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset) | string_constraint_generatort | |
add_axioms_for_insert(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_bool(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_char(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_double(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_float(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_int(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_intern(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_is_empty(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset) | string_constraint_generatort | private |
add_axioms_for_is_prefix(const function_application_exprt &f, bool swap_arguments=false) | string_constraint_generatort | private |
add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false) | string_constraint_generatort | private |
add_axioms_for_last_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_last_index_of(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_last_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_length(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_offset_by_code_point(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_parse_int(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_replace(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_set_length(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_string_of_float(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_string_of_float(const array_string_exprt &res, const exprt &f) | string_constraint_generatort | private |
add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) | string_constraint_generatort | private |
add_axioms_for_substring(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_to_lower_case(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_to_upper_case(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_trim(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_bool(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_bool(const array_string_exprt &res, const exprt &i) | string_constraint_generatort | private |
add_axioms_from_char(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_char(const array_string_exprt &res, const exprt &i) | string_constraint_generatort | private |
add_axioms_from_double(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f) | string_constraint_generatort | private |
add_axioms_from_float_scientific_notation(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_int(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_int(const array_string_exprt &res, const exprt &input_int, size_t max_size=0) | string_constraint_generatort | private |
add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i) | string_constraint_generatort | private |
add_axioms_from_int_hex(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0) | string_constraint_generatort | private |
add_axioms_from_literal(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_long(const function_application_exprt &f) | string_constraint_generatort | private |
add_constraint_on_characters(const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set) | string_constraint_generatort | private |
add_lemma(const exprt &) | string_constraint_generatort | |
array_pool | string_constraint_generatort | |
associate_array_to_pointer(const function_application_exprt &f) | string_constraint_generatort | private |
associate_length_to_array(const function_application_exprt &f) | string_constraint_generatort | private |
axiom_for_is_positive_index(const exprt &x) | string_constraint_generatort | private |
boolean_symbols | string_constraint_generatort | private |
char_array_of_pointer(const exprt &pointer, const exprt &length) | string_constraint_generatort | private |
character_equals_ignore_case(exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z) | string_constraint_generatort | privatestatic |
clear_constraints() | string_constraint_generatort | |
constant_char(int i, const typet &char_type) | string_constraint_generatort | privatestatic |
constraints | string_constraint_generatort | private |
created_strings | string_constraint_generatort | private |
fresh_boolean(const irep_idt &prefix) | string_constraint_generatort | private |
fresh_exist_index(const irep_idt &prefix, const typet &type) | string_constraint_generatort | |
fresh_string(const typet &index_type, const typet &char_type) | string_constraint_generatort | private |
fresh_symbol | string_constraint_generatort | |
fresh_univ_index(const irep_idt &prefix, const typet &type) | string_constraint_generatort | |
get_boolean_symbols() const | string_constraint_generatort | |
get_constraints() const | string_constraint_generatort | |
get_created_strings() const | string_constraint_generatort | |
get_index_symbols() const | string_constraint_generatort | |
get_lemmas() const | string_constraint_generatort | |
get_not_contains_constraints() const | string_constraint_generatort | |
get_return_code_type() | string_constraint_generatort | inline |
get_string_expr(const exprt &expr) | string_constraint_generatort | private |
get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const | string_constraint_generatort | inline |
hash_code_of_string | string_constraint_generatort | private |
index_symbols | string_constraint_generatort | private |
int_of_hex_char(const exprt &chr) | string_constraint_generatort | privatestatic |
intern_of_string | string_constraint_generatort | private |
is_high_surrogate(const exprt &chr) | string_constraint_generatort | privatestatic |
is_low_surrogate(const exprt &chr) | string_constraint_generatort | privatestatic |
lemmas | string_constraint_generatort | private |
make_array_pointer_association(const function_application_exprt &expr) | string_constraint_generatort | |
message | string_constraint_generatort | private |
not_contains_constraints | string_constraint_generatort | private |
ns | string_constraint_generatort | private |
string_constraint_generatort(const namespacet &ns) | string_constraint_generatort | explicit |
to_integer_or_default(const exprt &expr, unsigned long def) | string_constraint_generatort | private |
witness | string_constraint_generatort | |