cprover
|
Program Transformation. More...
#include "goto_convert.h"
#include <cassert>
#include <util/arith_tools.h>
#include <util/cprover_prefix.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <util/c_types.h>
#include "goto_convert_class.h"
#include "destructor.h"
#include "remove_skip.h"
Go to the source code of this file.
Functions | |
static bool | is_empty (const goto_programt &goto_program) |
static void | finish_catch_push_targets (goto_programt &dest) |
Populate the CATCH instructions with the targets corresponding to their associated labels. More... | |
static bool | is_size_one (const goto_programt &g) |
This is (believed to be) faster than using std::list.size. More... | |
static bool | has_and_or (const exprt &expr) |
if(guard) goto target; More... | |
void | goto_convert (const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode) |
void | goto_convert (symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler) |
Program Transformation.
Definition in file goto_convert.cpp.
|
static |
Populate the CATCH instructions with the targets corresponding to their associated labels.
Definition at line 42 of file goto_convert.cpp.
References code_push_catcht::exception_list(), Forall_goto_program_instructions, and to_code_push_catch().
Referenced by goto_convertt::goto_convert_rec().
void goto_convert | ( | const codet & | code, |
symbol_table_baset & | symbol_table, | ||
goto_programt & | dest, | ||
message_handlert & | message_handler, | ||
const irep_idt & | mode | ||
) |
Definition at line 2019 of file goto_convert.cpp.
References messaget::eom(), goto_convert(), messaget::M_ERROR, and message_handler.
Referenced by get_gen_nondet_init_instructions(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), goto_convert(), initialize_goto_model(), link_to_library(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new_array(), and model_argc_argv().
void goto_convert | ( | symbol_table_baset & | symbol_table, |
goto_programt & | dest, | ||
message_handlert & | message_handler | ||
) |
Definition at line 2055 of file goto_convert.cpp.
References goto_convert(), message_handler, symbolt::mode, symbol_table_baset::symbols, to_code(), and symbolt::value.
|
static |
if(guard) goto target;
Definition at line 1762 of file goto_convert.cpp.
References forall_operands, and irept::id().
Referenced by goto_convertt::generate_conditional_branch().
|
static |
Definition at line 31 of file goto_convert.cpp.
References forall_goto_program_instructions, goto_program, and is_skip().
Referenced by goto_convertt::generate_ifthenelse().
|
inlinestatic |
This is (believed to be) faster than using std::list.size.
Definition at line 1607 of file goto_convert.cpp.
References goto_programt::instructions.
Referenced by goto_convertt::generate_ifthenelse().