28 components().emplace_back(
"length", index_type);
29 components().emplace_back(
"content", char_array);
37 type.
id()==ID_struct &&
45 if(type.
id()==ID_pointer)
58 if(type.
id()==ID_symbol)
61 return tag==
"java::java.lang.String";
63 else if(type.
id()==ID_struct)
66 return tag==
"java.lang.String";
75 if(type.
id()==ID_pointer)
79 if(subtype.
id()==ID_struct)
82 return tag==
"java.lang.StringBuilder";
92 if(type.
id()==ID_pointer)
96 if(subtype.
id()==ID_struct)
99 return tag==
"java.lang.CharSequence";
The type of an expression.
static bool is_java_string_pointer_type(const typet &type)
static bool is_java_string_builder_type(const typet &type)
Type for string expressions used by the string solver.
static bool is_java_char_sequence_type(const typet &type)
static bool is_c_string_type(const typet &type)
const componentst & components() const
const irep_idt & id() const
static bool is_java_string_type(const typet &type)
An expression denoting infinity.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
const typet & subtype() const
refined_string_typet(const typet &index_type, const typet &char_type)
bitvector_typet char_type()
const irep_idt & get_identifier() const