dfcc_infer_loop_assigns.cpp File Reference

#include "dfcc_infer_loop_assigns.h"
#include <util/expr.h>
#include <util/find_symbols.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <goto-instrument/havoc_utils.h>
#include "dfcc_root_object.h"

Include dependency graph for dfcc_infer_loop_assigns.cpp:

Go to the source code of this file.

Functions
static exprt	make_object_whole_call_expr (const exprt &expr, const namespacet &ns)
	Builds a call expression object_whole(expr)
static bool	depends_on (const exprt &expr, std::unordered_set< irep_idt > identifiers)
	Returns true iff expr contains at least one identifier found in identifiers.
assignst	dfcc_infer_loop_assigns (const local_may_aliast &local_may_alias, const loopt &loop_instructions, const source_locationt &loop_head_location, const namespacet &ns)

Function Documentation

depends_on()

static bool depends_on ( const exprt & expr, std::unordered_set< irep_idt > identifiers )

static

Returns true iff expr contains at least one identifier found in identifiers.

Definition at line 37 of file dfcc_infer_loop_assigns.cpp.

dfcc_infer_loop_assigns()

assignst dfcc_infer_loop_assigns	(	const local_may_aliast &	local_may_alias,
		const loopt &	loop_instructions,
		const source_locationt &	loop_head_location,
		const namespacet &	ns )

Definition at line 48 of file dfcc_infer_loop_assigns.cpp.

make_object_whole_call_expr()

static exprt make_object_whole_call_expr ( const exprt & expr, const namespacet & ns )

static

Builds a call expression object_whole(expr)

Definition at line 22 of file dfcc_infer_loop_assigns.cpp.