cprover
Loading...
Searching...
No Matches
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.
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.

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]

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.