Go to the source code of this file.
|
static symbol_exprt | create_contract_write_set (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol) |
| Generate the contract write set.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
◆ create_addr_of_contract_write_set()
◆ create_addr_of_ensures_write_set()
◆ create_addr_of_is_fresh_set()
◆ create_addr_of_requires_write_set()
◆ create_contract_write_set()
◆ create_ensures_write_set()
◆ create_is_fresh_set()
◆ create_requires_write_set()