CBMC
|
Pointer Dereferencing. More...
#include "add_failed_symbols.h"
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/symbol_table_base.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... | |
std::optional< symbol_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 35 of file add_failed_symbols.cpp.
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 62 of file add_failed_symbols.cpp.
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 77 of file add_failed_symbols.cpp.
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 26 of file add_failed_symbols.cpp.
std::optional<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 91 of file add_failed_symbols.cpp.