Loading...

Searching...

No Matches

Functions

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]

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.