goto_loops.cpp File Reference

#include "irep2/irep2_utils.h"
#include <goto-programs/goto_loops.h>
#include <util/config/config.h>
#include <util/expr/expr_util.h>

Include dependency graph for goto_loops.cpp:

Functions
static bool	indexes_through_pointer (const expr2tc &expr)
static expr2tc	extract_queried_pointer (const expr2tc &expr)
bool	check_var_name (const expr2tc &expr)
	True for symbols that name genuine user storage — excludes ESBMC internals, return-value temporaries, k-induction-generated names, etc.
static bool	writes_through_pointer (const expr2tc &lhs)
	True when a write target is storage reached through a pointer (*p = ..., p->f = ..., p->e[i] = ..., ((S *)v)->f = ...): nothing named is written, so a havoc over named symbols cannot cover it.
static expr2tc	written_pointee (const expr2tc &lhs)
static void	record_pointer_write (loopst &loop, const expr2tc &lhs)
static std::vector< expr2tc >	written_arguments (const irep_idt &function, const std::vector< expr2tc > &args)
static expr2tc	replace_symbols (const expr2tc &e, const std::unordered_map< irep_idt, expr2tc, irep_id_hash > &by)
static bool	is_unassigned_parameter (expr2tc ptr, const std::vector< irep_idt > &params, const loopst::loop_varst &modified)
	The caller havocs what a call's pointer arguments point to, which covers a write through a parameter the callee never reassigns, and nothing else: not a global pointer, nor a pointer loaded through the parameter.
static void	record_callee_pointer_writes (loopst &loop, const code_function_call2t &call)
	A callee writing through its own parameter names storage the caller cannot: the parameter is out of scope at the call.

Function Documentation

check_var_name()

bool check_var_name

(

const expr2tc &

expr

)

True for symbols that name genuine user storage — excludes ESBMC internals, return-value temporaries, k-induction-generated names, etc.

Defined in goto_loops.cpp; declared here so the k-induction pass can reuse it when filtering value-set objects (issue #5230).

extract_queried_pointer()

expr2tc extract_queried_pointer ( const expr2tc & expr )

static

indexes_through_pointer()

bool indexes_through_pointer ( const expr2tc & expr )

static

is_unassigned_parameter()

bool is_unassigned_parameter ( expr2tc ptr, const std::vector< irep_idt > & params, const loopst::loop_varst & modified )

static

The caller havocs what a call's pointer arguments point to, which covers a write through a parameter the callee never reassigns, and nothing else: not a global pointer, nor a pointer loaded through the parameter.

record_callee_pointer_writes()

void record_callee_pointer_writes ( loopst & loop, const code_function_call2t & call )

static

A callee writing through its own parameter names storage the caller cannot: the parameter is out of scope at the call.

The call's own pointer arguments are what it was handed, so record those and let the havoc reach the pointee through them. Recording an argument the callee never writes only widens the abstraction, which stays sound (issue #7478).

record_pointer_write()

void record_pointer_write ( loopst & loop, const expr2tc & lhs )

static

replace_symbols()

expr2tc replace_symbols ( const expr2tc & e, const std::unordered_map< irep_idt, expr2tc, irep_id_hash > & by )

static

writes_through_pointer()

bool writes_through_pointer ( const expr2tc & lhs )

static

True when a write target is storage reached through a pointer (*p = ..., p->f = ..., p->e[i] = ..., ((S *)v)->f = ...): nothing named is written, so a havoc over named symbols cannot cover it.

Writing the pointer variable itself (p = ...) names a symbol the havoc does cover.

written_arguments()

std::vector< expr2tc > written_arguments ( const irep_idt & function, const std::vector< expr2tc > & args )

static

written_pointee()

expr2tc written_pointee ( const expr2tc & lhs )

static