cprover
goto_convertt Class Reference

#include <goto_convert_class.h>

+ Inheritance diagram for goto_convertt:
+ Collaboration diagram for goto_convertt:

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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Protected Types

typedef std::map< irep_idt, std::pair< goto_programt::targett, node_indext > > labelst
 
typedef std::list< std::pair< goto_programt::targett, node_indext > > 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)
 
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)
 
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 &)
 
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 code_dowhilet &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_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 code_gcc_switch_case_ranget &, 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 (const irep_idt &mode)
 
void unwind_destructor_stack (const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={})
 Unwinds the destructor stack and creates destructors for each node between destructor_start_point and destructor_end_point (including the start, excluding the end). More...
 
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 &rhs, const exprt::operandst &arguments, goto_programt &dest)
 
void do_output (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
 
lifetimet lifetime = lifetimet::STATIC_GLOBAL
 
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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Definition at line 28 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 362 of file goto_convert_class.h.

◆ casest

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

Definition at line 361 of file goto_convert_class.h.

◆ caset

Definition at line 360 of file goto_convert_class.h.

◆ computed_gotost

Definition at line 359 of file goto_convert_class.h.

◆ gotost

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

Definition at line 358 of file goto_convert_class.h.

◆ labelst

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

Definition at line 356 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 34 of file goto_convert_class.h.

◆ ~goto_convertt()

virtual goto_convertt::~goto_convertt ( )
inlinevirtual

Definition at line 44 of file goto_convert_class.h.

Member Function Documentation

◆ case_guard()

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

Definition at line 1088 of file goto_convert.cpp.

◆ clean_expr()

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

Definition at line 161 of file goto_clean_expr.cpp.

◆ clean_expr_address_of()

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

Definition at line 430 of file goto_clean_expr.cpp.

◆ collect_operands()

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

Definition at line 1419 of file goto_convert.cpp.

◆ 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 427 of file goto_convert.cpp.

◆ convert_asm()

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

Definition at line 14 of file goto_asm.cpp.

◆ convert_assert()

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

Definition at line 811 of file goto_convert.cpp.

◆ convert_assign()

void goto_convertt::convert_assign ( const code_assignt code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 673 of file goto_convert.cpp.

◆ convert_assume()

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

Definition at line 835 of file goto_convert.cpp.

◆ convert_atomic_begin()

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

Definition at line 1352 of file goto_convert.cpp.

◆ convert_atomic_end()

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

Definition at line 1364 of file goto_convert.cpp.

◆ convert_block()

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

Definition at line 540 of file goto_convert.cpp.

◆ convert_break()

void goto_convertt::convert_break ( const code_breakt code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 1208 of file goto_convert.cpp.

◆ convert_continue()

void goto_convertt::convert_continue ( const code_continuet code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 1284 of file goto_convert.cpp.

◆ convert_cpp_delete()

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

Definition at line 749 of file goto_convert.cpp.

◆ convert_CPROVER_throw()

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

Definition at line 180 of file goto_convert_exceptions.cpp.

◆ convert_CPROVER_try_catch()

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

Definition at line 144 of file goto_convert_exceptions.cpp.

◆ convert_CPROVER_try_finally()

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

Definition at line 211 of file goto_convert_exceptions.cpp.

◆ convert_decl()

void goto_convertt::convert_decl ( const code_declt code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 607 of file goto_convert.cpp.

◆ convert_decl_type()

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

Definition at line 666 of file goto_convert.cpp.

◆ convert_dowhile()

void goto_convertt::convert_dowhile ( const code_dowhilet code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 1020 of file goto_convert.cpp.

◆ convert_end_thread()

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

Definition at line 1340 of file goto_convert.cpp.

◆ convert_expression()

void goto_convertt::convert_expression ( const code_expressiont code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 570 of file goto_convert.cpp.

◆ convert_for()

void goto_convertt::convert_for ( const code_fort code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 870 of file goto_convert.cpp.

◆ convert_function_call()

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

Definition at line 24 of file goto_convert_function_call.cpp.

◆ convert_gcc_computed_goto()

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

Definition at line 1313 of file goto_convert.cpp.

◆ convert_gcc_local_label()

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

Definition at line 347 of file goto_convert.cpp.

◆ convert_gcc_switch_case_range()

void goto_convertt::convert_gcc_switch_case_range ( const code_gcc_switch_case_ranget code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 386 of file goto_convert.cpp.

◆ convert_goto()

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

Definition at line 1303 of file goto_convert.cpp.

◆ convert_ifthenelse()

void goto_convertt::convert_ifthenelse ( const code_ifthenelset code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 1376 of file goto_convert.cpp.

◆ convert_label()

void goto_convertt::convert_label ( const code_labelt code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 306 of file goto_convert.cpp.

◆ convert_loop_invariant()

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

Definition at line 847 of file goto_convert.cpp.

◆ convert_msc_leave()

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

Definition at line 69 of file goto_convert_exceptions.cpp.

◆ convert_msc_try_except()

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

Definition at line 54 of file goto_convert_exceptions.cpp.

◆ convert_msc_try_finally()

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

Definition at line 16 of file goto_convert_exceptions.cpp.

◆ convert_return()

void goto_convertt::convert_return ( const code_returnt code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 1225 of file goto_convert.cpp.

◆ convert_skip()

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

Definition at line 826 of file goto_convert.cpp.

◆ convert_start_thread()

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

Definition at line 1326 of file goto_convert.cpp.

◆ convert_switch()

void goto_convertt::convert_switch ( const code_switcht code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 1108 of file goto_convert.cpp.

◆ convert_switch_case()

void goto_convertt::convert_switch_case ( const code_switch_caset code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 354 of file goto_convert.cpp.

◆ convert_try_catch()

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

Definition at line 85 of file goto_convert_exceptions.cpp.

◆ convert_while()

void goto_convertt::convert_while ( const code_whilet code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 962 of file goto_convert.cpp.

◆ copy()

void goto_convertt::copy ( const codet code,
goto_program_instruction_typet  type,
goto_programt dest 
)
protected

Definition at line 296 of file goto_convert.cpp.

◆ 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 540 of file builtin_functions.cpp.

◆ 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

Definition at line 603 of file builtin_functions.cpp.

◆ do_atomic_begin()

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

Definition at line 375 of file builtin_functions.cpp.

◆ do_atomic_end()

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

Definition at line 398 of file builtin_functions.cpp.

◆ do_cpp_new()

void goto_convertt::do_cpp_new ( const exprt lhs,
const side_effect_exprt rhs,
goto_programt dest 
)
protectedvirtual

Definition at line 421 of file builtin_functions.cpp.

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

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

Definition at line 37 of file goto_convert_function_call.cpp.

◆ 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

Definition at line 96 of file goto_convert_function_call.cpp.

◆ 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

Definition at line 158 of file goto_convert_function_call.cpp.

◆ 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

add function calls to function queue for later processing

Definition at line 645 of file builtin_functions.cpp.

◆ do_function_call_symbol() [2/2]

virtual void goto_convertt::do_function_call_symbol ( const symbolt )
inlineprotectedvirtual

Definition at line 199 of file goto_convert_class.h.

◆ do_input()

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

Definition at line 337 of file builtin_functions.cpp.

◆ 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 rhs,
const exprt::operandst arguments,
goto_programt dest 
)
protected

Definition at line 356 of file builtin_functions.cpp.

◆ do_printf()

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

Definition at line 198 of file builtin_functions.cpp.

◆ do_prob_coin()

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

Definition at line 111 of file builtin_functions.cpp.

◆ do_prob_uniform()

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

Definition at line 32 of file builtin_functions.cpp.

◆ do_scanf()

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

Definition at line 235 of file builtin_functions.cpp.

◆ exception_flag()

symbol_exprt goto_convertt::exception_flag ( const irep_idt mode)
protected

Definition at line 235 of file goto_convert_exceptions.cpp.

◆ finish_computed_gotos()

void goto_convertt::finish_computed_gotos ( goto_programt dest)
protected

Definition at line 199 of file goto_convert.cpp.

◆ finish_gotos()

void goto_convertt::finish_gotos ( goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 106 of file goto_convert.cpp.

◆ 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

if(guard) goto target_true; else goto target_false;

Definition at line 1636 of file goto_convert.cpp.

◆ 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

Definition at line 1602 of file goto_convert.cpp.

◆ 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

if(guard) true_case; else false_case;

Definition at line 1446 of file goto_convert.cpp.

◆ 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
modeLanguage mode

Definition at line 1887 of file goto_convert.cpp.

◆ get_array_argument()

exprt goto_convertt::get_array_argument ( const exprt src)
protected

Definition at line 567 of file builtin_functions.cpp.

◆ get_constant()

exprt goto_convertt::get_constant ( const exprt expr)
protected

Definition at line 1772 of file goto_convert.cpp.

◆ get_string_constant() [1/2]

irep_idt goto_convertt::get_string_constant ( const exprt expr)
protected

Definition at line 1758 of file goto_convert.cpp.

◆ get_string_constant() [2/2]

bool goto_convertt::get_string_constant ( const exprt expr,
irep_idt value 
)
protected

Definition at line 1710 of file goto_convert.cpp.

◆ goto_convert()

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

Definition at line 275 of file goto_convert.cpp.

◆ goto_convert_rec()

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

Definition at line 283 of file goto_convert.cpp.

◆ has_function_call()

bool goto_convertt::has_function_call ( const exprt expr)
staticprotected

Definition at line 24 of file goto_convert_side_effect.cpp.

◆ has_sideeffect()

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

◆ make_compound_literal()

symbol_exprt goto_convertt::make_compound_literal ( const exprt expr,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 23 of file goto_clean_expr.cpp.

◆ make_temp_symbol()

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

Definition at line 1821 of file goto_convert.cpp.

◆ needs_cleaning()

bool goto_convertt::needs_cleaning ( const exprt expr)
staticprotected

Definition at line 65 of file goto_clean_expr.cpp.

◆ 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

Definition at line 1798 of file goto_convert.cpp.

◆ 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 231 of file goto_convert.cpp.

◆ remove_assignment()

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

Definition at line 37 of file goto_convert_side_effect.cpp.

◆ remove_cpp_delete()

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

Definition at line 390 of file goto_convert_side_effect.cpp.

◆ remove_cpp_new()

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

Definition at line 363 of file goto_convert_side_effect.cpp.

◆ remove_function_call()

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

Definition at line 287 of file goto_convert_side_effect.cpp.

◆ remove_gcc_conditional_expression()

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

Definition at line 495 of file goto_clean_expr.cpp.

◆ remove_malloc()

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

Definition at line 406 of file goto_convert_side_effect.cpp.

◆ remove_post()

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

Definition at line 207 of file goto_convert_side_effect.cpp.

◆ remove_pre()

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

Definition at line 136 of file goto_convert_side_effect.cpp.

◆ remove_side_effect()

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

Definition at line 553 of file goto_convert_side_effect.cpp.

◆ remove_statement_expression()

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

Definition at line 474 of file goto_convert_side_effect.cpp.

◆ remove_temporary_object()

void goto_convertt::remove_temporary_object ( side_effect_exprt expr,
goto_programt dest 
)
protected

Definition at line 439 of file goto_convert_side_effect.cpp.

◆ replace_new_object()

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

Definition at line 352 of file goto_convert_side_effect.cpp.

◆ rewrite_boolean()

void goto_convertt::rewrite_boolean ( exprt dest)
protected

re-write boolean operators into ?:

Definition at line 110 of file goto_clean_expr.cpp.

◆ unwind_destructor_stack()

void goto_convertt::unwind_destructor_stack ( const source_locationt source_location,
goto_programt dest,
const irep_idt mode,
optionalt< node_indext end_index = {},
optionalt< node_indext starting_index = {} 
)
protected

Unwinds the destructor stack and creates destructors for each node between destructor_start_point and destructor_end_point (including the start, excluding the end).

If end_index isn't passed, it will unwind the whole stack. If start_index isn't passed, it will unwind from the current node.

When destructors are non-trivial (i.e. if they contain DECL or GOTO statements) then unwinding becomes more complicated because when we call convert on the destructor code it may recursively invoke this function.

Say we have a tree of [3, 2, 1, 0] and we start unwinding from top to bottom. If node 1 has such a non-trivial destructor during the convert it will add nodes to the tree so it ends up looking like this:

3, 2, 1, 0
   5, 4,/

If for example the destructor contained a THROW statement then it would unwind destroying variables 5, 4 and finally 0. Note that we don't have 1 here even if that was the instruction that triggered the recursive unwind because it's already been popped off before convert is called.

After our unwind has finished, we return to our [3, 2, 1, 0] branch and continue processing the branch for destructor 0.

Definition at line 283 of file goto_convert_exceptions.cpp.

Member Data Documentation

◆ lifetime

lifetimet goto_convertt::lifetime = lifetimet::STATIC_GLOBAL
protected

Definition at line 52 of file goto_convert_class.h.

◆ ns

namespacet goto_convertt::ns
protected

Definition at line 50 of file goto_convert_class.h.

◆ symbol_table

symbol_table_baset& goto_convertt::symbol_table
protected

Definition at line 49 of file goto_convert_class.h.

◆ targets

struct goto_convertt::targetst goto_convertt::targets
protected

◆ tmp_symbol_prefix

std::string goto_convertt::tmp_symbol_prefix
protected

Definition at line 51 of file goto_convert_class.h.


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