goto_convert.h File Reference

Program Transformation. More...

#include <util/message.h>
#include <util/std_code.h>
#include "goto_program.h"

Include dependency graph for goto_convert.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
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)

Detailed Description

Program Transformation.

Definition in file goto_convert.h.

Function Documentation

goto_convert() [1/2]

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

goto_convert() [2/2]

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.