rebuild_goto_start_function.cpp File Reference

Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m. More...

#include "rebuild_goto_start_function.h"
#include <util/prefix.h>
#include <util/symbol_table_base.h>
#include <goto-programs/goto_functions.h>
#include <langapi/language.h>
#include <langapi/mode.h>
#include <memory>

Include dependency graph for rebuild_goto_start_function.cpp:

Go to the source code of this file.

Functions
std::unique_ptr< languaget >	get_entry_point_language (const symbol_table_baset &symbol_table, const optionst &options, message_handlert &message_handler)
	Find the language corresponding to the __CPROVER_start function. More...
const irep_idt &	get_entry_point_mode (const symbol_table_baset &symbol_table)
	Find out the mode of the current entry point to determine the mode of the replacement entry point. More...
void	remove_existing_entry_point (symbol_table_baset &symbol_table)
	Eliminate the existing entry point function symbol and any symbols created in that scope from the symbol_table. More...

Detailed Description

Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.

Definition in file rebuild_goto_start_function.cpp.

Function Documentation

get_entry_point_language()

std::unique_ptr<languaget> get_entry_point_language	(	const symbol_table_baset &	symbol_table,
		const optionst &	options,
		message_handlert &	message_handler
	)

Find the language corresponding to the __CPROVER_start function.

Parameters

symbol_table	The symbol table of the goto model.
options	Command-line options
message_handler	The message handler to report any messages with

Definition at line 24 of file rebuild_goto_start_function.cpp.

get_entry_point_mode()

const irep_idt& get_entry_point_mode

(

const symbol_table_baset &

symbol_table

)

Find out the mode of the current entry point to determine the mode of the replacement entry point.

Returns

A mode string saying which language to use

Definition at line 39 of file rebuild_goto_start_function.cpp.

remove_existing_entry_point()

void remove_existing_entry_point

(

symbol_table_baset &

symbol_table

)

Eliminate the existing entry point function symbol and any symbols created in that scope from the symbol_table.

Definition at line 46 of file rebuild_goto_start_function.cpp.