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:

• /home/runner/work/cbmc/cbmc/src/solvers/lowering/functions.h
• /home/runner/work/cbmc/cbmc/src/solvers/lowering/functions.cpp