value_set_fi_fp_removal.cpp File Reference

#include "value_set_fi_fp_removal.h"
#include <util/message.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_function_pointers.h>
#include <pointer-analysis/value_set_analysis_fi.h>

Include dependency graph for value_set_fi_fp_removal.cpp:

Go to the source code of this file.

Functions
void	value_set_fi_fp_removal (goto_modelt &goto_model, message_handlert &message_handler)
	Builds the flow-insensitive value set for all function pointers and replaces function pointers with a non-deterministic switch between this set. More...

Function Documentation

value_set_fi_fp_removal()

void value_set_fi_fp_removal	(	goto_modelt &	goto_model,
		message_handlert &	message_handler
	)

Builds the flow-insensitive value set for all function pointers and replaces function pointers with a non-deterministic switch between this set.

If the set is empty, the function pointer is not removed. Thus remove_function_pointers should be run after this to

Parameters

goto_model	goto model to be modified
message_handler	message handler for status output

Definition at line 20 of file value_set_fi_fp_removal.cpp.