cprover
goto_convertt Class Reference

#include <goto_convert_class.h>

Inheritance diagram for goto_convertt:
[legend]
Collaboration diagram for goto_convertt:
[legend]

Classes

struct  break_continue_targetst
 
struct  break_switch_targetst
 
struct  leave_targett
 
struct  targetst
 
struct  throw_targett
 

Public Member Functions

void goto_convert (const codet &code, goto_programt &dest, const irep_idt &mode)
 
 goto_convertt (symbol_table_baset &_symbol_table, message_handlert &_message_handler)
 
virtual ~goto_convertt ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Protected Types

typedef std::vector< codetdestructor_stackt
 
typedef std::map< irep_idt, std::pair< goto_programt::targett, destructor_stackt > > labelst
 
typedef std::list< std::pair< goto_programt::targett, destructor_stackt > > gotost
 
typedef std::list< goto_programt::targettcomputed_gotost
 
typedef exprt::operandst caset
 
typedef std::list< std::pair< goto_programt::targett, caset > > casest
 
typedef std::map< goto_programt::targett, casest::iterator > cases_mapt
 

Protected Member Functions

void goto_convert_rec (const codet &code, goto_programt &dest, const irep_idt &mode)
 
symboltnew_tmp_symbol (const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
 
symbol_exprt make_compound_literal (const exprt &expr, goto_programt &dest, const irep_idt &mode)
 
void clean_expr (exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
 
void clean_expr_address_of (exprt &expr, goto_programt &dest, const irep_idt &mode)
 
void make_temp_symbol (exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
 
void rewrite_boolean (exprt &dest)
 re-write boolean operators into ?: More...
 
void remove_side_effect (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
 
void remove_assignment (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
 
void remove_pre (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
 
void remove_post (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
 
void remove_function_call (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
 
void remove_cpp_new (side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
 
void remove_cpp_delete (side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
 
void remove_malloc (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
 
void remove_temporary_object (side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
 
void remove_statement_expression (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
 
void remove_gcc_conditional_expression (exprt &expr, goto_programt &dest, const irep_idt &mode)
 
virtual void do_cpp_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
 
void do_java_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
 
void do_java_new_array (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
 
void cpp_new_initializer (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
 builds a goto program for object initialization after new More...
 
virtual void do_function_call (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 
virtual void do_function_call_if (const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 
virtual void do_function_call_symbol (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 add function calls to function queue for later processing More...
 
virtual void do_function_call_symbol (const symbolt &symbol)
 
virtual void do_function_call_other (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void convert_block (const code_blockt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_decl (const code_declt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_decl_type (const codet &code, goto_programt &dest)
 
void convert_expression (const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
 
void convert_assign (const code_assignt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_cpp_delete (const codet &code, goto_programt &dest)
 
void convert_loop_invariant (const codet &code, goto_programt::targett loop, const irep_idt &mode)
 
void convert_for (const code_fort &code, goto_programt &dest, const irep_idt &mode)
 
void convert_while (const code_whilet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_dowhile (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_assume (const code_assumet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_assert (const code_assertt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_switch (const code_switcht &code, goto_programt &dest, const irep_idt &mode)
 
void convert_break (const code_breakt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_return (const code_returnt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_continue (const code_continuet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_ifthenelse (const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
 
void convert_init (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_goto (const code_gotot &code, goto_programt &dest)
 
void convert_gcc_computed_goto (const codet &code, goto_programt &dest)
 
void convert_skip (const codet &code, goto_programt &dest)
 
void convert_label (const code_labelt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_gcc_local_label (const codet &code, goto_programt &dest)
 
void convert_switch_case (const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
 
void convert_gcc_switch_case_range (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_function_call (const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
 
void convert_start_thread (const codet &code, goto_programt &dest)
 
void convert_end_thread (const codet &code, goto_programt &dest)
 
void convert_atomic_begin (const codet &code, goto_programt &dest)
 
void convert_atomic_end (const codet &code, goto_programt &dest)
 
void convert_msc_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_msc_try_except (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_msc_leave (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_CPROVER_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_CPROVER_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_CPROVER_throw (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void convert_asm (const code_asmt &code, goto_programt &dest)
 
void convert (const codet &code, goto_programt &dest, const irep_idt &mode)
 converts 'code' and appends the result to 'dest' More...
 
void copy (const codet &code, goto_program_instruction_typet type, goto_programt &dest)
 
symbol_exprt exception_flag ()
 
void unwind_destructor_stack (const source_locationt &, std::size_t stack_size, goto_programt &dest, const irep_idt &mode)
 
void unwind_destructor_stack (const source_locationt &, std::size_t stack_size, goto_programt &dest, destructor_stackt &stack, const irep_idt &mode)
 
void finish_gotos (goto_programt &dest, const irep_idt &mode)
 
void finish_computed_gotos (goto_programt &dest)
 
void optimize_guarded_gotos (goto_programt &dest)
 Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a branch target. More...
 
exprt case_guard (const exprt &value, const caset &case_op)
 
void generate_ifthenelse (const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
 if(guard) true_case; else false_case; More...
 
void generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
 if(guard) goto target_true; else goto target_false; More...
 
void generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, const source_locationt &, goto_programt &dest, const irep_idt &mode)
 
void generate_thread_block (const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
 Generates the necessary goto-instructions to represent a thread-block. More...
 
irep_idt get_string_constant (const exprt &expr)
 
bool get_string_constant (const exprt &expr, irep_idt &)
 
exprt get_constant (const exprt &expr)
 
void do_atomic_begin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void do_atomic_end (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void do_create_thread (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void do_array_equal (const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
 
void do_array_op (const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void do_printf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void do_scanf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void do_input (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
 
void do_output (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
 
void do_prob_coin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void do_prob_uniform (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
exprt get_array_argument (const exprt &src)
 

Static Protected Member Functions

static bool needs_cleaning (const exprt &expr)
 
static bool has_sideeffect (const exprt &expr)
 
static bool has_function_call (const exprt &expr)
 
static void replace_new_object (const exprt &object, exprt &dest)
 
static void collect_operands (const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
 

Protected Attributes

symbol_table_basetsymbol_table
 
namespacet ns
 
std::string tmp_symbol_prefix
 
struct goto_convertt::targetst targets
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 26 of file goto_convert_class.h.

Member Typedef Documentation

◆ cases_mapt

typedef std::map<goto_programt::targett, casest::iterator> goto_convertt::cases_mapt
protected

Definition at line 367 of file goto_convert_class.h.

◆ casest

typedef std::list<std::pair<goto_programt::targett, caset> > goto_convertt::casest
protected

Definition at line 366 of file goto_convert_class.h.

◆ caset

Definition at line 365 of file goto_convert_class.h.

◆ computed_gotost

Definition at line 364 of file goto_convert_class.h.

◆ destructor_stackt

typedef std::vector<codet> goto_convertt::destructor_stackt
protected

Definition at line 336 of file goto_convert_class.h.

◆ gotost

typedef std::list<std::pair<goto_programt::targett, destructor_stackt> > goto_convertt::gotost
protected

Definition at line 363 of file goto_convert_class.h.

◆ labelst

typedef std::map<irep_idt, std::pair<goto_programt::targett, destructor_stackt> > goto_convertt::labelst
protected

Definition at line 361 of file goto_convert_class.h.

Constructor & Destructor Documentation

◆ goto_convertt()

goto_convertt::goto_convertt ( symbol_table_baset _symbol_table,
message_handlert _message_handler 
)
inline

Definition at line 32 of file goto_convert_class.h.

◆ ~goto_convertt()

virtual goto_convertt::~goto_convertt ( )
inlinevirtual

Definition at line 42 of file goto_convert_class.h.

Member Function Documentation

◆ case_guard()

exprt goto_convertt::case_guard ( const exprt value,
const caset case_op 
)
protected

◆ clean_expr()

void goto_convertt::clean_expr ( exprt expr,
goto_programt dest,
const irep_idt mode,
bool  result_is_used = true 
)
protected

◆ clean_expr_address_of()

void goto_convertt::clean_expr_address_of ( exprt expr,
goto_programt dest,
const irep_idt mode 
)
protected

◆ collect_operands()

void goto_convertt::collect_operands ( const exprt expr,
const irep_idt id,
std::list< exprt > &  dest 
)
staticprotected

Definition at line 1589 of file goto_convert.cpp.

References forall_operands, and irept::id().

Referenced by generate_conditional_branch().

◆ convert()

void goto_convertt::convert ( const codet code,
goto_programt dest,
const irep_idt mode 
)
protected

converts 'code' and appends the result to 'dest'

Definition at line 447 of file goto_convert.cpp.

References goto_programt::add_instruction(), CATCH, convert_asm(), convert_assert(), convert_assign(), convert_assume(), convert_atomic_begin(), convert_atomic_end(), convert_block(), convert_break(), convert_continue(), convert_cpp_delete(), convert_CPROVER_throw(), convert_CPROVER_try_catch(), convert_CPROVER_try_finally(), convert_decl(), convert_decl_type(), convert_dowhile(), convert_end_thread(), convert_expression(), convert_for(), convert_function_call(), convert_gcc_computed_goto(), convert_gcc_local_label(), convert_gcc_switch_case_range(), convert_goto(), convert_ifthenelse(), convert_init(), convert_label(), convert_msc_leave(), convert_msc_try_except(), convert_msc_try_finally(), convert_return(), convert_skip(), convert_start_thread(), convert_switch(), convert_switch_case(), convert_try_catch(), convert_while(), copy(), DEAD, messaget::eom(), messaget::error(), exprt::find_source_location(), forall_operands, codet::get_statement(), get_string_constant(), goto_programt::instructions, exprt::make_typecast(), ns, exprt::op0(), exprt::op1(), exprt::operands(), OTHER, simplify(), SKIP, exprt::source_location(), messaget::mstreamt::source_location, to_code(), to_code_asm(), to_code_assert(), to_code_assign(), to_code_assume(), to_code_block(), to_code_break(), to_code_continue(), to_code_decl(), to_code_expression(), to_code_for(), to_code_function_call(), to_code_goto(), to_code_ifthenelse(), to_code_label(), to_code_return(), to_code_switch(), to_code_switch_case(), and to_code_while().

Referenced by clean_expr(), clean_expr_address_of(), convert_block(), convert_cpp_delete(), convert_CPROVER_try_catch(), convert_CPROVER_try_finally(), convert_dowhile(), convert_for(), convert_gcc_switch_case_range(), convert_ifthenelse(), convert_init(), convert_label(), convert_msc_leave(), convert_msc_try_except(), convert_msc_try_finally(), convert_switch(), convert_switch_case(), convert_try_catch(), convert_while(), cpp_new_initializer(), do_cpp_new(), generate_thread_block(), goto_convert_rec(), make_compound_literal(), make_temp_symbol(), remove_assignment(), remove_cpp_new(), remove_malloc(), remove_post(), remove_pre(), remove_statement_expression(), remove_temporary_object(), and unwind_destructor_stack().

◆ convert_asm()

void goto_convertt::convert_asm ( const code_asmt code,
goto_programt dest 
)
protected

Definition at line 14 of file goto_asm.cpp.

References copy(), and OTHER.

Referenced by convert().

◆ convert_assert()

void goto_convertt::convert_assert ( const code_assertt code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ convert_assign()

◆ convert_assume()

void goto_convertt::convert_assume ( const code_assumet code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ convert_atomic_begin()

void goto_convertt::convert_atomic_begin ( const codet code,
goto_programt dest 
)
protected

◆ convert_atomic_end()

void goto_convertt::convert_atomic_end ( const codet code,
goto_programt dest 
)
protected

◆ convert_block()

void goto_convertt::convert_block ( const code_blockt code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ convert_break()

◆ convert_continue()

◆ convert_cpp_delete()

◆ convert_CPROVER_throw()

◆ convert_CPROVER_try_catch()

◆ convert_CPROVER_try_finally()

void goto_convertt::convert_CPROVER_try_finally ( const codet code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ convert_decl()

◆ convert_decl_type()

void goto_convertt::convert_decl_type ( const codet code,
goto_programt dest 
)
protected

Definition at line 717 of file goto_convert.cpp.

Referenced by convert().

◆ convert_dowhile()

◆ convert_end_thread()

void goto_convertt::convert_end_thread ( const codet code,
goto_programt dest 
)
protected

◆ convert_expression()

◆ convert_for()

◆ convert_function_call()

void goto_convertt::convert_function_call ( const code_function_callt code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ convert_gcc_computed_goto()

void goto_convertt::convert_gcc_computed_goto ( const codet code,
goto_programt dest 
)
protected

◆ convert_gcc_local_label()

void goto_convertt::convert_gcc_local_label ( const codet code,
goto_programt dest 
)
protected

Definition at line 357 of file goto_convert.cpp.

Referenced by convert().

◆ convert_gcc_switch_case_range()

◆ convert_goto()

void goto_convertt::convert_goto ( const code_gotot code,
goto_programt dest 
)
protected

◆ convert_ifthenelse()

◆ convert_init()

void goto_convertt::convert_init ( const codet code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ convert_label()

◆ convert_loop_invariant()

void goto_convertt::convert_loop_invariant ( const codet code,
goto_programt::targett  loop,
const irep_idt mode 
)
protected

◆ convert_msc_leave()

◆ convert_msc_try_except()

void goto_convertt::convert_msc_try_except ( const codet code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ convert_msc_try_finally()

◆ convert_return()

◆ convert_skip()

void goto_convertt::convert_skip ( const codet code,
goto_programt dest 
)
protected

Definition at line 927 of file goto_convert.cpp.

References goto_programt::add_instruction(), SKIP, and exprt::source_location().

Referenced by convert().

◆ convert_start_thread()

void goto_convertt::convert_start_thread ( const codet code,
goto_programt dest 
)
protected

◆ convert_switch()

◆ convert_switch_case()

◆ convert_try_catch()

◆ convert_while()

◆ copy()

◆ cpp_new_initializer()

void goto_convertt::cpp_new_initializer ( const exprt lhs,
const side_effect_exprt rhs,
goto_programt dest 
)
protected

builds a goto program for object initialization after new

Definition at line 533 of file builtin_functions.cpp.

References convert(), irept::find(), side_effect_exprt::get_statement(), irept::is_not_nil(), replace_new_object(), typet::subtype(), to_code(), exprt::type(), and UNREACHABLE.

Referenced by do_cpp_new().

◆ do_array_equal()

void goto_convertt::do_array_equal ( const exprt lhs,
const symbol_exprt rhs,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_array_op()

void goto_convertt::do_array_op ( const irep_idt id,
const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_atomic_begin()

void goto_convertt::do_atomic_begin ( const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_atomic_end()

void goto_convertt::do_atomic_end ( const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_cpp_new()

◆ do_create_thread()

void goto_convertt::do_create_thread ( const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_function_call()

◆ do_function_call_if()

void goto_convertt::do_function_call_if ( const exprt lhs,
const if_exprt function,
const exprt::operandst arguments,
goto_programt dest,
const irep_idt mode 
)
protectedvirtual

◆ do_function_call_other()

void goto_convertt::do_function_call_other ( const exprt lhs,
const exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protectedvirtual

◆ do_function_call_symbol() [1/2]

void goto_convertt::do_function_call_symbol ( const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protectedvirtual

◆ do_function_call_symbol() [2/2]

virtual void goto_convertt::do_function_call_symbol ( const symbolt symbol)
inlineprotectedvirtual

Definition at line 198 of file goto_convert_class.h.

◆ do_input()

void goto_convertt::do_input ( const exprt lhs,
const exprt rhs,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_java_new()

void goto_convertt::do_java_new ( const exprt lhs,
const side_effect_exprt rhs,
goto_programt dest 
)
protected

◆ do_java_new_array()

void goto_convertt::do_java_new_array ( const exprt lhs,
const side_effect_exprt rhs,
goto_programt dest 
)
protected

◆ do_output()

void goto_convertt::do_output ( const exprt lhs,
const exprt rhs,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_printf()

void goto_convertt::do_printf ( const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_prob_coin()

void goto_convertt::do_prob_coin ( const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_prob_uniform()

void goto_convertt::do_prob_uniform ( const exprt lhs,
const symbol_exprt function,
const exprt::operandst arguments,
goto_programt dest 
)
protected

◆ do_scanf()

◆ exception_flag()

◆ finish_computed_gotos()

◆ finish_gotos()

◆ generate_conditional_branch() [1/2]

void goto_convertt::generate_conditional_branch ( const exprt guard,
goto_programt::targett  target_true,
goto_programt::targett  target_false,
const source_locationt source_location,
goto_programt dest,
const irep_idt mode 
)
protected

◆ generate_conditional_branch() [2/2]

void goto_convertt::generate_conditional_branch ( const exprt guard,
goto_programt::targett  target_true,
const source_locationt source_location,
goto_programt dest,
const irep_idt mode 
)
protected

◆ generate_ifthenelse()

void goto_convertt::generate_ifthenelse ( const exprt cond,
goto_programt true_case,
goto_programt false_case,
const source_locationt source_location,
goto_programt dest,
const irep_idt mode 
)
protected

◆ generate_thread_block()

void goto_convertt::generate_thread_block ( const code_blockt thread_body,
goto_programt dest,
const irep_idt mode 
)
protected

Generates the necessary goto-instructions to represent a thread-block.

Specifically, the following instructions are generated:

A: START_THREAD : C B: GOTO Z C: SKIP D: {THREAD BODY} E: END_THREAD Z: SKIP

Parameters
thread_bodysequence of codet's that can be executed in parallel.
[out]destresulting goto-instructions.

Definition at line 2089 of file goto_convert.cpp.

References goto_programt::add_instruction(), convert(), goto_programt::destructive_append(), END_THREAD, exprt::source_location(), and START_THREAD.

Referenced by convert_label().

◆ get_array_argument()

◆ get_constant()

exprt goto_convertt::get_constant ( const exprt expr)
protected

◆ get_string_constant() [1/2]

◆ get_string_constant() [2/2]

◆ goto_convert()

void goto_convertt::goto_convert ( const codet code,
goto_programt dest,
const irep_idt mode 
)

Definition at line 280 of file goto_convert.cpp.

References goto_convert_rec().

◆ goto_convert_rec()

void goto_convertt::goto_convert_rec ( const codet code,
goto_programt dest,
const irep_idt mode 
)
protected

◆ has_function_call()

bool goto_convertt::has_function_call ( const exprt expr)
staticprotected

Definition at line 23 of file goto_convert_side_effect.cpp.

References forall_operands, irept::get(), and irept::id().

◆ has_sideeffect()

static bool goto_convertt::has_sideeffect ( const exprt expr)
staticprotected

◆ make_compound_literal()

◆ make_temp_symbol()

void goto_convertt::make_temp_symbol ( exprt expr,
const std::string &  suffix,
goto_programt dest,
const irep_idt mode 
)
protected

◆ needs_cleaning()

bool goto_convertt::needs_cleaning ( const exprt expr)
staticprotected

◆ new_tmp_symbol()

symbolt & goto_convertt::new_tmp_symbol ( const typet type,
const std::string &  suffix,
goto_programt dest,
const source_locationt source_location,
const irep_idt mode 
)
protected

◆ optimize_guarded_gotos()

void goto_convertt::optimize_guarded_gotos ( goto_programt dest)
protected

Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a branch target.

parameters: Destination goto program

Definition at line 238 of file goto_convert.cpp.

References boolean_negate(), goto_programt::instructions, and goto_programt::instructiont::nil_target.

Referenced by goto_convert_rec().

◆ remove_assignment()

◆ remove_cpp_delete()

void goto_convertt::remove_cpp_delete ( side_effect_exprt expr,
goto_programt dest,
bool  result_is_used 
)
protected

◆ remove_cpp_new()

◆ remove_function_call()

◆ remove_gcc_conditional_expression()

◆ remove_malloc()

void goto_convertt::remove_malloc ( side_effect_exprt expr,
goto_programt dest,
const irep_idt mode,
bool  result_is_used 
)
protected

◆ remove_post()

◆ remove_pre()

◆ remove_side_effect()

◆ remove_statement_expression()

◆ remove_temporary_object()

◆ replace_new_object()

void goto_convertt::replace_new_object ( const exprt object,
exprt dest 
)
staticprotected

◆ rewrite_boolean()

void goto_convertt::rewrite_boolean ( exprt dest)
protected

◆ unwind_destructor_stack() [1/2]

void goto_convertt::unwind_destructor_stack ( const source_locationt source_location,
std::size_t  stack_size,
goto_programt dest,
const irep_idt mode 
)
protected

◆ unwind_destructor_stack() [2/2]

void goto_convertt::unwind_destructor_stack ( const source_locationt source_location,
std::size_t  stack_size,
goto_programt dest,
destructor_stackt stack,
const irep_idt mode 
)
protected

Definition at line 290 of file goto_convert_exceptions.cpp.

References exprt::add_source_location(), and convert().

Member Data Documentation

◆ ns

◆ symbol_table

◆ targets

◆ tmp_symbol_prefix

std::string goto_convertt::tmp_symbol_prefix
protected

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