cprover
resolve_inherited_component.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO Program Utilities
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include <algorithm>
10 
12 
16  const symbol_tablet &symbol_table)
17  : symbol_table(symbol_table)
18 {
19 }
20 
33  const irep_idt &class_id,
34  const irep_idt &component_name,
35  bool include_interfaces)
36 {
37  PRECONDITION(!class_id.empty());
38  PRECONDITION(!component_name.empty());
39 
40  std::vector<irep_idt> classes_to_visit;
41  classes_to_visit.push_back(class_id);
42  while(!classes_to_visit.empty())
43  {
44  irep_idt current_class = classes_to_visit.back();
45  classes_to_visit.pop_back();
46 
47  const irep_idt &full_component_identifier=
48  build_full_component_identifier(current_class, component_name);
49 
50  if(symbol_table.has_symbol(full_component_identifier))
51  {
52  return inherited_componentt(current_class, component_name);
53  }
54 
55  const auto current_class_symbol_it =
56  symbol_table.symbols.find(current_class);
57 
58  if(current_class_symbol_it != symbol_table.symbols.end())
59  {
60  const auto parents =
61  make_range(to_struct_type(current_class_symbol_it->second.type).bases())
62  .map([](const struct_typet::baset &base) {
63  return base.type().get_identifier();
64  });
65 
66  if(include_interfaces)
67  {
68  classes_to_visit.insert(
69  classes_to_visit.end(), parents.begin(), parents.end());
70  }
71  else
72  {
73  if(!parents.empty())
74  classes_to_visit.push_back(*parents.begin());
75  }
76  }
77  }
78 
79  return {};
80 }
81 
89  const irep_idt &class_name, const irep_idt &component_name)
90 {
91  // Verify the parameters are called in the correct order.
92  PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
93  PRECONDITION(id2string(component_name).find("::")==std::string::npos);
94  return id2string(class_name)+'.'+id2string(component_name);
95 }
96 
101 {
104 }
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
resolve_inherited_componentt::inherited_componentt
Definition: resolve_inherited_component.h:27
resolve_inherited_componentt::inherited_componentt::component_identifier
irep_idt component_identifier
Definition: resolve_inherited_component.h:44
resolve_inherited_componentt::inherited_componentt::get_full_component_identifier
irep_idt get_full_component_identifier() const
Get the full name of this function.
Definition: resolve_inherited_component.cpp:100
resolve_inherited_componentt::inherited_componentt::class_identifier
irep_idt class_identifier
Definition: resolve_inherited_component.h:43
resolve_inherited_component.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
dstringt::empty
bool empty() const
Definition: dstring.h:88
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
struct_typet::baset::type
struct_tag_typet & type()
Definition: std_types.cpp:73
resolve_inherited_componentt::symbol_table
const symbol_tablet & symbol_table
Definition: resolve_inherited_component.h:56
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
resolve_inherited_componentt::operator()
optionalt< inherited_componentt > operator()(const irep_idt &class_id, const irep_idt &component_name, bool include_interfaces)
Given a class and a component, identify the concrete field or method it is resolved to.
Definition: resolve_inherited_component.cpp:32
resolve_inherited_componentt::build_full_component_identifier
static irep_idt build_full_component_identifier(const irep_idt &class_name, const irep_idt &component_name)
Build a component name as found in a GOTO symbol table equivalent to the name of a concrete component...
Definition: resolve_inherited_component.cpp:88
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
resolve_inherited_componentt::resolve_inherited_componentt
resolve_inherited_componentt(const symbol_tablet &symbol_table)
See the operator() method comment.
Definition: resolve_inherited_component.cpp:15
struct_typet::baset
Base class or struct that a class or struct inherits from.
Definition: std_types.h:247