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 || symbol_pair.second.mode ==
"jsil"))
49 symbol_list.push_back(symbol_pair.first);
53 for(
const auto &
id : symbol_list)
64 if(!symbol_pair.second.is_type &&
65 symbol_pair.second.type.id()==ID_code &&
66 symbol_pair.second.value.is_not_nil())
68 symbol_pair.second.value=
codet();
78 for(
const auto &label : i_it->labels)
79 if(label==
"__CPROVER_HIDE")
91 if(!f.body.instructions.empty() &&
92 f.body.instructions.back().is_return())
96 if(!f.body.instructions.empty() &&
97 f.body.instructions.back().is_goto() &&
98 f.body.instructions.back().guard.is_true())
102 if(!f.body.instructions.empty())
105 f.body.instructions.end();
111 if(last_instruction->is_goto() &&
112 last_instruction->guard.is_true())
116 if(last_instruction->is_return())
120 if(last_instruction->is_dead() &&
121 last_instruction!=f.body.instructions.begin() &&
122 !last_instruction->is_target())
136 t->source_location=source_location;
146 if(f.body_available())
161 error() <<
"got invalid code for function `" << identifier <<
"'" 178 end_function->source_location=end_location;
179 end_function->code.
set(ID_identifier, identifier);
184 f.type.return_type().id()!=ID_empty &&
185 f.type.return_type().id()!=ID_constructor &&
186 f.type.return_type().id()!=ID_destructor;
195 if(!f.body.instructions.empty() &&
201 f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
204 a_end->make_atomic_end();
205 a_end->source_location=end_location;
209 if(i_it->is_goto() && i_it->get_target()->is_end_function())
210 i_it->set_target(a_end);
215 f.body.destructive_append(tmp_end_function);
218 f.update_instructions_function(identifier);
241 const unsigned errors_before=
253 goto_convert_functions.
error();
261 catch(
const std::string &e)
276 const unsigned errors_before=
289 goto_convert_functions.
error();
297 catch(
const std::string &e)
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 generic 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.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
This class represents an instruction in the GOTO intermediate representation.
const irep_idt & id() const
void compute_location_numbers()
std::string tmp_symbol_prefix
instructionst::iterator targett
const source_locationt & find_source_location() const
source_locationt source_location
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)
::goto_functiont goto_functiont
A side effect that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
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.
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
goto_programt & goto_program
#define Forall_goto_program_instructions(it, program)
const codet & to_code(const exprt &expr)
const code_blockt & to_code_block(const codet &code)
goto_programt coverage_criteriont message_handlert & message_handler
A statement in a programming language.
void add_return(goto_functionst::goto_functiont &, const source_locationt &)
#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 namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)