CBMC
|
Program Transformation. More...
#include "goto_convert.h"
#include "goto_convert_class.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/cprover_prefix.h>
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/pointer_expr.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <util/symbol_table_builder.h>
#include <goto-programs/remove_skip.h>
#include "destructor.h"
Go to the source code of this file.
Classes | |
struct | build_declaration_hops_inputst |
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.
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 2187 of file goto_convert.cpp.
void goto_convert | ( | symbol_table_baset & | symbol_table, |
goto_programt & | dest, | ||
message_handlert & | message_handler | ||
) |
Definition at line 2200 of file goto_convert.cpp.
|
static |
if(guard) goto target;
Definition at line 1920 of file goto_convert.cpp.
|
static |
Definition at line 31 of file goto_convert.cpp.
|
inlinestatic |
This is (believed to be) faster than using std::list.size.
Definition at line 1747 of file goto_convert.cpp.