add_failed_symbols.h File Reference

Pointer Dereferencing. More...

#include <util/expr.h>

Include dependency graph for add_failed_symbols.h:

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

Go to the source code of this file.

Functions
void	add_failed_symbols (symbol_table_baset &symbol_table)
	Create a failed-dereference symbol for all symbols in the given table that need one (i.e. More...
void	add_failed_symbol_if_needed (const symbolt &symbol, symbol_table_baset &symbol_table)
	Create a failed-dereference symbol for the given base symbol if it is pointer-typed, an lvalue, and doesn't already have one. More...
irep_idt	failed_symbol_id (const irep_idt &identifier)
	Get the name of the special symbol used to denote an unknown referee pointed to by a given pointer-typed symbol. More...
std::optional< symbol_exprt >	get_failed_symbol (const symbol_exprt &expr, const namespacet &ns)
	Get the failed-dereference symbol for the given symbol. More...
bool	is_failed_symbol (const exprt &expr)
	Return true if, and only if, expr is the result of failed dereferencing. More...

Detailed Description

Pointer Dereferencing.

Definition in file add_failed_symbols.h.

Function Documentation

add_failed_symbol_if_needed()

void add_failed_symbol_if_needed	(	const symbolt &	symbol,
		symbol_table_baset &	symbol_table
	)

Create a failed-dereference symbol for the given base symbol if it is pointer-typed, an lvalue, and doesn't already have one.

If any of these conditions are not met, do nothing.

Parameters

symbol	symbol to created a failed symbol for
symbol_table	global symbol table

Definition at line 62 of file add_failed_symbols.cpp.

add_failed_symbols()

void add_failed_symbols

(

symbol_table_baset &

symbol_table

)

Create a failed-dereference symbol for all symbols in the given table that need one (i.e.

pointer-typed lvalues).

Parameters

symbol_table

global symbol table

Definition at line 77 of file add_failed_symbols.cpp.

failed_symbol_id()

irep_idt failed_symbol_id

(

const irep_idt &

id

)

Get the name of the special symbol used to denote an unknown referee pointed to by a given pointer-typed symbol.

Parameters

id	base symbol id

Returns

id of the corresponding unknown-object ("failed") symbol.

Definition at line 26 of file add_failed_symbols.cpp.

get_failed_symbol()

std::optional<symbol_exprt> get_failed_symbol	(	const symbol_exprt &	expr,
		const namespacet &	ns
	)

Get the failed-dereference symbol for the given symbol.

Parameters

expr	symbol expression to get a failed symbol for
ns	global namespace

Returns

symbol expression for the failed-dereference symbol, or an empty optional if none exists.

Definition at line 91 of file add_failed_symbols.cpp.

is_failed_symbol()

bool is_failed_symbol ( const exprt &  expr )

inline

Return true if, and only if, expr is the result of failed dereferencing.

Definition at line 38 of file add_failed_symbols.h.