value_set_fi_fp_removal.h File Reference

flow insensitive value set function pointer removal More...

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

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

Detailed Description

flow insensitive value set function pointer removal

Definition in file value_set_fi_fp_removal.h.

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.