cprover
Loading...
Searching...
No Matches
goto_check_c.h File Reference

Program Transformation. More...

+ Include dependency graph for goto_check_c.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_c (const namespacet &ns, const optionst &options, goto_functionst &goto_functions, message_handlert &message_handler)
 
void goto_check_c (const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
 
void goto_check_c (const optionst &options, goto_modelt &goto_model, message_handlert &message_handler)
 

Detailed Description

Program Transformation.

Definition in file goto_check_c.h.

Macro Definition Documentation

◆ HELP_GOTO_CHECK

#define HELP_GOTO_CHECK
Value:
" {y--bounds-check} \t enable array bounds checks\n" \
" {y--pointer-check} \t enable pointer checks\n" \
" {y--memory-leak-check} \t enable memory leak checks\n" \
" {y--memory-cleanup-check} \t enable memory cleanup checks\n" \
" {y--div-by-zero-check} \t enable division by zero checks\n" \
" {y--signed-overflow-check} \t " \
"enable signed arithmetic over- and underflow checks\n" \
" {y--unsigned-overflow-check} \t " \
"enable arithmetic over- and underflow checks\n" \
" {y--pointer-overflow-check} \t " \
"enable pointer arithmetic over- and underflow checks\n" \
" {y--conversion-check} \t " \
"check whether values can be represented after type cast\n" \
" {y--undefined-shift-check} \t check shift greater than bit-width\n" \
" {y--float-overflow-check} \t check floating-point for +/-Inf\n" \
" {y--nan-check} \t check floating-point for NaN\n" \
" {y--enum-range-check} \t " \
"checks that all enum type expressions have values in the enum range\n" \
" {y--pointer-primitive-check} \t " \
"checks that all pointers in pointer primitives are valid or null\n" \
" {y--retain-trivial-checks} \t include checks that are trivially true\n" \
" {y--error-label} {ulabel} \t check that label {ulabel} is unreachable\n" \
" {y--no-built-in-assertions} \t ignore assertions in built-in library\n" \
" {y--no-assertions} \t ignore user assertions\n" \
" {y--no-assumptions} \t ignore user assumptions\n" \
" {y--assert-to-assume} \t convert user assertions to assumptions\n"

Definition at line 52 of file goto_check_c.h.

◆ OPT_GOTO_CHECK

#define OPT_GOTO_CHECK
Value:
"(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-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)" \
"(retain-trivial-checks)" \
"(error-label):" \
"(no-assertions)(no-assumptions)" \
"(assert-to-assume)"

Definition at line 40 of file goto_check_c.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("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \
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) */ \
options.set_option("retain-trivial-checks", \
cmdline.isset("retain-trivial-checks")); \
options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \
options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \
options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
if(cmdline.isset("error-label")) \
options.set_option("error-label", cmdline.get_values("error-label")); \
(void)0

Definition at line 81 of file goto_check_c.h.

Function Documentation

◆ goto_check_c() [1/3]

void goto_check_c ( const irep_idt & function_identifier,
goto_functionst::goto_functiont & goto_function,
const namespacet & ns,
const optionst & options,
message_handlert & message_handler )

Definition at line 2392 of file goto_check_c.cpp.

◆ goto_check_c() [2/3]

void goto_check_c ( const namespacet & ns,
const optionst & options,
goto_functionst & goto_functions,
message_handlert & message_handler )

Definition at line 2403 of file goto_check_c.cpp.

◆ goto_check_c() [3/3]

void goto_check_c ( const optionst & options,
goto_modelt & goto_model,
message_handlert & message_handler )

Definition at line 2419 of file goto_check_c.cpp.