cprover
|
Type for string expressions used by the string solver. More...
Go to the source code of this file.
Classes | |
class | refined_string_typet |
Functions | |
bool | is_refined_string_type (const typet &type) |
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.
|
inline |
Definition at line 50 of file refined_string_type.h.
References CPROVER_PREFIX, struct_union_typet::get_tag(), irept::id(), and to_struct_type().
Referenced by string_constraint_generatort::add_axioms_for_index_of(), add_dependency_to_string_subexprs(), string_constraint_generatort::get_string_expr(), string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(), and to_refined_string_type().
|
inline |
Definition at line 57 of file refined_string_type.h.
References is_refined_string_type(), and PRECONDITION.