CBMC
resolve_inherited_component.h File Reference

Given a class and a component (either field or method), find the closest parent that defines that component. More...

#include <util/irep.h>
#include <functional>
#include <optional>
+ Include dependency graph for resolve_inherited_component.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  resolve_inherited_componentt
 
class  resolve_inherited_componentt::inherited_componentt
 

Functions

std::optional< resolve_inherited_componentt::inherited_componenttget_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. More...
 

Detailed Description

Given a class and a component (either field or method), find the closest parent that defines that component.

Definition in file resolve_inherited_component.h.

Function Documentation

◆ get_inherited_method_implementation()

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.

For example, a reference Child.abc refers to Child's method or field if it exists, or else Parent.abc, and so on regarding Parent's ancestors. If none are found, an empty string will be returned. This looks first for non-abstract methods inherited from the first base (i.e., for Java the superclass), then for non-abstract methods inherited otherwise (for Java, interface default methods), then for any abstract declaration.

Parameters
classnameThe name of the class the function is being called on
call_basenameThe base name of the component (i.e. without the class specifier)
symbol_tableGlobal symbol table
Returns
The concrete component that has been resolved

Definition at line 126 of file resolve_inherited_component.cpp.