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)(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)" 43 #define HELP_GOTO_CHECK \ 44 " --bounds-check enable array bounds checks\n" \ 45 " --pointer-check enable pointer checks\n" \ 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" \ 49 " --unsigned-overflow-check enable arithmetic over- and underflow checks\n" \ 50 " --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" \ 51 " --conversion-check check whether values can be represented after type cast\n" \ 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" \ 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")); \ 64 options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \ 65 options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); \ 66 options.set_option("conversion-check", cmdline.isset("conversion-check")); \ 67 options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \ 68 options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \ 69 options.set_option("nan-check", cmdline.isset("nan-check")); \ 70 options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) 72 #endif // CPROVER_ANALYSES_GOTO_CHECK_H void goto_check(const namespacet &ns, const optionst &options, goto_functionst &goto_functions)
Goto Programs with Functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::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...