cprover
|
Program Transformation. More...
#include "goto_convert.h"
#include <cassert>
#include <util/cprover_prefix.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <util/simplify_expr.h>
#include <util/rename.h>
#include <util/c_types.h>
#include "goto_convert_class.h"
#include "destructor.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_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler) |
void | goto_convert (symbol_tablet &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 43 of file goto_convert.cpp.
References irept::find(), Forall_goto_program_instructions, irept::get_sub(), and irept::is_nil().
Referenced by goto_convertt::goto_convert_rec().
void goto_convert | ( | const codet & | code, |
symbol_tablet & | symbol_table, | ||
goto_programt & | dest, | ||
message_handlert & | message_handler | ||
) |
Definition at line 2179 of file goto_convert.cpp.
Referenced by goto_diff_parse_optionst::get_goto_program(), clobber_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), goto_convert(), initialize_goto_model(), link_to_library(), and model_argc_argv().
void goto_convert | ( | symbol_tablet & | symbol_table, |
goto_programt & | dest, | ||
message_handlert & | message_handler | ||
) |
Definition at line 2214 of file goto_convert.cpp.
|
static |
if(guard) goto target;
Definition at line 1905 of file goto_convert.cpp.
References forall_operands, and irept::id().
Referenced by goto_convertt::generate_conditional_branch().
|
static |
Definition at line 30 of file goto_convert.cpp.
References forall_goto_program_instructions.
Referenced by goto_convertt::generate_ifthenelse().
|
inlinestatic |
This is (believed to be) faster than using std::list.size.
Definition at line 1757 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::instructions.
Referenced by goto_convertt::generate_ifthenelse().