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_is_cprover_symbol.h"
#include "dfcc_library.h"
#include "dfcc_lift_memory_predicates.h"
#include "dfcc_pointer_equals.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_ptr_pred_ctx (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_ptr_pred_ctx (symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
	Generate object set pointer used to support is_fresh predicates.
void	disable_may_fail_rec (exprt &expr, bool no_fail)
	Recursively traverses expression, adding "no_fail" attributes to pointer predicates that we know cannot fail when invoked in an assume context: Starting from the root with "no_fail" true, we recurse over the boolean structure, setting the "no_fail" false for all but the last operand disjunctive operators like || and ==>, and distributing the current "no_fail" status over disjunctions.
void	disable_may_fail (exprt &expr)

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 49 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 105 of file dfcc_wrapper_program.cpp.

create_addr_of_ptr_pred_ctx()

static symbol_exprt create_addr_of_ptr_pred_ctx ( 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 133 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 77 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 35 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 91 of file dfcc_wrapper_program.cpp.

create_ptr_pred_ctx()

static symbol_exprt create_ptr_pred_ctx ( 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 119 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 63 of file dfcc_wrapper_program.cpp.

disable_may_fail()

void disable_may_fail

(

exprt &

expr

)

Definition at line 631 of file dfcc_wrapper_program.cpp.

disable_may_fail_rec()

void disable_may_fail_rec	(	exprt &	expr,
		bool	no_fail
	)

Recursively traverses expression, adding "no_fail" attributes to pointer predicates that we know cannot fail when invoked in an assume context: Starting from the root with "no_fail" true, we recurse over the boolean structure, setting the "no_fail" false for all but the last operand disjunctive operators like || and ==>, and distributing the current "no_fail" status over disjunctions.

For instance:

(len > 0):no_fail=false ==> is_fresh(p, len):no_fail=true

is_fresh(p, len):no_fail=true && is_fresh(q, len):no_fail=true

is_fresh(p, len):no_fail=false ||
is_fresh(q, len):no_fail=false ||
is_fresh(r, len):no_fail=true

is_fresh(p, len):no_fail=false ||
(
   is_fresh(q, len):no_fail=true &&
   (
     (len>0):no_fail=true ==> is_fresh(r, len):no_fail=true
   )
)

Parameters

expr	The expression to traverse
no_fail	The current no_fail value based on logical context

Definition at line 572 of file dfcc_wrapper_program.cpp.