37 typedef std::list<irep_idt> symbol_listt;
38 symbol_listt symbol_list;
43 !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
44 symbol_pair.second.type.id() == ID_code &&
45 (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
46 symbol_pair.second.mode == ID_java || symbol_pair.second.mode ==
"jsil"))
48 symbol_list.push_back(symbol_pair.first);
52 for(
const auto &
id : symbol_list)
63 if(!symbol_pair.second.is_type &&
64 symbol_pair.second.type.id()==ID_code &&
65 symbol_pair.second.value.is_not_nil())
67 symbol_pair.second.value=
codet();
77 for(
const auto &label : i_it->labels)
90 if(!f.body.instructions.empty() &&
91 f.body.instructions.back().is_return())
95 if(!f.body.instructions.empty() &&
96 f.body.instructions.back().is_goto() &&
97 f.body.instructions.back().guard.is_true())
101 if(!f.body.instructions.empty())
104 f.body.instructions.end();
110 if(last_instruction->is_goto() &&
111 last_instruction->guard.is_true())
115 if(last_instruction->is_return())
119 if(last_instruction->is_dead() &&
120 last_instruction!=f.body.instructions.begin() &&
121 !last_instruction->is_target())
135 t->source_location=source_location;
145 if(f.body_available())
169 end_function->source_location=end_location;
170 end_function->code.
set(ID_identifier, identifier);
175 f.type.return_type().id()!=ID_empty &&
176 f.type.return_type().id()!=ID_constructor &&
177 f.type.return_type().id()!=ID_destructor;
186 if(!f.body.instructions.empty() &&
192 f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
195 a_end->make_atomic_end();
196 a_end->source_location=end_location;
200 if(i_it->is_goto() && i_it->get_target()->is_end_function())
201 i_it->set_target(a_end);
206 f.body.destructive_append(tmp_end_function);
209 f.update_instructions_function(identifier);
225 symbol_table_builder, goto_model.
goto_functions, message_handler);
237 symbol_table_builder, message_handler);
252 symbol_table_builder, message_handler);
const irep_idt & get_statement() const
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
struct goto_convertt::targetst targets
irep_idt mode
Language mode.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
source_locationt end_location() const
Fresh auxiliary symbol creation.
exprt value
Initial value of symbol.
function_mapt function_map
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
void compute_location_numbers()
std::string tmp_symbol_prefix
instructionst::iterator targett
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
instructionst::const_iterator const_targett
goto_convert_functionst(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
::goto_functiont goto_functiont
A side_effect_exprt that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static bool hide(const goto_programt &)
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
Goto Programs with Functions.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
The symbol table base class interface.
void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
virtual ~goto_convert_functionst()
void goto_convert(goto_functionst &functions)
symbol_table_baset & symbol_table
#define Forall_goto_program_instructions(it, program)
const codet & to_code(const exprt &expr)
const code_blockt & to_code_block(const codet &code)
Data structure for representing an arbitrary statement in a program.
void add_return(goto_functionst::goto_functiont &, const source_locationt &)
codet representation of a "return from a function" statement.
#define forall_goto_program_instructions(it, program)
void set_return(goto_programt::targett _return_target)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)