CBMC
|
#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"
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) More... | |
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 . More... | |
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) |
Returns true iff expr
contains at least one identifier found in identifiers
.
Definition at line 37 of file dfcc_infer_loop_assigns.cpp.
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.
|
static |
Builds a call expression object_whole(expr)
Definition at line 22 of file dfcc_infer_loop_assigns.cpp.