ansi_c_entry_point.cpp File Reference

#include "ansi_c_entry_point.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/symbol_table_base.h>
#include <goto-programs/goto_functions.h>
#include <linking/static_lifetime_init.h>
#include "c_nondet_symbol_factory.h"
#include "expr2c.h"

Include dependency graph for ansi_c_entry_point.cpp:

Go to the source code of this file.

Functions
exprt::operandst	build_function_environment (const code_typet::parameterst &parameters, code_blockt &init_code, symbol_table_baset &symbol_table, const c_object_factory_parameterst &object_factory_parameters)
void	record_function_outputs (const symbolt &function, code_blockt &init_code, symbol_table_baset &symbol_table)
bool	ansi_c_entry_point (symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
bool	generate_ansi_c_start_function (const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
	Generate a _start function for a specific function. More...

Function Documentation

ansi_c_entry_point()

bool ansi_c_entry_point	(	symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		const c_object_factory_parameterst &	object_factory_parameters
	)

Definition at line 105 of file ansi_c_entry_point.cpp.

build_function_environment()

exprt::operandst build_function_environment	(	const code_typet::parameterst &	parameters,
		code_blockt &	init_code,
		symbol_table_baset &	symbol_table,
		const c_object_factory_parameterst &	object_factory_parameters
	)

Definition at line 25 of file ansi_c_entry_point.cpp.

generate_ansi_c_start_function()

bool generate_ansi_c_start_function	(	const symbolt &	symbol,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		const c_object_factory_parameterst &	object_factory_parameters
	)

Generate a _start function for a specific function.

Parameters

symbol	The symbol for the function that should be used as the entry point
symbol_table	The symbol table for the program. The new _start function symbol will be added to this table
message_handler	The message handler
object_factory_parameters	configuration parameters for the object factory

Returns

Returns false if the _start method was generated correctly

Definition at line 184 of file ansi_c_entry_point.cpp.

record_function_outputs()

void record_function_outputs	(	const symbolt &	function,
		code_blockt &	init_code,
		symbol_table_baset &	symbol_table
	)

Definition at line 55 of file ansi_c_entry_point.cpp.