cprover
goto_check.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Program Transformation
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_ANALYSES_GOTO_CHECK_H
13
#define CPROVER_ANALYSES_GOTO_CHECK_H
14
15
#include <
goto-programs/goto_functions.h
>
16
#include <
goto-programs/goto_model.h
>
17
18
class
namespacet
;
19
class
optionst
;
20
21
void
goto_check
(
22
const
namespacet
&ns,
23
const
optionst
&options,
24
goto_functionst
&goto_functions);
25
26
void
goto_check
(
27
const
irep_idt
&function_identifier,
28
goto_functionst::goto_functiont
&goto_function,
29
const
namespacet
&ns,
30
const
optionst
&options);
31
32
void
goto_check
(
33
const
optionst
&options,
34
goto_modelt
&goto_model);
35
36
#define OPT_GOTO_CHECK \
37
"(bounds-check)(pointer-check)(memory-leak-check)" \
38
"(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-" \
39
"overflow-check)" \
40
"(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
41
"(float-overflow-check)(nan-check)(no-built-in-assertions)"
42
43
// clang-format off
44
#define HELP_GOTO_CHECK \
45
" --bounds-check enable array bounds checks\n" \
46
" --pointer-check enable pointer checks\n"
/* NOLINT(whitespace/line_length) */
\
47
" --memory-leak-check enable memory leak checks\n" \
48
" --div-by-zero-check enable division by zero checks\n" \
49
" --signed-overflow-check enable signed arithmetic over- and underflow checks\n"
/* NOLINT(whitespace/line_length) */
\
50
" --unsigned-overflow-check enable arithmetic over- and underflow checks\n"
/* NOLINT(whitespace/line_length) */
\
51
" --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n"
/* NOLINT(whitespace/line_length) */
\
52
" --conversion-check check whether values can be represented after type cast\n"
/* NOLINT(whitespace/line_length) */
\
53
" --undefined-shift-check check shift greater than bit-width\n" \
54
" --float-overflow-check check floating-point for +/-Inf\n" \
55
" --nan-check check floating-point for NaN\n" \
56
" --no-built-in-assertions ignore assertions in built-in library\n" \
57
" --enum-range-check checks that all enum type expressions have values in the enum range\n"
/* NOLINT(whitespace/line_length) */
\
58
// clang-format on
59
60
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
61
options.set_option("bounds-check", cmdline.isset("bounds-check")); \
62
options.set_option("pointer-check", cmdline.isset("pointer-check")); \
63
options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
64
options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
65
options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
66
options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check"));
/* NOLINT(whitespace/line_length) */
\
67
options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check"));
/* NOLINT(whitespace/line_length) */
\
68
options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check"));
/* NOLINT(whitespace/line_length) */
\
69
options.set_option("conversion-check", cmdline.isset("conversion-check")); \
70
options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check"));
/* NOLINT(whitespace/line_length) */
\
71
options.set_option("float-overflow-check", cmdline.isset("float-overflow-check"));
/* NOLINT(whitespace/line_length) */
\
72
options.set_option("nan-check", cmdline.isset("nan-check")); \
73
options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions"))
/* NOLINT(whitespace/line_length) */
74
75
#endif // CPROVER_ANALYSES_GOTO_CHECK_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
optionst
Definition:
options.h:23
goto_model.h
goto_modelt
Definition:
goto_model.h:26
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition:
goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:23
goto_functions.h
goto_check
void goto_check(const namespacet &ns, const optionst &options, goto_functionst &goto_functions)
Definition:
goto_check.cpp:2153
analyses
goto_check.h
Generated by
1.8.18