cprover
|
#include <functions.h>
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_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 | |
prop_convt & | prop_conv |
function_mapt | function_map |
Definition at line 21 of file functions.h.
|
protected |
Definition at line 42 of file functions.h.
|
protected |
Definition at line 49 of file functions.h.
|
inlineexplicit |
Definition at line 24 of file functions.h.
|
inlinevirtual |
Definition at line 27 of file functions.h.
|
protectedvirtual |
|
protectedvirtual |
Definition at line 58 of file functions.cpp.
References functionst::function_infot::applications, arguments_equal(), prop_conv, and decision_proceduret::set_to_true().
|
protected |
Definition at line 32 of file functions.cpp.
References exprt::make_typecast(), exprt::operands(), and exprt::type().
Referenced by add_function_constraints().
|
inlinevirtual |
Definition at line 34 of file functions.h.
References add_function_constraints().
Referenced by boolbvt::post_process().
void functionst::record | ( | const function_application_exprt & | function_application | ) |
Definition at line 16 of file functions.cpp.
References function_application_exprt::function(), and function_map.
Referenced by boolbvt::convert_function_application().
|
protected |
Definition at line 50 of file functions.h.
Referenced by add_function_constraints(), and record().
|
protected |
Definition at line 40 of file functions.h.
Referenced by add_function_constraints().