cprover
refined_string_type.h File Reference

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>
Include dependency graph for refined_string_type.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  refined_string_typet
 

Functions

const refined_string_typetto_refined_string_type (const typet &type)
 

Detailed Description

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.

Function Documentation

§ to_refined_string_type()

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().