dfcc_lift_memory_predicates.cpp File Reference

#include "dfcc_lift_memory_predicates.h"
#include <util/cprover_prefix.h>
#include <util/format_expr.h>
#include <util/graph.h>
#include <util/pointer_expr.h>
#include <util/replace_symbol.h>
#include <util/symbol.h>
#include <goto-programs/goto_model.h>
#include "dfcc_instrument.h"
#include "dfcc_library.h"
#include "dfcc_utils.h"

Include dependency graph for dfcc_lift_memory_predicates.cpp:

Go to the source code of this file.

Functions
static bool	is_core_memory_predicate (const irep_idt &function_id)
	True iff function_id is a core memory predicate. More...
static std::optional< std::size_t >	is_param_expr (const exprt &expr, const std::map< irep_idt, std::size_t > &parameter_rank)

Function Documentation

is_core_memory_predicate()

static bool is_core_memory_predicate ( const irep_idt &  function_id )

static

True iff function_id is a core memory predicate.

Definition at line 45 of file dfcc_lift_memory_predicates.cpp.

is_param_expr()

static std::optional<std::size_t> is_param_expr ( const exprt &  expr, const std::map< irep_idt, std::size_t > &  parameter_rank  )

static

Definition at line 183 of file dfcc_lift_memory_predicates.cpp.