goto_convert_new_switch_case.cpp File Reference

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"

Include dependency graph for goto_convert_new_switch_case.cpp:

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)

Detailed Description

Program Transformation.

Definition in file goto_convert_new_switch_case.cpp.

Function Documentation

goto_convert() [1/2]

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().

goto_convert() [2/2]

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.

has_and_or()

static bool has_and_or ( const exprt &  expr )

static

if(guard) goto target;

Definition at line 1702 of file goto_convert_new_switch_case.cpp.

References forall_operands, and irept::id().

is_empty()

static bool is_empty ( const goto_programt &  goto_program )

static

Definition at line 28 of file goto_convert_new_switch_case.cpp.

References forall_goto_program_instructions.