cprover
|
#include <code_contracts.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 current_operation) |
assigns_clause_targett * | add_pointer_target (exprt current_operation) |
goto_programt | init_block (source_locationt location) |
goto_programt & | temporary_declarations (source_locationt location, irep_idt function_name, irep_idt language_mode) |
goto_programt | dead_stmts (source_locationt location, irep_idt function_name, irep_idt language_mode) |
goto_programt | havoc_code (source_locationt location, irep_idt function_name, irep_idt language_mode) |
exprt | alias_expression (const exprt &lhs) |
exprt | compatible_expression (const assigns_clauset &called_assigns) |
Protected Attributes | |
const exprt & | assigns_expr |
std::vector< assigns_clause_targett * > | targets |
goto_programt | standin_declarations |
code_contractst & | parent |
const irep_idt | function_id |
messaget | log |
Definition at line 328 of file code_contracts.h.
assigns_clauset::assigns_clauset | ( | const exprt & | assigns, |
code_contractst & | contract, | ||
const irep_idt | function_id, | ||
messaget | log_parameter | ||
) |
Definition at line 1430 of file code_contracts.cpp.
assigns_clauset::~assigns_clauset | ( | ) |
Definition at line 1445 of file code_contracts.cpp.
assigns_clause_targett * assigns_clauset::add_pointer_target | ( | exprt | current_operation | ) |
Definition at line 1482 of file code_contracts.cpp.
assigns_clause_targett * assigns_clauset::add_target | ( | exprt | current_operation | ) |
Definition at line 1453 of file code_contracts.cpp.
Definition at line 1554 of file code_contracts.cpp.
exprt assigns_clauset::compatible_expression | ( | const assigns_clauset & | called_assigns | ) |
Definition at line 1580 of file code_contracts.cpp.
goto_programt assigns_clauset::dead_stmts | ( | source_locationt | location, |
irep_idt | function_name, | ||
irep_idt | language_mode | ||
) |
Definition at line 1520 of file code_contracts.cpp.
goto_programt assigns_clauset::havoc_code | ( | source_locationt | location, |
irep_idt | function_name, | ||
irep_idt | language_mode | ||
) |
Definition at line 1537 of file code_contracts.cpp.
goto_programt assigns_clauset::init_block | ( | source_locationt | location | ) |
Definition at line 1487 of file code_contracts.cpp.
goto_programt & assigns_clauset::temporary_declarations | ( | source_locationt | location, |
irep_idt | function_name, | ||
irep_idt | language_mode | ||
) |
Definition at line 1501 of file code_contracts.cpp.
|
protected |
Definition at line 358 of file code_contracts.h.
|
protected |
Definition at line 364 of file code_contracts.h.
|
protected |
Definition at line 365 of file code_contracts.h.
|
protected |
Definition at line 363 of file code_contracts.h.
|
protected |
Definition at line 361 of file code_contracts.h.
|
protected |
Definition at line 360 of file code_contracts.h.