117 for(
const auto &
id :
id_set)
119 return static_cast<cpp_scopet &
>(id->get_parent());
151 base_name=std::string(
"#anon_")+std::to_string(++
anon_counter);
214 error() <<
"compound tag '" << base_name <<
"' declared previously\n"
215 <<
"location of previous definition: " << symbol.
location
220 else if(symbol.
type.
id() != type.
id())
224 <<
" as different kind of tag" <<
eom;
232 symbol.base_name=base_name;
234 symbol.module=
module;
248 error() <<
"cpp_typecheckt::typecheck_compound_type: "
249 <<
"symbol_table.move() failed" <<
eom;
261 id.class_identifier=new_symbol->
name;
303 declaration.
type().
id()==
"cpp-cast-operator";
329 error() <<
"void-typed member not permitted" <<
eom;
350 error() <<
"declarator in compound needs to be simple name"
355 bool is_method=!is_typedef && final_type.
id()==
ID_code;
358 bool is_virtual=declaration.
member_spec().is_virtual();
359 bool is_explicit=declaration.
member_spec().is_explicit();
360 bool is_inline=declaration.
member_spec().is_inline();
366 if(is_virtual && !is_method)
369 error() <<
"only methods can be virtual" <<
eom;
373 if(is_inline && !is_method)
376 error() <<
"only methods can be inlined" <<
eom;
380 if(is_virtual && is_static)
383 error() <<
"static methods cannot be virtual" <<
eom;
390 error() <<
"cast operators cannot be static" <<
eom;
397 error() <<
"constructors cannot be virtual" <<
eom;
404 error() <<
"only constructors can be explicit" <<
eom;
411 error() <<
"member function must return a value or void" <<
eom;
419 error() <<
"destructor with wrong name" <<
eom;
431 is_method || is_static)
442 identifier=base_name;
464 const typet &method_qualifier=
510 for(
const auto &
comp : components)
519 !
code_type.parameters().empty(),
"must have parameters");
533 method_qualifier, value);
535 if(!value.
is_nil() && !is_static)
538 error() <<
"no initialization allowed here" <<
eom;
555 error() <<
"expected 0 to mark pure virtual method, got " << i <<
eom;
589 compo.set_base_name(
"@vtable_pointer");
593 components.push_back(
compo);
639 for(
auto &arg : args)
663 lookup(args[0].get_identifier()).symbol_expr(),
671 expr_call.arguments().reserve(args.size());
673 for(
const auto &arg : args)
676 lookup(arg.get_identifier()).symbol_expr());
714 if(is_static && !is_method)
748 ops.push_back(value);
798 if(base_name.
empty())
842 if(!
id.is_class() && !
id.is_enum())
845 error() <<
"'" << base_name <<
"' already in compound scope" <<
eom;
873 error() <<
"friend template not supported" <<
eom;
886 error() <<
"unexpected friend" <<
eom;
893 error() <<
"friend declaration must not have compound body" <<
eom;
909 std::cout <<
"friend declaration: " << declaration.
pretty() <<
'\n';
915 std::cout <<
"decl: " <<
sub_it.pretty() <<
"\n with value "
916 <<
sub_it.value().pretty() <<
'\n';
920 if(
sub_it.value().is_not_nil())
953 error() <<
"union types must not have bases" <<
eom;
994 if(declaration.
type().
id().empty())
1010 bool is_mutable=declaration.
storage_spec().is_mutable();
1017 error() <<
"invalid storage class specified for field" <<
eom;
1038 error() <<
"member declaration does not declare anything"
1044 declaration,
access, components);
1065 declaration, declarator, components,
1066 access, is_static, is_typedef, is_mutable);
1069 else if(it->id()==
"cpp-public")
1071 else if(it->id()==
"cpp-private")
1073 else if(it->id()==
"cpp-protected")
1092 dtor,
dtor.declarators()[0], components,
1131 declarator.name().get_base_name();
1134 if(declarator.value().is_not_nil())
1142 {}, type.
components(), declarator.member_initializers());
1149 declarator.member_initializers());
1154 declarator.member_initializers());
1161 bool is_mutable=declaration.
storage_spec().is_mutable();
1166 declaration, declarator, components,
1167 access, is_static, is_typedef, is_mutable);
1170 else if(it->id()==
"cpp-public")
1172 else if(it->id()==
"cpp-private")
1174 else if(it->id()==
"cpp-protected")
1195 cpctor.declarators()[0].value()=value;
1214 assignop.declarators().push_back(declarator);
1243 error() <<
"only constructors are allowed to "
1244 <<
"have member initializers" <<
eom;
1251 error() <<
"only constructors with body are allowed to "
1252 <<
"have member initializers" <<
eom;
1259 exprt::operandst::iterator
o_it=value.
operands().begin();
1273 const typet &method_qualifier,
1280 if(!method_qualifier.
id().empty())
1283 error() <<
"method is static -- no qualifiers allowed" <<
eom;
1315 symbol.base_name=
component.get_base_name();
1316 symbol.value.swap(value);
1317 symbol.module=
module;
1318 symbol.location=
component.source_location();
1327 *new_symbol = std::move(symbol);
1332 error() <<
"failed to insert new method symbol: " << symbol.name <<
'\n'
1333 <<
"name of previous symbol: " << new_symbol->
name <<
'\n'
1334 <<
"location of previous symbol: " << new_symbol->
location <<
eom;
1350 const typet &method_qualifier)
1373 parameters.insert(parameters.begin(),
parameter);
1394 error() <<
"anonymous struct/union member '"
1396 <<
"' shall not have function members" <<
eom;
1400 if(
comp.get_anonymous())
1413 error() <<
"'" << base_name <<
"' already in scope" <<
eom;
1419 id.identifier=
comp.get_name();
1444 error() <<
"storage class is not allowed here" <<
eom;
1451 error() <<
"anonymous struct/union member is not POD" <<
eom;
1456 irep_idt base_name=
"#anon_member"+std::to_string(components.size());
1462 typet compound_type;
1487 const exprt &
object,
1507 tmp.add_source_location()=source_location;
1509 if(
component.get_name()==component_name)
1524 error() <<
"member '" << component_name <<
"' is not accessible ("
1567 error() <<
"member '" << component_name <<
"' is not accessible"
1610 !(
pscope->is_root_scope());
1638 !(
pscope->is_root_scope());
1656 for(
const auto &
b : type.
bases())
1669 std::list<irep_idt> &
vbases)
const
1674 for(
const auto &
b : type.
bases())
1694 std::set<irep_idt> bases;
1698 return bases.find(
to.get(
ID_name))!=bases.end();
pointer_typet pointer_type(const typet &subtype)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
symbol_table_baset & symbol_table
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void make_constant_index(exprt &expr)
A codet representing sequential composition of program statements.
codet representation of an expression statement.
codet representation of a "return from a function" statement.
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
const declaratorst & declarators() const
bool is_destructor() const
const cpp_member_spect & member_spec() const
const cpp_storage_spect & storage_spec() const
bool is_constructor() const
void name_anon_struct_union()
irept & member_initializers()
typet merge_type(const typet &declaration_type) const
bool is_template_scope() const
const source_locationt & source_location() const
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
cpp_scopet & get_global_scope()
cpp_scopet & get_scope(const irep_idt &identifier)
cpp_scopet & set_scope(const irep_idt &identifier)
void go_to_global_scope()
cpp_scopet & current_scope()
cpp_scopet & get_parent() const
cpp_idt & insert(const irep_idt &_base_name)
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
bool contains(const irep_idt &base_name_to_lookup)
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
void typecheck_compound_body(symbolt &symbol)
void do_virtual_table(const symbolt &symbol)
void put_compound_into_scope(const struct_union_typet::componentt &component)
void typecheck_type(typet &) override
void convert_anon_struct_union_member(const cpp_declarationt &declaration, const irep_idt &access, struct_typet::componentst &components)
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
static bool has_const(const typet &type)
dynamic_initializationst dynamic_initializations
void convert_template_declaration(cpp_declarationt &declaration)
void typecheck_compound_declarator(const symbolt &symbol, const cpp_declarationt &declaration, cpp_declaratort &declarator, struct_typet::componentst &components, const irep_idt &access, bool is_static, bool is_typedef, bool is_mutable)
void default_dtor(const symbolt &symb, cpp_declarationt &dtor)
Note:
bool check_component_access(const struct_union_typet::componentt &component, const struct_union_typet &struct_union_type)
void typecheck_member_function(const symbolt &compound_symbol, struct_typet::componentt &component, irept &initializers, const typet &method_qualifier, exprt &value)
bool cpp_is_pod(const typet &type) const
void check_fixed_size_array(typet &type)
check that an array has fixed size
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
bool find_assignop(const symbolt &symbol) const
bool get_component(const source_locationt &source_location, const exprt &object, const irep_idt &component_name, exprt &member)
void typecheck_compound_type(struct_union_typet &) override
void add_anonymous_members_to_scope(const symbolt &struct_union_symbol)
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
std::unordered_set< irep_idt > deferred_typechecking
void add_method_body(symbolt *_method_symbol)
void check_member_initializers(const struct_typet::basest &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
void typecheck_compound_bases(struct_typet &type)
void elaborate_class_template(const typet &type)
elaborate class template instances
static bool has_auto(const typet &type)
static bool has_volatile(const typet &type)
irep_idt function_identifier(const typet &type)
for function overloading
void typecheck_friend_declaration(symbolt &symbol, cpp_declarationt &cpp_declaration)
void add_this_to_method_type(const symbolt &compound_symbol, code_typet &method_type, const typet &method_qualifier)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type)
void convert_parameter(const irep_idt ¤t_mode, code_typet::parametert ¶meter)
bool find_cpctor(const symbolt &symbol) const
void move_member_initializers(irept &initializers, const code_typet &type, exprt &value)
bool disable_access_control
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
void get_bases(const struct_typet &type, std::set< irep_idt > &set_bases) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
void move_to_sub(irept &irep)
const irep_idt & id() const
irept & add(const irep_idt &name)
const std::string & get_string(const irep_idt &name) const
Extract member of struct or union.
source_locationt source_location
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A side_effect_exprt representation of a function call side effect.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
const basest & bases() const
Get the collection of base classes/structs.
const irep_idt & get_base_name() const
const irep_idt & get_name() const
Base type for structs and unions.
irep_idt default_access() const
Return the access specification for members where access has not been modified.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
const irep_idt & get_identifier() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Semantic type conversion.
The type of an expression, extends irept.
const source_locationt & source_location() const
A union tag type, i.e., union_typet with an identifier.
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
cpp_namet & to_cpp_name(irept &cpp_name)
std::string cpp_type2name(const typet &type)
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
static bool symbol_exists(const goto_modelt &goto_model, const irep_idt &name, const bool require_has_code_type, const bool require_body_available)
Returns true iff the given symbol exists and satisfies requirements.
#define Forall_operands(it, expr)
const std::string & id2string(const irep_idt &d)
static bool is_constructor(const irep_idt &method_name)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
static bool failed(bool error_indicator)
const type_with_subtypest & to_type_with_subtypes(const typet &type)