/*******************************************************************\
Module: C++ Language Type Checking
Author: Daniel Kroening, [email protected]
\*******************************************************************/
/// \file
/// C++ Language Type Checking
#include
#include
#include
#include
#include "cpp_typecheck.h"
void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
{
PRECONDITION(symbol.type.id() == ID_struct);
// builds virtual-table value maps: (class x virtual_name x value)
std::map > vt_value_maps;
const struct_typet &struct_type=to_struct_type(symbol.type);
for(std::size_t i=0; i < struct_type.components().size(); i++)
{
const struct_typet::componentt &compo=struct_type.components()[i];
if(!compo.get_bool(ID_is_virtual))
continue;
const code_typet &code_type=to_code_type(compo.type());
DATA_INVARIANT(code_type.parameters().size() > 0, "parameters expected");
const pointer_typet ¶meter_pointer_type=
to_pointer_type(code_type.parameters()[0].type());
const irep_idt &class_id =
parameter_pointer_type.base_type().get(ID_identifier);
std::map &value_map =
vt_value_maps[class_id];
exprt e=symbol_exprt(compo.get_name(), code_type);
if(compo.get_bool(ID_is_pure_virtual))
{
pointer_typet code_pointer_type=pointer_type(code_type);
e=null_pointer_exprt(code_pointer_type);
value_map[compo.get(ID_virtual_name)] = e;
}
else
{
address_of_exprt address(e);
value_map[compo.get(ID_virtual_name)] = address;
}
}
// create virtual-table symbol variables
for(std::map >::const_iterator cit =
vt_value_maps.begin(); cit!=vt_value_maps.end(); cit++)
{
const std::map &value_map=cit->second;
const symbolt &late_cast_symb = lookup(cit->first);
const symbolt &vt_symb_type =
lookup("virtual_table::" + id2string(late_cast_symb.name));
symbolt vt_symb_var{
id2string(vt_symb_type.name) + "@" + id2string(symbol.name),
struct_tag_typet(vt_symb_type.name),
symbol.mode};
vt_symb_var.base_name=
id2string(vt_symb_type.base_name) + "@" + id2string(symbol.base_name);
vt_symb_var.module=module;
vt_symb_var.location=vt_symb_type.location;
vt_symb_var.is_lvalue=true;
vt_symb_var.is_static_lifetime=true;
// do the values
const struct_typet &vt_type=to_struct_type(vt_symb_type.type);
struct_exprt values({}, struct_tag_typet(vt_symb_type.name));
for(const auto &compo : vt_type.components())
{
std::map::const_iterator cit2 =
value_map.find(compo.get_base_name());
CHECK_RETURN(cit2 != value_map.end());
const exprt &value=cit2->second;
DATA_INVARIANT(value.type() == compo.type(), "component type mismatch");
values.operands().push_back(value);
}
vt_symb_var.value=values;
bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
CHECK_RETURN(!failed);
}
}