Insert final assert false into a function. More...

#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:

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.

Macro Definition Documentation

#define HELP_INSERT_FINAL_ASSERT_FALSE

Value:

" {y--insert-final-assert-false} {ufunction} \t " \

"generate assert(false) at end of function {ufunction}\n"

#define OPT_INSERT_FINAL_ASSERT_FALSE "(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.