goto_check.h File Reference

Checks for Errors in C and Java Programs. More...

#include <goto-programs/goto_functions.h>

Include dependency graph for goto_check.h:

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

Go to the source code of this file.

Functions
void	goto_check (const namespacet &, const optionst &, goto_functionst &, message_handlert &)
void	goto_check (const irep_idt &function_identifier, goto_functionst::goto_functiont &, const namespacet &, const optionst &, message_handlert &)
void	goto_check (const optionst &, goto_modelt &, message_handlert &)

Detailed Description

Checks for Errors in C and Java Programs.

Definition in file goto_check.h.

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.