dfcc_wrapper_program.cpp File Reference
#include "dfcc_wrapper_program.h"#include <util/arith_tools.h>#include <util/c_types.h>#include <util/expr_util.h>#include <util/format_expr.h>#include <util/invariant.h>#include <util/mathematical_expr.h>#include <util/namespace.h>#include <util/pointer_offset_size.h>#include <util/std_expr.h>#include <goto-programs/goto_model.h>#include <ansi-c/c_expr.h>#include <goto-instrument/contracts/utils.h>#include <langapi/language_util.h>#include "dfcc_contract_functions.h"#include "dfcc_instrument.h"#include "dfcc_library.h"#include "dfcc_lift_memory_predicates.h"#include "dfcc_utils.h"
Include dependency graph for dfcc_wrapper_program.cpp:Go to the source code of this file.
Functions | |
| static symbol_exprt | create_contract_write_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate the contract write set. More... | |
| static symbol_exprt | create_addr_of_contract_write_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate the contract write set pointer. More... | |
| static symbol_exprt | create_requires_write_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| static symbol_exprt | create_addr_of_requires_write_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate the write set pointer to check side effects in requires clauses. More... | |
| static symbol_exprt | create_ensures_write_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate the write set to check side effects in ensures clauses. More... | |
| static symbol_exprt | create_addr_of_ensures_write_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate the write set pointer to check side effects in ensures clauses. More... | |
| static symbol_exprt | create_is_fresh_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate object set used to support is_fresh predicates. More... | |
| static symbol_exprt | create_addr_of_is_fresh_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate object set pointer used to support is_fresh predicates. More... | |
Function Documentation
◆ create_addr_of_contract_write_set()
|
static |
Generate the contract write set pointer.
Definition at line 47 of file dfcc_wrapper_program.cpp.
◆ create_addr_of_ensures_write_set()
|
static |
Generate the write set pointer to check side effects in ensures clauses.
Definition at line 103 of file dfcc_wrapper_program.cpp.
◆ create_addr_of_is_fresh_set()
|
static |
Generate object set pointer used to support is_fresh predicates.
Definition at line 131 of file dfcc_wrapper_program.cpp.
◆ create_addr_of_requires_write_set()
|
static |
Generate the write set pointer to check side effects in requires clauses.
Definition at line 75 of file dfcc_wrapper_program.cpp.
◆ create_contract_write_set()
|
static |
Generate the contract write set.
Definition at line 33 of file dfcc_wrapper_program.cpp.
◆ create_ensures_write_set()
|
static |
Generate the write set to check side effects in ensures clauses.
Definition at line 89 of file dfcc_wrapper_program.cpp.
◆ create_is_fresh_set()
|
static |
Generate object set used to support is_fresh predicates.
Definition at line 117 of file dfcc_wrapper_program.cpp.
◆ create_requires_write_set()
|
static |
Definition at line 61 of file dfcc_wrapper_program.cpp.
