12 #ifndef CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H 13 #define CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H 34 #endif // CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H 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-ty...
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.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Base class for all expressions.
The symbol table base class interface.
Expression to hold a symbol (variable)
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...