goto_loopst::function_summaryt Struct Reference

Per-callee summary: the leaf symbols (post check_var_name filtering) that walking the callee's body would contribute to the current loop. More...

#include <goto_loops.h>

Public Member Functions
void	record_write (const expr2tc &lhs)
void	bind_arguments (const goto_functiont &callee, const std::vector< expr2tc > &arguments)
	Restate the callee's written pointers in the caller's scope: a parameter the callee never reassigns holds the argument this call passes, which resolves more precisely than the parameter every call site shares.

Public Attributes
loopst::loop_varst	modified
loopst::loop_varst	unmodified
bool	modifies_pointer_array = false
	True iff the callee writes an array element through a pointer, which havocking through the call's arguments cannot cover (#5224).
bool	writes_through_pointer = false
	True iff the callee writes through a dereference.
bool	pointer_write_unresolvable = false
	True iff the callee may write through a pointer it was not handed, so havocing the pointees of the call's arguments misses the write.
loopst::loop_varst	written_pointers
	The pointers the callee writes through, in its own scope, and whether it writes through one it cannot name.
bool	unnamed_write = false
std::unordered_set< irep_idt, irep_id_hash >	address_taken
	The variables whose address the callee takes.

Detailed Description

Per-callee summary: the leaf symbols (post check_var_name filtering) that walking the callee's body would contribute to the current loop.

Cached across loops in the same goto_loopst instance so two loops in the same outer function don't re-walk a shared helper.

Scope is intentionally per-instance (one goto_loopst per analysed function), not per-program: goto_k_induction constructs a fresh instance per outer function, and promoting the cache to a static would need invalidation across the goto-program rewrites that happen between functions.

Member Function Documentation

bind_arguments()

void goto_loopst::function_summaryt::bind_arguments	(	const goto_functiont &	callee,
		const std::vector< expr2tc > &	arguments )

Restate the callee's written pointers in the caller's scope: a parameter the callee never reassigns holds the argument this call passes, which resolves more precisely than the parameter every call site shares.

record_write()

void goto_loopst::function_summaryt::record_write

(

const expr2tc &

lhs

)

Member Data Documentation

address_taken

std::unordered_set<irep_idt, irep_id_hash> goto_loopst::function_summaryt::address_taken

The variables whose address the callee takes.

modified

loopst::loop_varst goto_loopst::function_summaryt::modified

modifies_pointer_array

bool goto_loopst::function_summaryt::modifies_pointer_array = false

True iff the callee writes an array element through a pointer, which havocking through the call's arguments cannot cover (#5224).

pointer_write_unresolvable

bool goto_loopst::function_summaryt::pointer_write_unresolvable = false

True iff the callee may write through a pointer it was not handed, so havocing the pointees of the call's arguments misses the write.

unmodified

loopst::loop_varst goto_loopst::function_summaryt::unmodified

unnamed_write

bool goto_loopst::function_summaryt::unnamed_write = false

writes_through_pointer

bool goto_loopst::function_summaryt::writes_through_pointer = false

True iff the callee writes through a dereference.

See loopst::set_writes_through_pointer and issue #7478.

written_pointers

loopst::loop_varst goto_loopst::function_summaryt::written_pointers

The pointers the callee writes through, in its own scope, and whether it writes through one it cannot name.

See loopst::add_written_pointer.

---

The documentation for this struct was generated from the following files:

• src/goto-programs/goto_loops.h
• src/goto-programs/goto_loops.cpp