Loading...

Searching...

No Matches

dfcc_infer_loop_assigns.cpp File Reference

#include "dfcc_infer_loop_assigns.h"
#include <util/find_symbols.h>
#include <util/pointer_expr.h>
#include <goto-programs/goto_inline.h>
#include <analyses/goto_rw.h>
#include <analyses/local_may_alias.h>
#include <goto-instrument/contracts/utils.h>
#include "dfcc_loop_nesting_graph.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.

std::unordered_set< irep_idt > gen_loop_locals_set (const irep_idt &function_id, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop_node, message_handlert &message_handler, const namespacet &ns)

Collect identifiers that are local to this loop.

static std::unordered_set< irep_idt > find_symbol_identifiers (const goto_programt &src)

Find all identifiers in src.

static assignst dfcc_infer_loop_assigns_for_loop (const local_may_aliast &local_may_alias, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop, const std::unordered_set< irep_idt > &candidate_targets, message_handlert &message_handler, const namespacet &ns)

Infer loop assigns in the given loop.

static void remove_dead_object_assignment (goto_functiont &goto_function)

Remove assignments to __CPROVER_dead_object to avoid aliasing all targets that are assigned to __CPROVER_dead_object.

void dfcc_infer_loop_assigns_for_function (std::map< std::size_t, assignst > &inferred_loop_assigns_map, goto_functionst &goto_functions, const goto_functiont &goto_function, message_handlert &message_handler, const namespacet &ns)

Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis at the function level (with inlining), and store the result in inferred_loop_assigns_map, a map from loop numbers to the set of inferred assigns targets.

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 39 of file dfcc_infer_loop_assigns.cpp.

◆ dfcc_infer_loop_assigns_for_function()

void dfcc_infer_loop_assigns_for_function ( std::map< std::size_t, assignst > & inferred_loop_assigns_map,

goto_functionst & goto_functions,

const goto_functiont & goto_function,

message_handlert & message_handler,

const namespacet & ns

)

Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis at the function level (with inlining), and store the result in inferred_loop_assigns_map, a map from loop numbers to the set of inferred assigns targets.

Definition at line 299 of file dfcc_infer_loop_assigns.cpp.

◆ dfcc_infer_loop_assigns_for_loop()

static assignst dfcc_infer_loop_assigns_for_loop ( const local_may_aliast & local_may_alias,

goto_functiont & goto_function,

const dfcc_loop_nesting_graph_nodet & loop,

const std::unordered_set< irep_idt > & candidate_targets,

message_handlert & message_handler,

const namespacet & ns

)

static

Infer loop assigns in the given loop.

Loop assigns should depend on some identifiers in candidate_targets. function_assigns_map contains the function contracts used to infer loop assigns of function_call instructions.

Definition at line 213 of file dfcc_infer_loop_assigns.cpp.