cprover
|
Program Transformation. More...
#include "goto_convert_class.h"
#include <cassert>
#include <util/cprover_prefix.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.h"
#include "destructor.h"
Go to the source code of this file.
Functions | |
static bool | is_empty (const goto_programt &goto_program) |
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_new_switch_case.cpp.
void goto_convert | ( | const codet & | code, |
symbol_tablet & | symbol_table, | ||
goto_programt & | dest, | ||
message_handlert & | message_handler | ||
) |
Definition at line 1968 of file goto_convert_new_switch_case.cpp.
References messaget::eom(), message_handlert::get_message_count(), goto_convert(), and messaget::M_ERROR.
Referenced by goto_convert().
void goto_convert | ( | symbol_tablet & | symbol_table, |
goto_programt & | dest, | ||
message_handlert & | message_handler | ||
) |
Definition at line 2002 of file goto_convert_new_switch_case.cpp.
References goto_convert(), symbol_tablet::symbols, to_code(), and symbolt::value.
|
static |
if(guard) goto target;
Definition at line 1702 of file goto_convert_new_switch_case.cpp.
References forall_operands, and irept::id().
|
static |
Definition at line 28 of file goto_convert_new_switch_case.cpp.
References forall_goto_program_instructions.