39 typedef std::list<irep_idt> symbol_listt;
40 symbol_listt symbol_list;
44 if(!it->second.is_type &&
45 !it->second.is_macro &&
46 it->second.type.id()==ID_code &&
47 (it->second.mode==ID_C ||
48 it->second.mode==ID_cpp ||
49 it->second.mode==ID_java ||
50 it->second.mode==
"jsil"))
51 symbol_list.push_back(it->first);
54 for(
const auto &
id : symbol_list)
65 if(!it->second.is_type &&
66 it->second.type.id()==ID_code &&
67 it->second.value.is_not_nil())
68 it->second.value=
codet();
77 for(
const auto &label : i_it->labels)
78 if(label==
"__CPROVER_HIDE")
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;
148 if(f.body_available())
158 error() <<
"got invalid code for function `" << identifier <<
"'" 175 end_function->source_location=end_location;
176 end_function->code.
set(ID_identifier, identifier);
181 f.type.return_type().id()!=ID_empty &&
182 f.type.return_type().id()!=ID_constructor &&
183 f.type.return_type().id()!=ID_destructor;
192 if(!f.body.instructions.empty() &&
195 goto_programt::instructiont a_begin;
196 a_begin.make_atomic_begin();
197 a_begin.source_location=f.body.instructions.front().source_location;
198 f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
201 a_end->make_atomic_end();
202 a_end->source_location=end_location;
206 if(i_it->is_goto() && i_it->get_target()->is_end_function())
207 i_it->set_target(a_end);
212 f.body.destructive_append(tmp_end_function);
216 i_it->function=identifier;
238 const unsigned errors_before=
242 symbol_table, functions, message_handler);
251 goto_convert_functions.
error();
259 catch(
const std::string &e)
274 const unsigned errors_before=
278 symbol_table, functions, message_handler);
287 goto_convert_functions.
error();
295 catch(
const std::string &e)
const irep_idt & get_statement() const
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
symbol_tablet & symbol_table
#define forall_symbols(it, expr)
struct goto_convertt::targetst targets
source_locationt end_location() const
exprt value
Initial value of symbol.
symbol_tablet 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)
#define Forall_symbols(it, expr)
const irep_idt & id() const
instructionst::const_iterator const_targett
std::string tmp_symbol_prefix
void compute_location_numbers()
const source_locationt & find_source_location() const
source_locationt source_location
goto_functionst & functions
A side effect that returns a non-deterministically chosen value.
goto_function_templatet< goto_programt > goto_functiont
function_mapt function_map
void goto_convert_rec(const codet &code, goto_programt &dest)
bool has_prefix(const std::string &s, const std::string &prefix)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
void goto_convert(symbol_tablet &symbol_table, goto_modelt &goto_model, message_handlert &message_handler)
Goto Programs with Functions.
static bool hide(const goto_programt &goto_program)
goto_convert_functionst(symbol_tablet &_symbol_table, goto_functionst &_functions, message_handlert &_message_handler)
virtual ~goto_convert_functionst()
unsigned temporary_counter
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
#define Forall_goto_program_instructions(it, program)
const codet & to_code(const exprt &expr)
const code_blockt & to_code_block(const codet &code)
void swap(symbol_tablet &other)
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)
void convert_function(const irep_idt &identifier)
goto_functionst goto_functions
void set(const irep_namet &name, const irep_idt &value)
instructionst::iterator targett
unsigned get_message_count(unsigned level) const