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, message_handlert &message_handler)
 
std::set< irep_idt > & function_calls ()
 
void operator() (const goto_programt &prog)
 

Protected Attributes

const goto_functionst & goto_functions
 
message_handlert & message_handler
 
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 121 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,
message_handlert &  message_handler 
)
inline

Definition at line 124 of file memory_predicates.h.

Member Function Documentation

◆ function_calls()

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

Definition at line 29 of file memory_predicates.cpp.

◆ operator()()

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

Definition at line 34 of file memory_predicates.cpp.

Member Data Documentation

◆ function_set

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

Definition at line 139 of file memory_predicates.h.

◆ goto_functions

const goto_functionst& functions_in_scope_visitort::goto_functions
protected

Definition at line 137 of file memory_predicates.h.

◆ message_handler

message_handlert& functions_in_scope_visitort::message_handler
protected

Definition at line 138 of file memory_predicates.h.

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