goto_check.cpp File Reference

GOTO Programs. More...

#include "goto_check.h"
#include "goto_check_c.h"
#include <util/symbol.h>

Include dependency graph for goto_check.cpp:

Go to the source code of this file.

Functions
void	goto_check (const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
void	goto_check (const namespacet &ns, const optionst &options, goto_functionst &goto_functions, message_handlert &message_handler)
void	goto_check (const optionst &options, goto_modelt &goto_model, message_handlert &message_handler)

Detailed Description

GOTO Programs.

Definition in file goto_check.cpp.

Function Documentation

goto_check() [1/3]

void goto_check	(	const irep_idt &	function_identifier,
		goto_functionst::goto_functiont &	goto_function,
		const namespacet &	ns,
		const optionst &	options,
		message_handlert &	message_handler
	)

Definition at line 18 of file goto_check.cpp.

goto_check() [2/3]

void goto_check	(	const namespacet &	ns,
		const optionst &	options,
		goto_functionst &	goto_functions,
		message_handlert &	message_handler
	)

Definition at line 34 of file goto_check.cpp.

goto_check() [3/3]

void goto_check	(	const optionst &	options,
		goto_modelt &	goto_model,
		message_handlert &	message_handler
	)

Definition at line 43 of file goto_check.cpp.