goto_check_c.h File Reference

Program Transformation. More...

#include <goto-programs/goto_functions.h>

Include dependency graph for goto_check_c.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_OPTION_OVERRIDE(cmdline, options, option)
#define	PARSE_OPTIONS_GOTO_CHECK(cmdline, options)

Functions
void	goto_check_c (const namespacet &ns, const optionst &options, goto_functionst &goto_functions, message_handlert &message_handler)
void	goto_check_c (const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
void	goto_check_c (const optionst &options, goto_modelt &goto_model, message_handlert &message_handler)

Detailed Description

Program Transformation.

Definition in file goto_check_c.h.

Macro Definition Documentation

HELP_GOTO_CHECK

#define HELP_GOTO_CHECK

Definition at line 57 of file goto_check_c.h.

OPT_GOTO_CHECK

#define OPT_GOTO_CHECK

Value:

  "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)"     \
  "(div-by-zero-check)(float-div-by-zero-check)"                               \
  "(enum-range-check)"                                                         \
  "(signed-overflow-check)(unsigned-overflow-check)"                           \
  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
  "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
  "(pointer-primitive-check)"                                                  \
  "(retain-trivial-checks)"                                                    \
  "(error-label):"                                                             \
  "(no-assertions)(no-assumptions)"                                            \
  "(assert-to-assume)"                                                         \
  "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)"              \
  "(no-pointer-primitive-check)(no-undefined-shift-check)"                     \
  "(no-div-by-zero-check)"

Definition at line 40 of file goto_check_c.h.

PARSE_OPTION_OVERRIDE

#define PARSE_OPTION_OVERRIDE	(		cmdline,
			options,
			option
	)

Value:

  if(cmdline.isset(option))                                                    \
    options.set_option(option, true);                                          \
  if(cmdline.isset("no-" option))                                              \
    options.set_option(option, false);                                         \
  (void)0

Definition at line 101 of file goto_check_c.h.

PARSE_OPTIONS_GOTO_CHECK

#define PARSE_OPTIONS_GOTO_CHECK	(		cmdline,
			options
	)

Value:

  options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
  options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
  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("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) */ \
  options.set_option("retain-trivial-checks", \
                     cmdline.isset("retain-trivial-checks")); \
  options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
  if(cmdline.isset("error-label")) \
    options.set_option("error-label", cmdline.get_values("error-label"));      \
  PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
  PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
  PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
  PARSE_OPTION_OVERRIDE(cmdline, options, "float-div-by-zero-check"); \
  PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
  PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \
  PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \
  (void)0

Definition at line 109 of file goto_check_c.h.

Function Documentation

goto_check_c() [1/3]

void goto_check_c	(	const irep_idt &	function_identifier,
		goto_functionst::goto_functiont &	goto_function,
		const namespacet &	ns,
		const optionst &	options,
		message_handlert &	message_handler
	)

Definition at line 2472 of file goto_check_c.cpp.

goto_check_c() [2/3]

void goto_check_c	(	const namespacet &	ns,
		const optionst &	options,
		goto_functionst &	goto_functions,
		message_handlert &	message_handler
	)

Definition at line 2483 of file goto_check_c.cpp.

goto_check_c() [3/3]

void goto_check_c	(	const optionst &	options,
		goto_modelt &	goto_model,
		message_handlert &	message_handler
	)

Definition at line 2499 of file goto_check_c.cpp.