Go to the documentation of this file.
60 if(symbol.
type.
get_bool(ID_C_no_initialization_required))
84 goto_functionst::function_mapt::iterator fct_entry =
155 std::set<std::string> to_exclude;
157 for(
auto const &except : except_values)
159 const bool file_prefix_found = except.find(
":") != std::string::npos;
161 if(file_prefix_found)
163 to_exclude.insert(except);
166 to_exclude.insert(except.substr(2, except.length() - 2));
170 to_exclude.insert(
"./" + except);
185 symbol_it != symbol_table.
end();
188 symbolt &symbol = symbol_it.get_writeable_symbol();
191 if(to_exclude.find(qualified_name) != to_exclude.end())
193 symbol.
value.
set(ID_C_no_nondet_initialization, 1);
#define Forall_goto_program_instructions(it, program)
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.
source_locationt source_location
The location of the instruction in the source file.
#define CHECK_RETURN(CONDITION)
const irep_idt & display_name() const
Return language specific display name if present.
typet type
Type of symbol.
std::list< std::string > value_listt
function_mapt function_map
Expression to hold a symbol (variable)
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
virtual iteratort begin() override
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
virtual iteratort end() override
const std::string & id2string(const irep_idt &d)
codet code
Do not read or modify directly – use get_X() instead.
const irep_idt & get_identifier() const
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_function_callt & to_code_function_call(const codet &code)
A side_effect_exprt that returns a non-deterministically chosen value.
A collection of goto functions.
exprt value
Initial value of symbol.
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
goto_functionst goto_functions
GOTO functions.
const code_assignt & to_code_assign(const codet &code)
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components.
A generic container class for the GOTO intermediate representation of one function.
const irep_idt & get_file() const
bool has_prefix(const std::string &s, const std::string &prefix)
A codet representing an assignment in the program.
bool is_function_call() const
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.