Go to the documentation of this file.
46 std::set<std::string> symbols;
48 for(
const auto &symbol_pair : symbol_table.
symbols)
50 symbols.insert(
id2string(symbol_pair.first));
53 for(
const std::string &
id : symbols)
55 const symbolt &symbol=ns.lookup(
id);
68 identifier==
"__func__" ||
69 identifier==
"__FUNCTION__" ||
70 identifier==
"__PRETTY_FUNCTION__" ||
71 identifier==
"argc'" ||
72 identifier==
"argv'" ||
73 identifier==
"envp'" ||
74 identifier==
"envp_size'")
84 if(type.
id()==ID_code ||
97 if(type.
id()==ID_array &&
103 writable_symbol.
type = type;
107 if(type.
id()==ID_incomplete_struct ||
108 type.
id()==ID_incomplete_union)
111 if(symbol.
value.
id()==ID_nondet)
133 for(
const std::string &
id : symbols)
135 const symbolt &symbol=ns.lookup(
id);
137 if(symbol.
type.
id() != ID_code)
147 dest.
add(function_call);
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
#define PRECONDITION(CONDITION)
The type of an expression, extends irept.
typet type
Type of symbol.
Base class for all expressions.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
const codet & to_code(const exprt &expr)
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
codet representation of a label for branch targets.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
#define INITIALIZE_FUNCTION
const irep_idt & id() const
void add(const codet &code)
const parameterst & parameters() const
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
exprt value
Initial value of symbol.
A codet representing a skip statement.
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const typet & return_type() const
const code_blockt & to_code_block(const codet &code)
bool has_prefix(const std::string &s, const std::string &prefix)
source_locationt & add_source_location()
unsignedbv_typet size_type()
A codet representing an assignment in the program.
irep_idt name
The unique identifier.
#define CHECK_RETURN(CONDITION)