38 identifier ==
CPROVER_PREFIX "memory" || identifier ==
"__func__" ||
39 identifier ==
"__FUNCTION__" || identifier ==
"__PRETTY_FUNCTION__" ||
40 identifier ==
"argc'" || identifier ==
"argv'" || identifier ==
"envp'" ||
41 identifier ==
"envp_size'")
51 if(type.
id() == ID_code || type.
id() == ID_empty)
59 writable_symbol.
type = type;
64 (type.
id() == ID_struct || type.
id() == ID_union) &&
96 return std::move(code);
110 init_symbol.value.add_source_location()=source_location;
120 std::set<std::string> symbols;
122 for(
const auto &symbol_pair : symbol_table.
symbols)
124 symbols.insert(
id2string(symbol_pair.first));
128 for(
const std::string &
id : symbols)
133 dest.
add(std::move(*code));
137 for(
const std::string &
id : symbols)
142 dest.
add(std::move(*code));
147 for(
const std::string &
id : symbols)
151 if(symbol.
type.
id() != ID_code)
161 dest.
add(function_call);
unsignedbv_typet size_type()
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void add(const codet &code)
codet representation of a function call statement.
codet representation of a label for branch targets.
A codet representing a skip statement.
const parameterst & parameters() const
const typet & return_type() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
bool get_bool(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
exprt value
Initial value of symbol.
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
optionalt< exprt > nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create a non-deterministic value for type type, with all subtypes independently expanded as non-deter...
Expression Initialization.
const std::string & id2string(const irep_idt &d)
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
nonstd::optional< T > optionalt
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
#define INITIALIZE_FUNCTION
const code_blockt & to_code_block(const codet &code)
const codet & to_code(const exprt &expr)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.