cprover
|
Pointer Dereferencing. More...
#include "add_failed_symbols.h"
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <util/std_expr.h>
Go to the source code of this file.
Functions | |
irep_idt | failed_symbol_id (const irep_idt &id) |
void | add_failed_symbol (symbolt &symbol, symbol_tablet &symbol_table) |
void | add_failed_symbols (symbol_tablet &symbol_table) |
exprt | get_failed_symbol (const symbol_exprt &expr, const namespacet &ns) |
Pointer Dereferencing.
Definition in file add_failed_symbols.cpp.
void add_failed_symbol | ( | symbolt & | symbol, |
symbol_tablet & | symbol_table | ||
) |
Definition at line 23 of file add_failed_symbols.cpp.
References symbolt::base_name, failed_symbol_id(), irept::get(), irept::id(), symbolt::is_lvalue, irept::make_nil(), symbolt::mode, symbolt::module, symbol_tablet::move(), symbolt::name, irept::set(), typet::subtype(), symbolt::type, and symbolt::value.
Referenced by add_failed_symbols().
void add_failed_symbols | ( | symbol_tablet & | symbol_table | ) |
Definition at line 52 of file add_failed_symbols.cpp.
References add_failed_symbol(), Forall_symbols, and symbol_tablet::symbols.
Referenced by goto_fence_inserter_parse_optionst::instrument_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), goto_diff_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
Definition at line 18 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 | ||
) |
Definition at line 72 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(), goto_symext::symex_dead(), and goto_symext::symex_decl().