cprover
Loading...
Searching...
No Matches
dfcc_wrapper_program.cpp File Reference
+ 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.
 
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.
 

Function Documentation

◆ create_addr_of_contract_write_set()

static symbol_exprt create_addr_of_contract_write_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
static

Generate the contract write set pointer.

Definition at line 47 of file dfcc_wrapper_program.cpp.

◆ create_addr_of_ensures_write_set()

static symbol_exprt create_addr_of_ensures_write_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
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 symbol_exprt create_addr_of_is_fresh_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
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 symbol_exprt create_addr_of_requires_write_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
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 symbol_exprt create_contract_write_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
static

Generate the contract write set.

Definition at line 33 of file dfcc_wrapper_program.cpp.

◆ create_ensures_write_set()

static symbol_exprt create_ensures_write_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
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 symbol_exprt create_is_fresh_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
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 symbol_exprt create_requires_write_set ( symbol_table_baset & symbol_table,
dfcc_libraryt & library,
const symbolt & wrapper_symbol )
static

Definition at line 61 of file dfcc_wrapper_program.cpp.