CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
resolve_inherited_component.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: GOTO Program Utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
11#include <util/range.h>
12#include <util/std_types.h>
14
18 const symbol_table_baset &symbol_table)
19 : symbol_table(symbol_table)
20{
21}
22
35std::optional<resolve_inherited_componentt::inherited_componentt>
37 const irep_idt &class_id,
38 const irep_idt &component_name,
40 const std::function<bool(const symbolt &)> user_filter)
41{
42 PRECONDITION(!class_id.empty());
43 PRECONDITION(!component_name.empty());
44
45 std::vector<irep_idt> classes_to_visit;
46 classes_to_visit.push_back(class_id);
47 while(!classes_to_visit.empty())
48 {
50 classes_to_visit.pop_back();
51
54
55 const symbolt *symbol = symbol_table.lookup(full_component_identifier);
56 if(symbol && user_filter(*symbol))
57 {
58 return inherited_componentt(current_class, component_name);
59 }
60
61 const auto current_class_symbol_it =
62 symbol_table.symbols.find(current_class);
63
64 if(current_class_symbol_it != symbol_table.symbols.end())
65 {
66 const auto parents =
68 .map([](const struct_typet::baset &base) {
69 return base.type().get_identifier();
70 });
71
73 {
74 classes_to_visit.insert(
75 classes_to_visit.end(), parents.begin(), parents.end());
76 }
77 else
78 {
79 if(!parents.empty())
80 classes_to_visit.push_back(*parents.begin());
81 }
82 }
83 }
84
85 return {};
86}
87
95 const irep_idt &class_name, const irep_idt &component_name)
96{
97 // Verify the parameters are called in the correct order.
98 PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
99 PRECONDITION(id2string(component_name).find("::")==std::string::npos);
100 return id2string(class_name)+'.'+id2string(component_name);
101}
102
111
125std::optional<resolve_inherited_componentt::inherited_componentt>
127 const irep_idt &call_basename,
128 const irep_idt &classname,
130{
132 auto exclude_abstract_methods = [&](const symbolt &symbol) {
133 return !symbol.type.get_bool(ID_C_abstract);
134 };
135
136 auto resolved_call =
138 if(!resolved_call)
139 {
140 // Check for a default implementation:
143 }
144 if(!resolved_call)
145 {
146 // Finally accept any abstract definition, which will likely get stubbed:
148 }
149 return resolved_call;
150}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
irep_idt get_full_component_identifier() const
Get the full name of this function.
resolve_inherited_componentt(const symbol_table_baset &symbol_table)
See the operator() method comment.
std::optional< inherited_componentt > operator()(const irep_idt &class_id, const irep_idt &component_name, bool include_interfaces, std::function< bool(const symbolt &)> user_filter=[](const symbolt &) { return true;})
Given a class and a component, identify the concrete field or method it is resolved to.
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...
const symbol_table_baset & symbol_table
Base class or struct that a class or struct inherits from.
Definition std_types.h:252
struct_tag_typet & type()
Definition std_types.cpp:84
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
Given a class and a component (either field or method), find the closest parent that defines that com...
std::optional< resolve_inherited_componentt::inherited_componentt > get_inherited_method_implementation(const irep_idt &call_basename, const irep_idt &classname, const symbol_table_baset &symbol_table)
Given a class and a component, identify the concrete method it is resolved to.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
Author: Diffblue Ltd.