cprover
goto_check.h File Reference

Program Transformation. More...

+ 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.

Macros

#define OPT_GOTO_CHECK
 
#define HELP_GOTO_CHECK
 
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
 

Functions

void goto_check (const namespacet &ns, const optionst &options, goto_functionst &goto_functions)
 
void goto_check (const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
 
void goto_check (const optionst &options, goto_modelt &goto_model)
 

Detailed Description

Program Transformation.

Definition in file goto_check.h.

Macro Definition Documentation

◆ HELP_GOTO_CHECK

#define HELP_GOTO_CHECK
Value:
" --bounds-check enable array bounds checks\n" \
" --pointer-check enable pointer checks\n" /* NOLINT(whitespace/line_length) */ \
" --memory-leak-check enable memory leak checks\n" \
" --div-by-zero-check enable division by zero checks\n" \
" --signed-overflow-check enable signed arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
" --unsigned-overflow-check enable arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
" --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
" --conversion-check check whether values can be represented after type cast\n" /* NOLINT(whitespace/line_length) */ \
" --undefined-shift-check check shift greater than bit-width\n" \
" --float-overflow-check check floating-point for +/-Inf\n" \
" --nan-check check floating-point for NaN\n" \
" --no-built-in-assertions ignore assertions in built-in library\n" \
" --enum-range-check checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
" --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */

Definition at line 45 of file goto_check.h.

◆ OPT_GOTO_CHECK

#define OPT_GOTO_CHECK
Value:
"(bounds-check)(pointer-check)(memory-leak-check)" \
"(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-" \
"overflow-check)" \
"(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
"(float-overflow-check)(nan-check)(no-built-in-assertions)" \
"(pointer-primitive-check)"

Definition at line 36 of file goto_check.h.

◆ PARSE_OPTIONS_GOTO_CHECK

#define PARSE_OPTIONS_GOTO_CHECK (   cmdline,
  options 
)
Value:
options.set_option("bounds-check", cmdline.isset("bounds-check")); \
options.set_option("pointer-check", cmdline.isset("pointer-check")); \
options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \
options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */ \
options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */ \
options.set_option("conversion-check", cmdline.isset("conversion-check")); \
options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \
options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */ \
options.set_option("nan-check", cmdline.isset("nan-check")); \
options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")) /* NOLINT(whitespace/line_length) */

Definition at line 61 of 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 
)

Definition at line 2231 of file goto_check.cpp.

◆ goto_check() [2/3]

void goto_check ( const namespacet ns,
const optionst options,
goto_functionst goto_functions 
)

Definition at line 2241 of file goto_check.cpp.

◆ goto_check() [3/3]

void goto_check ( const optionst options,
goto_modelt goto_model 
)

Definition at line 2256 of file goto_check.cpp.