cprover
add_failed_symbols.cpp File Reference

Pointer Dereferencing. More...

#include "add_failed_symbols.h"
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <list>
Include dependency graph for add_failed_symbols.cpp:

Go to the source code of this file.

Functions

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. More...
 
void add_failed_symbol (symbolt &symbol, symbol_table_baset &symbol_table)
 Create a failed-dereference symbol for the given base symbol if it is pointer-typed; if not, do nothing. 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...
 
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...
 
exprt get_failed_symbol (const symbol_exprt &expr, const namespacet &ns)
 Get the failed-dereference symbol for the given symbol. More...
 

Detailed Description

Pointer Dereferencing.

Definition in file add_failed_symbols.cpp.

Function Documentation

◆ add_failed_symbol()

void add_failed_symbol ( symbolt symbol,
symbol_table_baset symbol_table 
)

Create a failed-dereference symbol for the given base symbol if it is pointer-typed; if not, do nothing.

Parameters
symbolsymbol to created a failed symbol for
symbol_tableglobal symbol table

Definition at line 33 of file add_failed_symbols.cpp.

References symbolt::base_name, failed_symbol_id(), irept::id(), symbol_table_baset::insert(), symbolt::is_lvalue, irept::make_nil(), symbolt::mode, symbolt::module, symbolt::name, irept::set(), typet::subtype(), symbolt::type, and symbolt::value.

Referenced by add_failed_symbol_if_needed().

◆ 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
symbolsymbol to created a failed symbol for
symbol_tableglobal symbol table

Definition at line 61 of file add_failed_symbols.cpp.

References add_failed_symbol(), irept::get(), symbol_table_baset::get_writeable(), symbolt::is_lvalue, symbolt::name, and symbolt::type.

Referenced by add_failed_symbols(), and jbmc_parse_optionst::process_goto_function().

◆ 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_tableglobal symbol table

Definition at line 76 of file add_failed_symbols.cpp.

References add_failed_symbol_if_needed(), and symbol_table_baset::symbols.

Referenced by jbmc_parse_optionst::doit(), jbmc_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), and cbmc_parse_optionst::process_goto_program().

◆ 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
idbase symbol id
Returns
id of the corresponding unknown-object ("failed") symbol.

Definition at line 24 of file add_failed_symbols.cpp.

References id2string().

Referenced by add_failed_symbol(), and get_failed_symbol().

◆ get_failed_symbol()

exprt get_failed_symbol ( const symbol_exprt expr,
const namespacet ns 
)

Get the failed-dereference symbol for the given symbol.

Parameters
exprsymbol expression to get a failed symbol for
nsglobal namespace
Returns
symbol expression for the failed-dereference symbol, or nil_exprt if none exists.

Definition at line 94 of file add_failed_symbols.cpp.

References dstringt::empty(), failed_symbol_id(), irept::get(), namespacet::lookup(), and symbolt::type.

Referenced by value_sett::apply_code_rec(), goto_symext::symex_dead(), and goto_symext::symex_decl().