Go to the documentation of this file.
33 catch(
const char *err)
40 catch(
const std::string &err)
47 if(type.
id()==ID_cpp_name)
59 if(symbol_expr.
id()!=ID_type)
62 error() <<
"error: expected type" <<
eom;
66 type=symbol_expr.
type();
72 qualifiers.
write(type);
74 else if(type.
id()==ID_struct ||
79 else if(type.
id()==ID_pointer)
93 typet &class_object =
static_cast<typet &
>(type.
add(ID_to_member));
95 if(class_object.
id()==ID_cpp_name)
97 assert(class_object.
get_sub().back().id()==
"::");
98 class_object.
get_sub().pop_back();
109 if(parameters.empty() || !parameters.front().get_this())
115 parameters.insert(parameters.begin(), a0);
123 qualifiers.
write(type);
125 else if(type.
id()==ID_array)
137 if(
to_array_type(type).element_type().get_bool(ID_C_constant))
138 type.
set(ID_C_constant,
true);
140 if(
to_array_type(type).element_type().get_bool(ID_C_volatile))
141 type.
set(ID_C_volatile,
true);
143 else if(type.
id()==ID_vector)
147 else if(type.
id() == ID_frontend_vector)
151 else if(type.
id()==ID_code)
158 for(
auto ¶m : parameters)
163 if(param.has_default_value())
170 else if(type.
id()==ID_template)
174 else if(type.
id()==ID_c_enum)
178 else if(type.
id()==ID_c_enum_tag)
181 else if(type.
id()==ID_c_bit_field)
186 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
187 type.
id() == ID_bool || type.
id() == ID_c_bool || type.
id() == ID_floatbv ||
188 type.
id() == ID_fixedbv || type.
id() == ID_empty)
191 else if(type.
id() == ID_struct_tag)
194 else if(type.
id() == ID_union_tag)
197 else if(type.
id()==ID_constructor ||
198 type.
id()==ID_destructor)
201 else if(type.
id()==
"cpp-cast-operator")
204 else if(type.
id()==
"cpp-template-type")
207 else if(type.
id()==ID_typeof)
214 static_cast<const typet &
>(type.
find(ID_type_arg));
216 if(tmp_type.
id()==ID_cpp_name)
228 type=symbol_expr.
type();
242 else if(type.
id()==ID_decltype)
247 if(e.
type().
id() == ID_c_bit_field)
252 else if(type.
id()==ID_unassigned)
256 else if(type.
id()==ID_template_class_instance)
260 else if(type.
id()==ID_block_pointer)
265 type.
id(ID_frontend_pointer);
268 else if(type.
id()==ID_nullptr)
271 else if(type.
id()==ID_already_typechecked)
275 else if(type.
id() == ID_gcc_attribute_mode)
282 type.
swap(as_parsed);
286 else if(type.
id() == ID_complex)
virtual void typecheck_vector_type(typet &type)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
The type of an expression, extends irept.
std::vector< parametert > parameterst
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const type_with_subtypet & to_type_with_subtype(const typet &type)
Base class for all expressions.
virtual void typecheck_type(typet &type)
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
const exprt & size() const
typet & type()
Return the type of the expression.
void typecheck_type(typet &) override
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
source_locationt source_location
void set(const irep_idt &name, const irep_idt &value)
#define PRECONDITION(CONDITION)
const source_locationt & source_location() const
virtual void write(typet &src) const override
bool simplify(exprt &expr, const namespacet &ns)
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
pointer_typet pointer_type(const typet &subtype)
const irep_idt & id() const
const parameterst & parameters() const
void typecheck_compound_type(struct_union_typet &) override
void set_base_name(const irep_idt &name)
const typet & underlying_type() const
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
void typecheck_expr(exprt &) override
message_handlert & get_message_handler()
irept & add(const irep_idt &name)
void implicit_typecast(exprt &expr, const typet &type) override
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
holds a combination of types
void typecheck_enum_type(typet &type)
const typet & return_type() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
template_typet & to_template_type(typet &type)
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
bool get_bool(const irep_idt &name) const
cpp_namet & to_cpp_name(irept &cpp_name)