cprover
|
Type for string expressions used by the string solver. More...
#include <util/std_types.h>
#include <util/std_expr.h>
#include <util/arith_tools.h>
#include <util/expr_util.h>
Go to the source code of this file.
Classes | |
class | refined_string_typet |
Functions | |
const refined_string_typet & | to_refined_string_type (const typet &type) |
Type for string expressions used by the string solver.
These string expressions contain a field length
, of type index_type
, a field content
of type content_type
. This module also defines functions to recognise the C and java string types.
Definition in file refined_string_type.h.
const refined_string_typet& to_refined_string_type | ( | const typet & | type | ) |
Definition at line 84 of file refined_string_type.h.
References irept::id().
Referenced by string_constraint_generatort::add_axioms_for_char_at(), string_constraint_generatort::add_axioms_for_char_set(), string_constraint_generatort::add_axioms_for_concat(), string_constraint_generatort::add_axioms_for_concat_bool(), string_constraint_generatort::add_axioms_for_concat_char(), string_constraint_generatort::add_axioms_for_concat_code_point(), string_constraint_generatort::add_axioms_for_concat_int(), string_constraint_generatort::add_axioms_for_concat_long(), string_constraint_generatort::add_axioms_for_copy(), string_constraint_generatort::add_axioms_for_empty_string(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_if(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_insert_bool(), string_constraint_generatort::add_axioms_for_insert_char(), string_constraint_generatort::add_axioms_for_insert_int(), string_constraint_generatort::add_axioms_for_insert_long(), string_constraint_generatort::add_axioms_for_last_index_of(), string_constraint_generatort::add_axioms_for_parse_int(), string_constraint_generatort::add_axioms_for_replace(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_substring(), string_constraint_generatort::add_axioms_for_to_lower_case(), string_constraint_generatort::add_axioms_for_to_upper_case(), string_constraint_generatort::add_axioms_for_trim(), string_constraint_generatort::add_axioms_for_value_of(), string_constraint_generatort::add_axioms_from_bool(), string_constraint_generatort::add_axioms_from_char(), string_constraint_generatort::add_axioms_from_float(), string_constraint_generatort::add_axioms_from_int(), string_constraint_generatort::add_axioms_from_int_hex(), string_constraint_generatort::add_axioms_from_literal(), string_constraint_generatort::add_axioms_from_long(), string_refinementt::dec_solve(), and string_constraint_generatort::find_or_add_string_of_symbol().