CBMC
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
functionst Class Reference

#include <functions.h>

+ Collaboration diagram for functionst:

Classes

struct  function_infot
 

Public Member Functions

 functionst (decision_proceduret &_decision_procedure)
 
virtual ~functionst ()
 
void record (const function_application_exprt &function_application)
 
virtual void finish_eager_conversion ()
 

Protected Types

typedef std::set< function_application_exprt > applicationst
 
typedef std::map< exprt, function_infot > function_mapt
 

Protected Member Functions

virtual void add_function_constraints ()
 
virtual void add_function_constraints (const function_infot &info)
 
exprt arguments_equal (const exprt::operandst &o1, const exprt::operandst &o2)
 

Protected Attributes

decision_proceduret & decision_procedure
 
function_mapt function_map
 

Detailed Description

Definition at line 22 of file functions.h.

Member Typedef Documentation

◆ applicationst

typedef std::set<function_application_exprt> functionst::applicationst
protected

Definition at line 44 of file functions.h.

◆ function_mapt

typedef std::map<exprt, function_infot> functionst::function_mapt
protected

Definition at line 51 of file functions.h.

Constructor & Destructor Documentation

◆ functionst()

functionst::functionst ( decision_proceduret &  _decision_procedure)
inlineexplicit

Definition at line 25 of file functions.h.

◆ ~functionst()

virtual functionst::~functionst ( )
inlinevirtual

Definition at line 30 of file functions.h.

Member Function Documentation

◆ add_function_constraints() [1/2]

void functionst::add_function_constraints ( )
protectedvirtual

Definition at line 21 of file functions.cpp.

◆ add_function_constraints() [2/2]

void functionst::add_function_constraints ( const function_infot &  info)
protectedvirtual

Definition at line 46 of file functions.cpp.

◆ arguments_equal()

exprt functionst::arguments_equal ( const exprt::operandst &  o1,
const exprt::operandst &  o2 
)
protected

Definition at line 27 of file functions.cpp.

◆ finish_eager_conversion()

virtual void functionst::finish_eager_conversion ( )
inlinevirtual

Definition at line 36 of file functions.h.

◆ record()

void functionst::record ( const function_application_exprt &  function_application)

Definition at line 15 of file functions.cpp.

Member Data Documentation

◆ decision_procedure

decision_proceduret& functionst::decision_procedure
protected

Definition at line 42 of file functions.h.

◆ function_map

function_mapt functionst::function_map
protected

Definition at line 52 of file functions.h.

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