goto_check.h File Reference

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

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

Go to the source code of this file.

Functions
void	transform_assertions_assumptions (const optionst &options, goto_modelt &goto_model)
	Handle the options "assertions", "built-in-assertions", "assumptions" to remove assertions and assumptions in goto_model when these are set to false in options. More...
void	transform_assertions_assumptions (const optionst &options, goto_programt &goto_program)
	Handle the options "assertions", "built-in-assertions", "assumptions" to remove assertions and assumptions in goto_program when these are set to false in options. More...

Detailed Description

Checks for Errors in C and Java Programs.

Definition in file goto_check.h.

Function Documentation

transform_assertions_assumptions() [1/2]

void transform_assertions_assumptions	(	const optionst &	options,
		goto_modelt &	goto_model
	)

Handle the options "assertions", "built-in-assertions", "assumptions" to remove assertions and assumptions in goto_model when these are set to false in options.

Definition at line 57 of file goto_check.cpp.

transform_assertions_assumptions() [2/2]

void transform_assertions_assumptions	(	const optionst &	options,
		goto_programt &	goto_program
	)

Handle the options "assertions", "built-in-assertions", "assumptions" to remove assertions and assumptions in goto_program when these are set to false in options.

Definition at line 80 of file goto_check.cpp.