goto_check.cpp File Reference

GOTO Programs. More...

#include "goto_check.h"
#include <util/options.h>
#include "goto_model.h"
#include "remove_skip.h"

Include dependency graph for goto_check.cpp:

Go to the source code of this file.

Functions
static void	transform_assertions_assumptions (goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
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

GOTO Programs.

Definition in file goto_check.cpp.

Function Documentation

transform_assertions_assumptions() [1/3]

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/3]

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.

transform_assertions_assumptions() [3/3]

static void transform_assertions_assumptions ( goto_programt &  goto_program, bool  enable_assertions, bool  enable_built_in_assertions, bool  enable_assumptions  )

static

Definition at line 19 of file goto_check.cpp.