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