CBMC
|
#include <goto_convert_class.h>
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 () |
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::targett > | computed_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_than > | cases_mapt |
Protected Member Functions | |
void | goto_convert_rec (const codet &code, goto_programt &dest, const irep_idt &mode) |
symbolt & | new_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_baset & | symbol_table |
namespacet | ns |
std::string | tmp_symbol_prefix |
lifetimet | lifetime = lifetimet::STATIC_GLOBAL |
struct goto_convertt::targetst | targets |
Additional Inherited Members |
Definition at line 33 of file goto_convert_class.h.
|
protected |
Definition at line 395 of file goto_convert_class.h.
|
protected |
Definition at line 390 of file goto_convert_class.h.
|
protected |
Definition at line 389 of file goto_convert_class.h.
|
protected |
Definition at line 388 of file goto_convert_class.h.
|
protected |
Definition at line 371 of file goto_convert_class.h.
|
protected |
Definition at line 387 of file goto_convert_class.h.
|
protected |
Definition at line 386 of file goto_convert_class.h.
|
inline |
Definition at line 39 of file goto_convert_class.h.
|
inlinevirtual |
Definition at line 49 of file goto_convert_class.h.
|
inlinestaticprotected |
Definition at line 122 of file goto_convert_class.h.
|
protected |
Definition at line 107 of file goto_convert.cpp.
Definition at line 1332 of file goto_convert.cpp.
|
protected |
Definition at line 177 of file goto_clean_expr.cpp.
|
protected |
Definition at line 477 of file goto_clean_expr.cpp.
|
staticprotected |
Definition at line 1727 of file goto_convert.cpp.
|
protected |
converts 'code' and appends the result to 'dest'
Definition at line 616 of file goto_convert.cpp.
|
protected |
Definition at line 14 of file goto_asm.cpp.
|
protected |
Definition at line 1033 of file goto_convert.cpp.
|
protected |
Definition at line 875 of file goto_convert.cpp.
|
protected |
Definition at line 1056 of file goto_convert.cpp.
|
protected |
Definition at line 1642 of file goto_convert.cpp.
|
protected |
Definition at line 1652 of file goto_convert.cpp.
|
protected |
Definition at line 728 of file goto_convert.cpp.
|
protected |
Definition at line 1501 of file goto_convert.cpp.
|
protected |
Definition at line 1578 of file goto_convert.cpp.
|
protected |
Definition at line 970 of file goto_convert.cpp.
|
protected |
Definition at line 181 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 145 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 212 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 870 of file goto_convert.cpp.
|
protected |
Definition at line 1253 of file goto_convert.cpp.
|
protected |
Definition at line 1632 of file goto_convert.cpp.
|
protected |
Definition at line 757 of file goto_convert.cpp.
|
protected |
Definition at line 1099 of file goto_convert.cpp.
|
protected |
Definition at line 798 of file goto_convert.cpp.
|
protected |
Definition at line 20 of file goto_convert_function_call.cpp.
|
protected |
Definition at line 1610 of file goto_convert.cpp.
|
protected |
Definition at line 530 of file goto_convert.cpp.
|
protected |
Definition at line 575 of file goto_convert.cpp.
|
protected |
Definition at line 1597 of file goto_convert.cpp.
|
protected |
Definition at line 1662 of file goto_convert.cpp.
|
protected |
Definition at line 489 of file goto_convert.cpp.
|
protected |
Definition at line 1071 of file goto_convert.cpp.
|
protected |
Definition at line 70 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 55 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 17 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 1518 of file goto_convert.cpp.
|
protected |
Definition at line 1050 of file goto_convert.cpp.
|
protected |
Definition at line 1622 of file goto_convert.cpp.
|
protected |
Definition at line 1361 of file goto_convert.cpp.
|
protected |
Definition at line 535 of file goto_convert.cpp.
|
protected |
Definition at line 86 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 1197 of file goto_convert.cpp.
|
protected |
Definition at line 480 of file goto_convert.cpp.
|
protected |
builds a goto program for object initialization after new
Definition at line 510 of file builtin_functions.cpp.
|
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.
|
protected |
|
protected |
Definition at line 570 of file builtin_functions.cpp.
|
protected |
Definition at line 340 of file builtin_functions.cpp.
|
protected |
Definition at line 363 of file builtin_functions.cpp.
|
protectedvirtual |
Definition at line 386 of file builtin_functions.cpp.
|
protected |
|
protectedvirtual |
Definition at line 33 of file goto_convert_function_call.cpp.
|
protectedvirtual |
Definition at line 91 of file goto_convert_function_call.cpp.
|
protectedvirtual |
Definition at line 154 of file goto_convert_function_call.cpp.
|
protectedvirtual |
add function calls to function queue for later processing
Definition at line 809 of file builtin_functions.cpp.
|
inlineprotectedvirtual |
Definition at line 225 of file goto_convert_class.h.
|
protected |
Definition at line 617 of file builtin_functions.cpp.
|
protected |
Definition at line 310 of file builtin_functions.cpp.
|
protected |
|
protected |
|
protected |
Definition at line 325 of file builtin_functions.cpp.
|
protected |
Definition at line 193 of file builtin_functions.cpp.
|
protected |
Definition at line 110 of file builtin_functions.cpp.
|
protected |
Definition at line 33 of file builtin_functions.cpp.
|
protected |
Definition at line 207 of file builtin_functions.cpp.
|
protected |
Definition at line 236 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 365 of file goto_convert.cpp.
|
protected |
Definition at line 252 of file goto_convert.cpp.
|
protected |
Definition at line 1934 of file goto_convert.cpp.
|
protected |
if(guard) goto target_true; else goto target_false;
Definition at line 1973 of file goto_convert.cpp.
|
protected |
if(guard) true_case; else false_case;
Definition at line 1754 of file goto_convert.cpp.
|
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
thread_body | Sequence of codet's that can be executed in parallel | |
[out] | dest | Resulting goto-instructions |
mode | Language mode |
Definition at line 2232 of file goto_convert.cpp.
Definition at line 537 of file builtin_functions.cpp.
Definition at line 2114 of file goto_convert.cpp.
Definition at line 2100 of file goto_convert.cpp.
Definition at line 2053 of file goto_convert.cpp.
void goto_convertt::goto_convert | ( | const codet & | code, |
goto_programt & | dest, | ||
const irep_idt & | mode | ||
) |
Definition at line 459 of file goto_convert.cpp.
|
protected |
Definition at line 467 of file goto_convert.cpp.
|
protected |
Definition at line 22 of file goto_clean_expr.cpp.
|
protected |
Definition at line 2164 of file goto_convert.cpp.
|
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.
|
protected |
Definition at line 2139 of file goto_convert.cpp.
|
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.
Definition at line 398 of file goto_convert.cpp.
|
protected |
Definition at line 27 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 461 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 429 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 361 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 550 of file goto_clean_expr.cpp.
|
protected |
Definition at line 478 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 633 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 274 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 179 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 712 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 559 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 515 of file goto_convert_side_effect.cpp.
Definition at line 419 of file goto_convert_side_effect.cpp.
|
protected |
re-write boolean operators into ?:
Definition at line 105 of file goto_clean_expr.cpp.
|
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.
|
protected |
Definition at line 57 of file goto_convert_class.h.
|
protected |
Definition at line 55 of file goto_convert_class.h.
|
protected |
Definition at line 54 of file goto_convert_class.h.
|
protected |
|
protected |
Definition at line 56 of file goto_convert_class.h.