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.
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.