goto_check.h File Reference

Program Transformation. More...

#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>

Include dependency graph for goto_check.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros
#define	OPT_GOTO_CHECK
#define	HELP_GOTO_CHECK
#define	PARSE_OPTIONS_GOTO_CHECK(cmdline, options)

Functions
void	goto_check (const namespacet &ns, const optionst &options, goto_functionst &goto_functions)
void	goto_check (const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
void	goto_check (const optionst &options, goto_modelt &goto_model)

Detailed Description

Program Transformation.

Definition in file goto_check.h.

Macro Definition Documentation

HELP_GOTO_CHECK

#define HELP_GOTO_CHECK

Value:

" --bounds-check               enable array bounds checks\n" \
  " --pointer-check              enable pointer checks\n" /* NOLINT(whitespace/line_length) */ \
  " --memory-leak-check          enable memory leak checks\n" \
  " --div-by-zero-check          enable division by zero checks\n" \
  " --signed-overflow-check      enable signed arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
  " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */  \
  " --pointer-overflow-check     enable pointer arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */  \
  " --conversion-check           check whether values can be represented after type cast\n" /* NOLINT(whitespace/line_length) */  \
  " --undefined-shift-check      check shift greater than bit-width\n" \
  " --float-overflow-check       check floating-point for +/-Inf\n" \
  " --nan-check                  check floating-point for NaN\n" \
  " --no-built-in-assertions     ignore assertions in built-in library\n" \

Definition at line 43 of file goto_check.h.

OPT_GOTO_CHECK

#define OPT_GOTO_CHECK

Value:

"(bounds-check)(pointer-check)(memory-leak-check)" \
  "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
  "(float-overflow-check)(nan-check)(no-built-in-assertions)"

Definition at line 36 of file goto_check.h.

PARSE_OPTIONS_GOTO_CHECK

#define PARSE_OPTIONS_GOTO_CHECK	(		cmdline,
			options
	)

Value:

options.set_option("bounds-check", cmdline.isset("bounds-check")); \
  options.set_option("pointer-check", cmdline.isset("pointer-check")); \
  options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
  options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
  options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */  \
  options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */  \
  options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */  \
  options.set_option("conversion-check", cmdline.isset("conversion-check")); \
  options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
  options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
  options.set_option("nan-check", cmdline.isset("nan-check")); \
  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */

Definition at line 58 of file goto_check.h.

Function Documentation

goto_check() [1/3]

void goto_check	(	const namespacet &	ns,
		const optionst &	options,
		goto_functionst &	goto_functions
	)

Definition at line 1794 of file goto_check.cpp.

goto_check() [2/3]

void goto_check	(	const namespacet &	ns,
		const optionst &	options,
		const irep_idt &	mode,
		goto_functionst::goto_functiont &	goto_function
	)

Definition at line 1784 of file goto_check.cpp.

goto_check() [3/3]

void goto_check	(	const optionst &	options,
		goto_modelt &	goto_model
	)

Definition at line 1810 of file goto_check.cpp.