cprover
goto_program2codet Class Reference

#include <goto_program2code.h>

Collaboration diagram for goto_program2codet:
[legend]

Classes

struct  caset
 

Public Member Functions

 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 operator() ()
 

Protected Member Functions

void build_loop_map ()
 
void build_dead_map ()
 
void scan_for_varargs ()
 
void cleanup_code (codet &code, const irep_idt parent_stmt)
 
void cleanup_function_call (const exprt &function, code_function_callt::argumentst &arguments)
 
void cleanup_code_block (codet &code, const irep_idt parent_stmt)
 
void cleanup_code_ifthenelse (codet &code, const irep_idt parent_stmt)
 
void cleanup_expr (exprt &expr, bool no_typecast)
 
void add_local_types (const typet &type)
 
void remove_const (typet &type)
 
goto_programt::const_targett convert_instruction (goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
 
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_assign_varargs (goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
 
void convert_assign_rec (const code_assignt &assign, codet &dest)
 
goto_programt::const_targett convert_return (goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
 
goto_programt::const_targett convert_decl (goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
 
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_goto (goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
 
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_goto_switch (goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
 
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)
 
bool set_block_end_points (goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
 
bool remove_default (const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
 
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_break_continue (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)
 
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_throw (goto_programt::const_targett target, codet &dest)
 
goto_programt::const_targett convert_catch (goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
 

Protected Attributes

const irep_idtfunc_name
 
const goto_programtgoto_program
 
symbol_tabletsymbol_table
 
const namespacet ns
 
code_blockttoplevel_block
 
id_listtlocal_static
 
id_listttype_names
 
const id_setttypedef_names
 
std::set< std::string > & system_headers
 
std::unordered_set< exprt, irep_hashva_list_expr
 
natural_loopst loops
 
loopt loop_map
 
id_sett labels_in_use
 
dead_mapt dead_map
 
loop_last_stackt loop_last_stack
 
id_sett local_static_set
 
id_sett type_names_set
 
id_sett const_removed
 

Private Types

typedef std::list< irep_idtid_listt
 
typedef std::unordered_set< irep_idt, irep_id_hashid_sett
 
typedef std::map< goto_programt::const_targett, goto_programt::const_targettloopt
 
typedef std::unordered_map< irep_idt, unsigned, irep_id_hashdead_mapt
 
typedef std::list< std::pair< goto_programt::const_targett, bool > > loop_last_stackt
 
typedef std::list< casetcases_listt
 

Detailed Description

Definition at line 20 of file goto_program2code.h.

Member Typedef Documentation

§ cases_listt

typedef std::list<caset> goto_program2codet::cases_listt
private

Definition at line 46 of file goto_program2code.h.

§ dead_mapt

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> goto_program2codet::dead_mapt
private

Definition at line 26 of file goto_program2code.h.

§ id_listt

typedef std::list<irep_idt> goto_program2codet::id_listt
private

Definition at line 22 of file goto_program2code.h.

§ id_sett

typedef std::unordered_set<irep_idt, irep_id_hash> goto_program2codet::id_sett
private

Definition at line 23 of file goto_program2code.h.

§ loop_last_stackt

typedef std::list<std::pair<goto_programt::const_targett, bool> > goto_program2codet::loop_last_stackt
private

Definition at line 28 of file goto_program2code.h.

§ loopt

Constructor & Destructor Documentation

§ goto_program2codet()

goto_program2codet::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 
)
inline

Definition at line 49 of file goto_program2code.h.

References local_static, operator()(), type_names, and type_names_set.

Member Function Documentation

§ add_local_types()

§ build_dead_map()

void goto_program2codet::build_dead_map ( )
protected

§ build_loop_map()

void goto_program2codet::build_loop_map ( )
protected

Definition at line 59 of file goto_program2code.cpp.

References goto_program, natural_loops_templatet< P, T >::loop_map, loop_map, and loops.

Referenced by operator()().

§ cleanup_code()

§ cleanup_code_block()

void goto_program2codet::cleanup_code_block ( codet code,
const irep_idt  parent_stmt 
)
protected

§ cleanup_code_ifthenelse()

§ cleanup_expr()

§ cleanup_function_call()

void goto_program2codet::cleanup_function_call ( const exprt function,
code_function_callt::argumentst arguments 
)
protected

§ convert_assign()

goto_programt::const_targett goto_program2codet::convert_assign ( goto_programt::const_targett  target,
goto_programt::const_targett  upper_bound,
codet dest 
)
protected

§ convert_assign_rec()

void goto_program2codet::convert_assign_rec ( const code_assignt assign,
codet dest 
)
protected

§ convert_assign_varargs()

§ convert_catch()

goto_programt::const_targett goto_program2codet::convert_catch ( goto_programt::const_targett  target,
goto_programt::const_targett  upper_bound,
codet dest 
)
protected

Definition at line 1423 of file goto_program2code.cpp.

Referenced by convert_instruction().

§ convert_decl()

§ convert_do_while()

goto_programt::const_targett goto_program2codet::convert_do_while ( goto_programt::const_targett  target,
goto_programt::const_targett  loop_end,
codet dest 
)
protected

§ convert_goto()

§ convert_goto_break_continue()

§ convert_goto_goto()

§ convert_goto_if()

§ convert_goto_switch()

§ convert_goto_while()

§ convert_instruction()

§ convert_labels()

§ convert_return()

§ convert_start_thread()

§ convert_throw()

goto_programt::const_targett goto_program2codet::convert_throw ( goto_programt::const_targett  target,
codet dest 
)
protected

Definition at line 1414 of file goto_program2code.cpp.

Referenced by convert_instruction().

§ get_cases()

§ operator()()

§ remove_const()

§ remove_default()

bool goto_program2codet::remove_default ( const cfg_dominatorst dominators,
const cases_listt cases,
goto_programt::const_targett  default_target 
)
protected

§ scan_for_varargs()

§ set_block_end_points()

bool goto_program2codet::set_block_end_points ( goto_programt::const_targett  upper_bound,
const cfg_dominatorst dominators,
cases_listt cases,
std::set< unsigned > &  processed_locations 
)
protected

Member Data Documentation

§ const_removed

id_sett goto_program2codet::const_removed
protected

Definition at line 98 of file goto_program2code.h.

Referenced by remove_const().

§ dead_map

dead_mapt goto_program2codet::dead_map
protected

Definition at line 94 of file goto_program2code.h.

Referenced by build_dead_map(), and convert_decl().

§ func_name

const irep_idt& goto_program2codet::func_name
protected

Definition at line 80 of file goto_program2code.h.

Referenced by scan_for_varargs().

§ goto_program

§ labels_in_use

id_sett goto_program2codet::labels_in_use
protected

§ local_static

id_listt& goto_program2codet::local_static
protected

Definition at line 85 of file goto_program2code.h.

Referenced by cleanup_expr(), and goto_program2codet().

§ local_static_set

id_sett goto_program2codet::local_static_set
protected

Definition at line 96 of file goto_program2code.h.

Referenced by cleanup_expr().

§ loop_last_stack

loop_last_stackt goto_program2codet::loop_last_stack
protected

§ loop_map

loopt goto_program2codet::loop_map
protected

Definition at line 92 of file goto_program2code.h.

Referenced by build_loop_map(), convert_goto(), and convert_instruction().

§ loops

natural_loopst goto_program2codet::loops
protected

§ ns

§ symbol_table

symbol_tablet& goto_program2codet::symbol_table
protected

Definition at line 82 of file goto_program2code.h.

Referenced by cleanup_expr(), remove_const(), and scan_for_varargs().

§ system_headers

std::set<std::string>& goto_program2codet::system_headers
protected

§ toplevel_block

code_blockt& goto_program2codet::toplevel_block
protected

Definition at line 84 of file goto_program2code.h.

Referenced by convert_decl(), convert_goto_switch(), and operator()().

§ type_names

id_listt& goto_program2codet::type_names
protected

Definition at line 86 of file goto_program2code.h.

Referenced by add_local_types(), and goto_program2codet().

§ type_names_set

id_sett goto_program2codet::type_names_set
protected

Definition at line 97 of file goto_program2code.h.

Referenced by add_local_types(), and goto_program2codet().

§ typedef_names

const id_sett& goto_program2codet::typedef_names
protected

Definition at line 87 of file goto_program2code.h.

Referenced by cleanup_code(), and cleanup_expr().

§ va_list_expr

std::unordered_set<exprt, irep_hash> goto_program2codet::va_list_expr
protected

Definition at line 89 of file goto_program2code.h.

Referenced by cleanup_code(), convert_assign(), convert_decl(), and scan_for_varargs().


The documentation for this class was generated from the following files: