12 #ifndef CPROVER_ANALYSES_GOTO_CHECK_H
13 #define CPROVER_ANALYSES_GOTO_CHECK_H
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-" \
40 "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
41 "(float-overflow-check)(nan-check)(no-built-in-assertions)" \
42 "(pointer-primitive-check)" \
43 "(retain-trivial-checks)" \
45 "(no-assertions)(no-assumptions)" \
49 #define HELP_GOTO_CHECK \
50 " --bounds-check enable array bounds checks\n" \
51 " --pointer-check enable pointer checks\n"
\
52 " --memory-leak-check enable memory leak checks\n" \
53 " --div-by-zero-check enable division by zero checks\n" \
54 " --signed-overflow-check enable signed arithmetic over- and underflow checks\n"
\
55 " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" \
56 " --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" \
57 " --conversion-check check whether values can be represented after type cast\n" \
58 " --undefined-shift-check check shift greater than bit-width\n" \
59 " --float-overflow-check check floating-point for +/-Inf\n" \
60 " --nan-check check floating-point for NaN\n" \
61 " --enum-range-check checks that all enum type expressions have values in the enum range\n"
\
62 " --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" \
63 " --no-built-in-assertions ignore assertions in built-in library\n" \
64 " --retain-trivial-checks include checks that are trivially true\n" \
65 " --error-label label check that label is unreachable\n" \
66 " --no-built-in-assertions ignore assertions in built-in library\n" \
67 " --no-assertions ignore user assertions\n" \
68 " --no-assumptions ignore user assumptions\n" \
69 " --assert-to-assume convert user assertions to assumptions\n" \
71 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
72 options.set_option("bounds-check", cmdline.isset("bounds-check")); \
73 options.set_option("pointer-check", cmdline.isset("pointer-check")); \
74 options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
75 options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
76 options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
77 options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check"));
\
78 options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check"));
\
79 options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check"));
\
80 options.set_option("conversion-check", cmdline.isset("conversion-check")); \
81 options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check"));
\
82 options.set_option("float-overflow-check", cmdline.isset("float-overflow-check"));
\
83 options.set_option("nan-check", cmdline.isset("nan-check")); \
84 options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions"));
\
85 options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check"));
\
86 options.set_option("retain-trivial-checks", \
87 cmdline.isset("retain-trivial-checks")); \
88 options.set_option("assertions", !cmdline.isset("no-assertions"));
\
89 options.set_option("assumptions", !cmdline.isset("no-assumptions"));
\
90 options.set_option("assert-to-assume", cmdline.isset("assert-to-assume"));
\
91 options.set_option("retain-trivial", cmdline.isset("retain-trivial"));
\
92 if(cmdline.isset("error-label")) \
93 options.set_option("error-label", cmdline.get_values("error-label")); \
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
::goto_functiont goto_functiont
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void goto_check(const namespacet &ns, const optionst &options, goto_functionst &goto_functions)
Goto Programs with Functions.