#include <goto-programs/goto_functions.h>
#include <goto-programs/loopst.h>
#include <util/irep/std_types.h>
#include <unordered_map>

Include dependency graph for goto_loops.h:

This graph shows which files directly or indirectly include this file:

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

Functions
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.

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).