cprover
Loading...
Searching...
No Matches
goto_check_c.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Checks for Errors in C/C++ Programs
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANSI_C_GOTO_CHECK_C_H
13#define CPROVER_ANSI_C_GOTO_CHECK_C_H
14
16
17class goto_modelt;
18class namespacet;
19class optionst;
21
22void goto_check_c(
23 const namespacet &ns,
24 const optionst &options,
25 goto_functionst &goto_functions,
26 message_handlert &message_handler);
27
28void goto_check_c(
29 const irep_idt &function_identifier,
31 const namespacet &ns,
32 const optionst &options,
33 message_handlert &message_handler);
34
35void goto_check_c(
36 const optionst &options,
37 goto_modelt &goto_model,
38 message_handlert &message_handler);
39
40#define OPT_GOTO_CHECK \
41 "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)" \
42 "(div-by-zero-check)(enum-range-check)" \
43 "(signed-overflow-check)(unsigned-overflow-check)" \
44 "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
45 "(float-overflow-check)(nan-check)(no-built-in-assertions)" \
46 "(pointer-primitive-check)" \
47 "(retain-trivial-checks)" \
48 "(error-label):" \
49 "(no-assertions)(no-assumptions)" \
50 "(assert-to-assume)"
51
52#define HELP_GOTO_CHECK \
53 " {y--bounds-check} \t enable array bounds checks\n" \
54 " {y--pointer-check} \t enable pointer checks\n" \
55 " {y--memory-leak-check} \t enable memory leak checks\n" \
56 " {y--memory-cleanup-check} \t enable memory cleanup checks\n" \
57 " {y--div-by-zero-check} \t enable division by zero checks\n" \
58 " {y--signed-overflow-check} \t " \
59 "enable signed arithmetic over- and underflow checks\n" \
60 " {y--unsigned-overflow-check} \t " \
61 "enable arithmetic over- and underflow checks\n" \
62 " {y--pointer-overflow-check} \t " \
63 "enable pointer arithmetic over- and underflow checks\n" \
64 " {y--conversion-check} \t " \
65 "check whether values can be represented after type cast\n" \
66 " {y--undefined-shift-check} \t check shift greater than bit-width\n" \
67 " {y--float-overflow-check} \t check floating-point for +/-Inf\n" \
68 " {y--nan-check} \t check floating-point for NaN\n" \
69 " {y--enum-range-check} \t " \
70 "checks that all enum type expressions have values in the enum range\n" \
71 " {y--pointer-primitive-check} \t " \
72 "checks that all pointers in pointer primitives are valid or null\n" \
73 " {y--retain-trivial-checks} \t include checks that are trivially true\n" \
74 " {y--error-label} {ulabel} \t check that label {ulabel} is unreachable\n" \
75 " {y--no-built-in-assertions} \t ignore assertions in built-in library\n" \
76 " {y--no-assertions} \t ignore user assertions\n" \
77 " {y--no-assumptions} \t ignore user assumptions\n" \
78 " {y--assert-to-assume} \t convert user assertions to assumptions\n"
79
80// clang-format off
81#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
82 options.set_option("bounds-check", cmdline.isset("bounds-check")); \
83 options.set_option("pointer-check", cmdline.isset("pointer-check")); \
84 options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
85 options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \
86 options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
87 options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
88 options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \
89 options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */ \
90 options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */ \
91 options.set_option("conversion-check", cmdline.isset("conversion-check")); \
92 options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \
93 options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */ \
94 options.set_option("nan-check", cmdline.isset("nan-check")); \
95 options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
96 options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
97 options.set_option("retain-trivial-checks", \
98 cmdline.isset("retain-trivial-checks")); \
99 options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \
100 options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \
101 options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
102 options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
103 if(cmdline.isset("error-label")) \
104 options.set_option("error-label", cmdline.get_values("error-label")); \
105 (void)0
106// clang-format on
107
108#endif // CPROVER_ANALYSES_GOTO_CHECK_C_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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...
Definition namespace.h:91
void goto_check_c(const namespacet &ns, const optionst &options, goto_functionst &goto_functions, message_handlert &message_handler)
Goto Programs with Functions.