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 
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 namespacet &ns,
28  const optionst &options,
29  const irep_idt &mode,
30  goto_functionst::goto_functiont &goto_function);
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)(signed-overflow-check)(unsigned-overflow-check)" \
39  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
40  "(float-overflow-check)(nan-check)(no-built-in-assertions)"
41 
42 // clang-format off
43 #define HELP_GOTO_CHECK \
44  " --bounds-check enable array bounds checks\n" \
45  " --pointer-check enable pointer checks\n" /* NOLINT(whitespace/line_length) */ \
46  " --memory-leak-check enable memory leak checks\n" \
47  " --div-by-zero-check enable division by zero checks\n" \
48  " --signed-overflow-check enable signed arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
49  " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
50  " --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
51  " --conversion-check check whether values can be represented after type cast\n" /* NOLINT(whitespace/line_length) */ \
52  " --undefined-shift-check check shift greater than bit-width\n" \
53  " --float-overflow-check check floating-point for +/-Inf\n" \
54  " --nan-check check floating-point for NaN\n" \
55  " --no-built-in-assertions ignore assertions in built-in library\n" \
56 // clang-format on
57 
58 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
59  options.set_option("bounds-check", cmdline.isset("bounds-check")); \
60  options.set_option("pointer-check", cmdline.isset("pointer-check")); \
61  options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
62  options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
63  options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \
64  options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */ \
65  options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */ \
66  options.set_option("conversion-check", cmdline.isset("conversion-check")); \
67  options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \
68  options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */ \
69  options.set_option("nan-check", cmdline.isset("nan-check")); \
70  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */
71 
72 #endif // CPROVER_ANALYSES_GOTO_CHECK_H
void goto_check(const namespacet &ns, const optionst &options, goto_functionst &goto_functions)
Goto Programs with Functions.
Symbol Table + CFG.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35