12 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H 13 #define CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H 16 #include <unordered_set> 23 typedef std::unordered_set<irep_idt, irep_id_hash>
id_sett;
24 typedef std::map<goto_programt::const_targett, goto_programt::const_targett>
26 typedef std::unordered_map<irep_idt, unsigned, irep_id_hash>
dead_mapt;
27 typedef std::list<std::pair<goto_programt::const_targett, bool> >
57 std::set<std::string> &_system_headers):
70 for(id_listt::const_iterator
107 const exprt &
function,
180 const exprt &switch_var,
189 std::set<unsigned> &processed_locations);
225 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H const goto_programt & goto_program
The type of an expression.
goto_programt::const_targett convert_do_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, codet &dest)
goto_programt::const_targett convert_instruction(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_goto_switch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
bool remove_default(const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
void convert_assign_rec(const code_assignt &assign, codet &dest)
caset(const goto_programt &goto_program, const exprt &v, goto_programt::const_targett sel, goto_programt::const_targett st)
std::map< goto_programt::const_targett, goto_programt::const_targett > loopt
void convert_labels(goto_programt::const_targett target, codet &dest)
goto_programt::const_targett convert_assign(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_start_thread(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_goto_if(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_goto_goto(goto_programt::const_targett target, codet &dest)
exprt::operandst argumentst
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const id_sett & typedef_names
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
loop_last_stackt loop_last_stack
instructionst::const_iterator const_targett
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
void cleanup_code(codet &code, const irep_idt parent_stmt)
void add_local_types(const typet &type)
goto_programt::const_targett convert_goto_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, codet &dest)
goto_programt::const_targett convert_assign_varargs(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
void cleanup_expr(exprt &expr, bool no_typecast)
std::unordered_set< irep_idt, irep_id_hash > id_sett
std::set< std::string > & system_headers
std::list< irep_idt > id_listt
bool set_block_end_points(goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
goto_program2codet(const irep_idt &identifier, const goto_programt &_goto_program, symbol_tablet &_symbol_table, code_blockt &_dest, id_listt &_local_static, id_listt &_type_names, const id_sett &_typedef_names, std::set< std::string > &_system_headers)
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
code_blockt & toplevel_block
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
goto_programt::const_targett convert_return(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const irep_idt & func_name
goto_programt::const_targett get_cases(goto_programt::const_targett target, goto_programt::const_targett upper_bound, const exprt &switch_var, cases_listt &cases, goto_programt::const_targett &first_target, goto_programt::const_targett &default_target)
goto_programt::const_targett convert_throw(goto_programt::const_targett target, codet &dest)
std::list< std::pair< goto_programt::const_targett, bool > > loop_last_stackt
Base class for all expressions.
goto_programt::const_targett case_selector
goto_programt::const_targett case_start
std::unordered_map< irep_idt, unsigned, irep_id_hash > dead_mapt
Compute natural loops in a goto_function.
A statement in a programming language.
std::list< caset > cases_listt
goto_programt::const_targett convert_goto(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
void remove_const(typet &type)
std::unordered_set< exprt, irep_hash > va_list_expr
symbol_tablet & symbol_table
goto_programt::const_targett case_last
void cleanup_code_block(codet &code, const irep_idt parent_stmt)