CBMC
Public Member Functions | Protected Attributes | List of all members
functions_in_scope_visitort Class Reference

Predicate to be used with the exprt::visit() function. More...

#include <memory_predicates.h>

+ Collaboration diagram for functions_in_scope_visitort:

Public Member Functions

 functions_in_scope_visitort (const goto_functionst &goto_functions, messaget &log)
 
std::set< irep_idt > & function_calls ()
 
void operator() (const goto_programt &prog)
 

Protected Attributes

const goto_functionst & goto_functions
 
messaget & log
 
std::set< irep_idt > function_set
 

Detailed Description

Predicate to be used with the exprt::visit() function.

The function found_return_value() will return true iff this predicate is called on an expr that contains __CPROVER_return_value.

Definition at line 113 of file memory_predicates.h.

Constructor & Destructor Documentation

◆ functions_in_scope_visitort()

functions_in_scope_visitort::functions_in_scope_visitort ( const goto_functionst &  goto_functions,
messaget &  log 
)
inline

Definition at line 116 of file memory_predicates.h.

Member Function Documentation

◆ function_calls()

std::set< irep_idt > & functions_in_scope_visitort::function_calls ( )

Definition at line 31 of file memory_predicates.cpp.

◆ operator()()

void functions_in_scope_visitort::operator() ( const goto_programt &  prog)

Definition at line 36 of file memory_predicates.cpp.

Member Data Documentation

◆ function_set

std::set<irep_idt> functions_in_scope_visitort::function_set
protected

Definition at line 131 of file memory_predicates.h.

◆ goto_functions

const goto_functionst& functions_in_scope_visitort::goto_functions
protected

Definition at line 129 of file memory_predicates.h.

◆ log

messaget& functions_in_scope_visitort::log
protected

Definition at line 130 of file memory_predicates.h.

The documentation for this class was generated from the following files: