41 op1.
type().
set(ID_C_reference,
true);
63 cpp_namet op0(member_base_name, source_location);
66 op1.
add(ID_component_cpp_name,
cpp_namet(member_base_name, source_location));
95 const cpp_namet array(member_base_name, source_location);
97 exprt member(ID_member);
99 ID_component_cpp_name,
cpp_namet(member_base_name, source_location));
133 ctor.
type().
id(ID_constructor);
134 ctor.
add(ID_storage_spec).
id(ID_cpp_storage_spec);
155 std::string param_identifier(
"ref");
161 const cpp_namet cpp_parameter(param_identifier, source_location);
166 parameter_tor.
set(ID_name, cpp_parameter);
172 parameter_decl.
set(ID_type, ID_merged_type);
174 sub.push_back(cppcomp.
as_type());
175 irept constnd(ID_const);
176 sub.push_back(
static_cast<const typet &
>(constnd));
181 decl0.
add(ID_type).
add(ID_parameters).
get_sub().push_back(parameter_decl);
184 irept &initializers=decl0.
add(ID_member_initializers);
185 initializers.
id(ID_member_initializers);
194 DATA_INVARIANT(b.id() == ID_base,
"base class expression expected");
205 const cpp_namet cppname(ctor_name, source_location);
207 codet mem_init(ID_member_initializer);
209 mem_init.
set(ID_member, cppname);
219 for(
const auto &mem_c : components)
222 if(mem_c.get_bool(ID_is_vtptr))
224 const cpp_namet cppname(mem_c.get_base_name(), source_location);
226 const symbolt &virtual_table_symbol_type =
239 exprt ptrmember(ID_ptrmember);
240 ptrmember.
set(ID_component_name, mem_c.get_name());
249 mem_c.get_bool(ID_from_base) || mem_c.get_bool(ID_is_type) ||
250 mem_c.get_bool(ID_is_static) || mem_c.type().id() == ID_code)
255 const irep_idt &mem_name = mem_c.get_base_name();
257 const cpp_namet cppname(mem_name, source_location);
259 codet mem_init(ID_member_initializer);
260 mem_init.
set(ID_member, cppname);
263 exprt memberexpr(ID_member);
264 memberexpr.
set(ID_component_cpp_name, cppname);
268 if(mem_c.type().id() == ID_array)
269 memberexpr.
set(ID_C_array_ini,
true);
289 std::string arg_name(
"ref");
291 cpctor.
add(ID_storage_spec).
id(ID_cpp_storage_spec);
292 cpctor.
type().
id(ID_struct_tag);
302 typet &declarator_type=declarator.
type();
306 declarator_name.
id(ID_cpp_name);
307 declarator_name.
get_sub().push_back(
irept(ID_operator));
310 declarator_type.
id(ID_function_type);
327 args_decl.
type().
id(ID_merged_type);
328 args_decl_type_sub.push_back(
331 args_decl_type_sub.push_back(
typet(ID_const));
338 args_decl_declor.
name() =
cpp_namet(arg_name, source_location);
342 args_decl_declor.
type().
set(ID_C_reference,
true);
357 std::string arg_name(
"ref");
362 DATA_INVARIANT(b.id() == ID_base,
"base class expression expected");
373 c.get_bool(ID_from_base) || c.get_bool(ID_is_type) ||
374 c.get_bool(ID_is_static) || c.get_bool(ID_is_vtptr) ||
375 c.type().id() == ID_code)
380 const irep_idt &mem_name = c.get_base_name();
382 if(c.type().id() == ID_array)
386 if(size_expr.
id()==ID_infinity)
394 const auto size = numeric_cast<mp_integer>(size_expr);
399 copy_array(source_location, mem_name, i, arg_name, block);
402 copy_member(source_location, mem_name, arg_name, block);
409 declarator.
value() = std::move(block);
423 const irept &initializers)
427 for(
const auto &initializer : initializers.
get_sub())
436 if(has_template_args)
444 for(
const auto &b : bases)
458 error() <<
"invalid initializer '" << member_name.
to_string() <<
"'"
468 for(
const auto &c : components)
470 if(c.get_base_name() != base_name)
475 !c.get_bool(ID_from_base) && !c.get_bool(ID_is_static) &&
476 c.type().id() != ID_code)
483 if(c.get_bool(ID_is_type))
485 if(c.type().id() != ID_struct_tag)
490 if(symb.
type.
id()!=ID_struct)
494 for(
const auto &b : bases)
507 c.get_bool(ID_from_base) && !c.get_bool(ID_is_type) &&
508 !c.get_bool(ID_is_static) && c.type().id() == ID_code &&
515 for(
const auto &b : bases)
518 member_type.
get(ID_identifier) ==
532 error() <<
"invalid initializer '" << base_name <<
"'" <<
eom;
554 irept final_initializers(ID_member_initializers);
556 if(struct_union_type.
id()==ID_struct)
560 std::list<irep_idt> vbases;
567 while(!vbases.empty())
575 codet mem_init(ID_member_initializer);
576 mem_init.
set(ID_member, cppname);
583 cpp_namet(
"@most_derived").as_expr(), std::move(block));
590 DATA_INVARIANT(b.id() == ID_base,
"base class expression expected");
610 if(!has_template_args)
617 for(
const auto &c : components)
620 c.get_base_name() == base_name && c.type().id() != ID_code &&
621 !c.get_bool(ID_is_type))
633 static_cast<const typet&
>(initializer.find(ID_member));
637 if(member_type.
id() != ID_struct_tag)
655 codet mem_init(ID_member_initializer);
656 mem_init.
set(ID_member, cppname);
660 if(b.get_bool(ID_virtual))
662 codet tmp(ID_member_initializer);
666 cpp_namet(
"@most_derived").as_expr(), std::move(tmp));
668 final_initializers.
get_sub().back().swap(cond);
674 for(
const auto &c : components)
677 if(c.get_bool(ID_is_vtptr))
679 const cpp_namet cppname(c.get_base_name(), c.source_location());
681 const symbolt &virtual_table_symbol_type =
684 const symbolt &virtual_table_symbol_var =
694 exprt ptrmember(ID_ptrmember);
695 ptrmember.
set(ID_component_name, c.get_name());
704 c.get_bool(ID_from_base) || c.type().id() == ID_code ||
705 c.get_bool(ID_is_type) || c.get_bool(ID_is_static))
710 const irep_idt &mem_name = c.get_base_name();
715 for(
auto &initializer : initializers.
get_sub())
717 if(initializer.get(ID_member)!=ID_cpp_name)
726 if(mem_name==base_name)
737 !found && c.type().id() == ID_pointer &&
738 c.type().get_bool(ID_C_reference))
741 error() <<
"reference must be explicitly initialized" <<
eom;
751 codet mem_init(ID_member_initializer);
752 mem_init.
set(ID_member, cppname);
757 initializers.
swap(final_initializers);
781 if(parameters.size() < 2)
786 const typet ¶meter1_type=parameter1.
type();
799 for(std::size_t i=2; i<parameters.size(); i++)
801 if(parameters[i].default_value().is_nil())
822 if(
component.get_base_name() !=
"operator=")
reference_typet reference_type(const typet &subtype)
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
Operator to return the address of an object.
static void make_already_typechecked(exprt &expr)
const exprt & size() const
A codet representing sequential composition of program statements.
void add(const codet &code)
codet representation of an expression statement.
A codet representing an assignment in the program.
codet representation of an if-then-else statement.
goto_instruction_codet representation of a "return from a function" statement.
std::vector< parametert > parameterst
const typet & return_type() const
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
const declaratorst & declarators() const
const typet & as_type() const
irep_idt get_base_name() const
const source_locationt & source_location() const
bool has_template_args() const
std::string to_string() const
const exprt & as_expr() const
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
void typecheck_type(typet &) override
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
bool cpp_is_pod(const typet &type) const
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
bool find_assignop(const symbolt &symbol) const
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
void check_member_initializers(const struct_typet::basest &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
bool find_cpctor(const symbolt &symbol) const
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
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.
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
void move_to_sub(irept &irep)
irept & add(const irep_idt &name)
source_locationt source_location
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
const typet & base_type() const
The type of the data what we point to.
A side_effect_exprt that performs an assignment.
void set_function(const irep_idt &function)
Structure type, corresponds to C style structs.
const basest & bases() const
Get the collection of base classes/structs.
std::vector< baset > basest
Base type for structs and unions.
const componentst & components() const
std::vector< componentt > componentst
irep_idt base_name
Base (non-scoped) name.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
const irep_idt & get_identifier() const
const typet & subtype() const
The type of an expression, extends irept.
const source_locationt & source_location() const
source_locationt & add_source_location()
cpp_namet & to_cpp_name(irept &cpp_name)
C++ Language Type Checking.
static void copy_array(const source_locationt &source_location, const irep_idt &member_base_name, mp_integer i, const irep_idt &arg_name, exprt &block)
Generate code to copy the member.
static void copy_member(const source_locationt &source_location, const irep_idt &member_base_name, const irep_idt &arg_name, exprt &block)
Generate code to copy the member.
static void copy_parent(const source_locationt &source_location, const irep_idt &parent_base_name, const irep_idt &arg_name, exprt &block)
Generate code to copy the parent.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_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)
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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const type_with_subtypest & to_type_with_subtypes(const typet &type)
const type_with_subtypet & to_type_with_subtype(const typet &type)