cprover
|
Pointer Dereferencing. More...
#include "add_failed_symbols.h"
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <list>
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... | |
Pointer Dereferencing.
Definition in file add_failed_symbols.cpp.
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.
symbol | symbol to created a failed symbol for |
symbol_table | global 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().
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.
symbol | symbol to created a failed symbol for |
symbol_table | global 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().
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).
symbol_table | global 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().
Get the name of the special symbol used to denote an unknown referee pointed to by a given pointer-typed symbol.
id | base symbol id |
Definition at line 24 of file add_failed_symbols.cpp.
References id2string().
Referenced by add_failed_symbol(), and get_failed_symbol().
exprt get_failed_symbol | ( | const symbol_exprt & | expr, |
const namespacet & | ns | ||
) |
Get the failed-dereference symbol for the given symbol.
expr | symbol expression to get a failed symbol for |
ns | global namespace |
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().