Go to the documentation of this file.
38 typedef std::list<irep_idt> symbol_listt;
39 symbol_listt symbol_list;
44 !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
45 symbol_pair.second.type.id() == ID_code &&
46 (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
47 symbol_pair.second.mode == ID_java ||
48 symbol_pair.second.mode ==
"jsil" ||
49 symbol_pair.second.mode == ID_statement_list))
51 symbol_list.push_back(symbol_pair.first);
55 for(
const auto &
id : symbol_list)
66 if(!symbol_pair.second.is_type &&
67 symbol_pair.second.type.id()==ID_code &&
68 symbol_pair.second.value.is_not_nil())
70 symbol_pair.second.value=
codet();
80 for(
const auto &label : i_it->labels)
93 if(!f.body.instructions.empty() &&
94 f.body.instructions.back().is_return())
98 if(!f.body.instructions.empty() &&
99 f.body.instructions.back().is_goto() &&
100 f.body.instructions.back().guard.is_true())
104 if(!f.body.instructions.empty())
113 last_instruction->is_goto() &&
114 last_instruction->get_condition().is_true())
120 if(last_instruction->is_return())
125 last_instruction->is_dead() &&
126 last_instruction != f.body.instructions.begin() &&
127 !last_instruction->is_target())
149 if(f.body_available())
158 f.set_parameter_identifiers(code_type);
166 for(
const auto &p : f.parameter_identifiers)
168 DATA_INVARIANT(!p.empty(),
"parameter identifier should not be empty");
171 "parameter identifier must be a known symbol");
194 f.type.return_type().id() != ID_constructor &&
195 f.type.return_type().id() != ID_destructor;
205 !f.body.instructions.empty() &&
211 f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
218 if(i_it->is_goto() && i_it->get_target()->is_end_function())
219 i_it->set_target(a_end);
224 f.body.destructive_append(tmp_end_function);
243 symbol_table_builder, goto_model.
goto_functions, message_handler);
255 symbol_table_builder, message_handler);
270 symbol_table_builder, message_handler);
#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.
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
void add_return(goto_functionst::goto_functiont &, const source_locationt &)
Fresh auxiliary symbol creation.
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
typet type
Type of symbol.
irept & add(const irep_namet &name)
std::string tmp_symbol_prefix
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
void compute_location_numbers()
void goto_convert(goto_functionst &functions)
function_mapt function_map
const codet & to_code(const exprt &expr)
void set_hidden()
Mark a symbol for internal use.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
struct goto_convertt::targetst targets
irep_idt mode
Language mode.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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)
The symbol table base class interface.
#define INITIALIZE_FUNCTION
void set_return(goto_programt::targett _return_target)
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
lifetimet
Selects the kind of objects allocated.
static instructiont make_return(const source_locationt &l=source_locationt::nil())
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
A collection of goto functions.
exprt value
Initial value of symbol.
codet representation of a "return from a function" statement.
goto_functionst goto_functions
GOTO functions.
virtual ~goto_convert_functionst()
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
A generic container class for the GOTO intermediate representation of one function.
goto_convert_functionst(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
static bool hide(const goto_programt &)
symbol_table_baset & symbol_table
const code_blockt & to_code_block(const codet &code)
instructionst::const_iterator const_targett
bool has_prefix(const std::string &s, const std::string &prefix)
Goto Programs with Functions.
const irep_idt & get_statement() const
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
irep_idt name
The unique identifier.
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
source_locationt end_location() const
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Data structure for representing an arbitrary statement in a program.