insert_final_assert_false.cpp File Reference

#include "insert_final_assert_false.h"
#include <goto-programs/goto_model.h>
#include <util/irep.h>
#include <iterator>
#include <list>

Include dependency graph for insert_final_assert_false.cpp:

Go to the source code of this file.

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.cpp.

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.