#include <memory>
#include <util/irep.h>

Include dependency graph for rebuild_goto_start_function.h:

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

Functions
void	remove_existing_entry_point (symbol_table_baset &)
	Eliminate the existing entry point function symbol and any symbols created in that scope from the `symbol_table`.

const irep_idt &	get_entry_point_mode (const symbol_table_baset &)
	Find out the mode of the current entry point to determine the mode of the replacement entry point.

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.

Detailed Description

Function Documentation

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

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.

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.