cprover
functionst Class Reference

#include <functions.h>

Collaboration diagram for functionst:
[legend]

Classes

struct  function_infot
 

Public Member Functions

 functionst (prop_convt &_prop_conv)
 
virtual ~functionst ()
 
void record (const function_application_exprt &function_application)
 
virtual void post_process ()
 

Protected Types

typedef std::set< function_application_exprtapplicationst
 
typedef std::map< exprt, function_infotfunction_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

prop_convtprop_conv
 
function_mapt function_map
 

Detailed Description

Definition at line 21 of file functions.h.

Member Typedef Documentation

§ applicationst

Definition at line 42 of file functions.h.

§ function_mapt

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

Definition at line 49 of file functions.h.

Constructor & Destructor Documentation

§ functionst()

functionst::functionst ( prop_convt _prop_conv)
inlineexplicit

Definition at line 24 of file functions.h.

§ ~functionst()

virtual functionst::~functionst ( )
inlinevirtual

Definition at line 27 of file functions.h.

References record().

Member Function Documentation

§ add_function_constraints() [1/2]

void functionst::add_function_constraints ( )
protectedvirtual

Definition at line 23 of file functions.cpp.

References function_map.

Referenced by post_process().

§ add_function_constraints() [2/2]

void functionst::add_function_constraints ( const function_infot info)
protectedvirtual

§ arguments_equal()

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

Definition at line 32 of file functions.cpp.

References exprt::make_typecast(), exprt::operands(), and exprt::type().

Referenced by add_function_constraints().

§ post_process()

virtual void functionst::post_process ( )
inlinevirtual

Definition at line 34 of file functions.h.

References add_function_constraints().

Referenced by boolbvt::post_process().

§ record()

void functionst::record ( const function_application_exprt function_application)

Member Data Documentation

§ function_map

function_mapt functionst::function_map
protected

Definition at line 50 of file functions.h.

Referenced by add_function_constraints(), and record().

§ prop_conv

prop_convt& functionst::prop_conv
protected

Definition at line 40 of file functions.h.

Referenced by add_function_constraints().


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