cprover
|
#include <assigns.h>
Public Member Functions | |
assigns_clauset (const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter) | |
~assigns_clauset () | |
assigns_clause_targett * | add_target (exprt target) |
goto_programt | init_block () |
goto_programt | dead_stmts () |
goto_programt | havoc_code () |
exprt | alias_expression (const exprt &lhs) |
exprt | compatible_expression (const assigns_clauset &called_assigns) |
Protected Attributes | |
const exprt & | assigns |
std::vector< assigns_clause_targett * > | targets |
goto_programt | standin_declarations |
code_contractst & | parent |
const irep_idt | function_id |
messaget | log |
assigns_clauset::assigns_clauset | ( | const exprt & | assigns, |
code_contractst & | contract, | ||
const irep_idt | function_id, | ||
messaget | log_parameter | ||
) |
Definition at line 119 of file assigns.cpp.
assigns_clauset::~assigns_clauset | ( | ) |
Definition at line 135 of file assigns.cpp.
assigns_clause_targett * assigns_clauset::add_target | ( | exprt | target | ) |
Definition at line 143 of file assigns.cpp.
Definition at line 195 of file assigns.cpp.
exprt assigns_clauset::compatible_expression | ( | const assigns_clauset & | called_assigns | ) |
Definition at line 211 of file assigns.cpp.
goto_programt assigns_clauset::dead_stmts | ( | ) |
Definition at line 170 of file assigns.cpp.
goto_programt assigns_clauset::havoc_code | ( | ) |
Definition at line 184 of file assigns.cpp.
goto_programt assigns_clauset::init_block | ( | ) |
Definition at line 156 of file assigns.cpp.
|
protected |
|
protected |
|
protected |