CBMC
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  clean_expr_resultt
 
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 (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::list< std::pair< goto_programt::targett, goto_programt::instructiont > > declaration_hop_instrumentationt
 
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, goto_programt::target_less_thancases_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)
 
clean_expr_resultt clean_expr (exprt &expr, const irep_idt &mode, bool result_is_used=true)
 
clean_expr_resultt clean_expr_address_of (exprt &expr, const irep_idt &mode)
 
irep_idt 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...
 
clean_expr_resultt remove_side_effect (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
 
clean_expr_resultt remove_assignment (side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
 
clean_expr_resultt remove_pre (side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
 
clean_expr_resultt remove_post (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt remove_function_call (side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt remove_cpp_new (side_effect_exprt &expr, bool result_is_used)
 
clean_expr_resultt remove_cpp_delete (side_effect_exprt &expr)
 
clean_expr_resultt remove_malloc (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt remove_temporary_object (side_effect_exprt &expr)
 
clean_expr_resultt remove_statement_expression (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt remove_gcc_conditional_expression (exprt &expr, const irep_idt &mode)
 
clean_expr_resultt remove_overflow (side_effect_expr_overflowt &expr, bool result_is_used, 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, const irep_idt &mode)
 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_frontend_decl (const code_frontend_declt &, goto_programt &, 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_contracts (const codet &code, goto_programt::targett loop)
 
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_frontend_returnt &, 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, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_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...
 
declaration_hop_instrumentationt build_declaration_hops (goto_programt &dest, std::unordered_map< irep_idt, symbolt, irep_id_hash > &label_flags, const build_declaration_hops_inputst &inputs)
 
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, const source_locationt &, goto_programt &true_case, const source_locationt &, 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)
 
void do_havoc_slice (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 
void do_alloca (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 alloca allocates memory that is freed when leaving the function (and not the block, as regular destructors would do). More...
 
exprt get_array_argument (const exprt &src)
 

Static Protected Member Functions

static bool needs_cleaning (const exprt &expr)
 Returns 'true' for expressions that may change the program state. More...
 
static bool assignment_lhs_needs_temporary (const exprt &lhs)
 
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 33 of file goto_convert_class.h.

Member Typedef Documentation

◆ cases_mapt

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

Definition at line 395 of file goto_convert_class.h.

◆ casest

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

Definition at line 390 of file goto_convert_class.h.

◆ caset

Definition at line 389 of file goto_convert_class.h.

◆ computed_gotost

Definition at line 388 of file goto_convert_class.h.

◆ declaration_hop_instrumentationt

◆ gotost

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

Definition at line 387 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 386 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 39 of file goto_convert_class.h.

◆ ~goto_convertt()

virtual goto_convertt::~goto_convertt ( )
inlinevirtual

Definition at line 49 of file goto_convert_class.h.

Member Function Documentation

◆ assignment_lhs_needs_temporary()

static bool goto_convertt::assignment_lhs_needs_temporary ( const exprt lhs)
inlinestaticprotected

Definition at line 122 of file goto_convert_class.h.

◆ build_declaration_hops()

goto_convertt::declaration_hop_instrumentationt goto_convertt::build_declaration_hops ( goto_programt dest,
std::unordered_map< irep_idt, symbolt, irep_id_hash > &  label_flags,
const build_declaration_hops_inputst inputs 
)
protected

Definition at line 107 of file goto_convert.cpp.

◆ case_guard()

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

Definition at line 1332 of file goto_convert.cpp.

◆ clean_expr()

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

Definition at line 177 of file goto_clean_expr.cpp.

◆ clean_expr_address_of()

goto_convertt::clean_expr_resultt goto_convertt::clean_expr_address_of ( exprt expr,
const irep_idt mode 
)
protected

Definition at line 477 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 1727 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 616 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 1033 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 875 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 1056 of file goto_convert.cpp.

◆ convert_atomic_begin()

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

Definition at line 1642 of file goto_convert.cpp.

◆ convert_atomic_end()

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

Definition at line 1652 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 728 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 1501 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 1578 of file goto_convert.cpp.

◆ convert_cpp_delete()

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

Definition at line 970 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 181 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 145 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 212 of file goto_convert_exceptions.cpp.

◆ convert_decl_type()

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

Definition at line 870 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 1253 of file goto_convert.cpp.

◆ convert_end_thread()

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

Definition at line 1632 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 757 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 1099 of file goto_convert.cpp.

◆ convert_frontend_decl()

void goto_convertt::convert_frontend_decl ( const code_frontend_declt code,
goto_programt dest,
const irep_idt mode 
)
protected

Definition at line 798 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 20 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 1610 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 530 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 575 of file goto_convert.cpp.

◆ convert_goto()

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

Definition at line 1597 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 1662 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 489 of file goto_convert.cpp.

◆ convert_loop_contracts()

void goto_convertt::convert_loop_contracts ( const codet code,
goto_programt::targett  loop 
)
protected

Definition at line 1071 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 70 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 55 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 17 of file goto_convert_exceptions.cpp.

◆ convert_return()

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

Definition at line 1518 of file goto_convert.cpp.

◆ convert_skip()

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

Definition at line 1050 of file goto_convert.cpp.

◆ convert_start_thread()

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

Definition at line 1622 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 1361 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 535 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 86 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 1197 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 480 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 510 of file builtin_functions.cpp.

◆ do_alloca()

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

alloca allocates memory that is freed when leaving the function (and not the block, as regular destructors would do).

Definition at line 700 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 570 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 340 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 363 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 386 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 33 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 91 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 154 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,
const irep_idt mode 
)
protectedvirtual

add function calls to function queue for later processing

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

◆ do_havoc_slice()

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

Definition at line 617 of file builtin_functions.cpp.

◆ do_input()

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

Definition at line 310 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 325 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 193 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 110 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 33 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 207 of file builtin_functions.cpp.

◆ exception_flag()

symbol_exprt goto_convertt::exception_flag ( const irep_idt mode)
protected

Definition at line 236 of file goto_convert_exceptions.cpp.

◆ finish_computed_gotos()

void goto_convertt::finish_computed_gotos ( goto_programt dest)
protected

Definition at line 365 of file goto_convert.cpp.

◆ finish_gotos()

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

Definition at line 252 of file goto_convert.cpp.

◆ generate_conditional_branch() [1/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 1934 of file goto_convert.cpp.

◆ generate_conditional_branch() [2/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 1973 of file goto_convert.cpp.

◆ generate_ifthenelse()

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

if(guard) true_case; else false_case;

Definition at line 1754 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 2232 of file goto_convert.cpp.

◆ get_array_argument()

exprt goto_convertt::get_array_argument ( const exprt src)
protected

Definition at line 537 of file builtin_functions.cpp.

◆ get_constant()

exprt goto_convertt::get_constant ( const exprt expr)
protected

Definition at line 2114 of file goto_convert.cpp.

◆ get_string_constant() [1/2]

irep_idt goto_convertt::get_string_constant ( const exprt expr)
protected

Definition at line 2100 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 2053 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 459 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 467 of file goto_convert.cpp.

◆ make_compound_literal()

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

Definition at line 22 of file goto_clean_expr.cpp.

◆ make_temp_symbol()

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

Definition at line 2164 of file goto_convert.cpp.

◆ needs_cleaning()

bool goto_convertt::needs_cleaning ( const exprt expr)
staticprotected

Returns 'true' for expressions that may change the program state.

Expressions that may trigger undefined behavior (e.g., dereference, index, division) are deliberately not included.

Definition at line 69 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 2139 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 398 of file goto_convert.cpp.

◆ remove_assignment()

goto_convertt::clean_expr_resultt goto_convertt::remove_assignment ( side_effect_exprt expr,
bool  result_is_used,
bool  address_taken,
const irep_idt mode 
)
protected

Definition at line 27 of file goto_convert_side_effect.cpp.

◆ remove_cpp_delete()

goto_convertt::clean_expr_resultt goto_convertt::remove_cpp_delete ( side_effect_exprt expr)
protected

Definition at line 461 of file goto_convert_side_effect.cpp.

◆ remove_cpp_new()

goto_convertt::clean_expr_resultt goto_convertt::remove_cpp_new ( side_effect_exprt expr,
bool  result_is_used 
)
protected

Definition at line 429 of file goto_convert_side_effect.cpp.

◆ remove_function_call()

goto_convertt::clean_expr_resultt goto_convertt::remove_function_call ( side_effect_expr_function_callt expr,
const irep_idt mode,
bool  result_is_used 
)
protected

Definition at line 361 of file goto_convert_side_effect.cpp.

◆ remove_gcc_conditional_expression()

goto_convertt::clean_expr_resultt goto_convertt::remove_gcc_conditional_expression ( exprt expr,
const irep_idt mode 
)
protected

Definition at line 550 of file goto_clean_expr.cpp.

◆ remove_malloc()

goto_convertt::clean_expr_resultt goto_convertt::remove_malloc ( side_effect_exprt expr,
const irep_idt mode,
bool  result_is_used 
)
protected

Definition at line 478 of file goto_convert_side_effect.cpp.

◆ remove_overflow()

goto_convertt::clean_expr_resultt goto_convertt::remove_overflow ( side_effect_expr_overflowt expr,
bool  result_is_used,
const irep_idt mode 
)
protected

Definition at line 633 of file goto_convert_side_effect.cpp.

◆ remove_post()

goto_convertt::clean_expr_resultt goto_convertt::remove_post ( side_effect_exprt expr,
const irep_idt mode,
bool  result_is_used 
)
protected

Definition at line 274 of file goto_convert_side_effect.cpp.

◆ remove_pre()

goto_convertt::clean_expr_resultt goto_convertt::remove_pre ( side_effect_exprt expr,
bool  result_is_used,
bool  address_taken,
const irep_idt mode 
)
protected

Definition at line 179 of file goto_convert_side_effect.cpp.

◆ remove_side_effect()

goto_convertt::clean_expr_resultt goto_convertt::remove_side_effect ( side_effect_exprt expr,
const irep_idt mode,
bool  result_is_used,
bool  address_taken 
)
protected

Definition at line 712 of file goto_convert_side_effect.cpp.

◆ remove_statement_expression()

goto_convertt::clean_expr_resultt goto_convertt::remove_statement_expression ( side_effect_exprt expr,
const irep_idt mode,
bool  result_is_used 
)
protected

Definition at line 559 of file goto_convert_side_effect.cpp.

◆ remove_temporary_object()

goto_convertt::clean_expr_resultt goto_convertt::remove_temporary_object ( side_effect_exprt expr)
protected

Definition at line 515 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 419 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 105 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,
std::optional< node_indext end_index = {},
std::optional< 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 280 of file goto_convert_exceptions.cpp.

Member Data Documentation

◆ lifetime

lifetimet goto_convertt::lifetime = lifetimet::STATIC_GLOBAL
protected

Definition at line 57 of file goto_convert_class.h.

◆ ns

namespacet goto_convertt::ns
protected

Definition at line 55 of file goto_convert_class.h.

◆ symbol_table

symbol_table_baset& goto_convertt::symbol_table
protected

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


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