#include <string>
#include <util/message.h>

Include dependency graph for insert_final_assert_false.h:

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

Classes
class	insert_final_assert_falset

Macros
#define	OPT_INSERT_FINAL_ASSERT_FALSE "(insert-final-assert-false):"

#define	HELP_INSERT_FINAL_ASSERT_FALSE

Functions
bool	insert_final_assert_false (goto_modelt &goto_model, const std::string &function_to_instrument, message_handlert &message_handler)
	Transform a goto program by inserting assert(false) at the end of a given function `function_to_instrument`. More...

Detailed Description

Insert final assert false into a function

Definition in file insert_final_assert_false.h.

Macro Definition Documentation

◆ HELP_INSERT_FINAL_ASSERT_FALSE

#define HELP_INSERT_FINAL_ASSERT_FALSE

Value:

  " --insert-final-assert-false <function>\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              generate assert(false) at end of function\n"

Definition at line 53 of file insert_final_assert_false.h.

◆ OPT_INSERT_FINAL_ASSERT_FALSE

#define OPT_INSERT_FINAL_ASSERT_FALSE "(insert-final-assert-false):"

Definition at line 50 of file insert_final_assert_false.h.

Function Documentation

◆ insert_final_assert_false()

bool insert_final_assert_false	(	goto_modelt &	goto_model,
		const std::string &	function_to_instrument,
		message_handlert &	message_handler
	)

Transform a goto program by inserting assert(false) at the end of a given function function_to_instrument.

The instrumented assert is expected to fail. If it does not then this may indicate inconsistent assumptions.

Parameters

goto_model	The goto program to modify.
function_to_instrument	Name of the function to instrument.
message_handler	Handles logging.

Returns: false on success

Definition at line 53 of file insert_final_assert_false.cpp.

Classes