label_function_pointer_call_sites.h File Reference

Label function pointer call sites across a goto model. More...

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

Go to the source code of this file.

Functions
void	label_function_pointer_call_sites (goto_modelt &goto_model)
	This ensures that call instructions can be only one of two things: More...

Detailed Description

Label function pointer call sites across a goto model.

See also

simplify_function_pointers

Definition in file label_function_pointer_call_sites.h.

Function Documentation

label_function_pointer_call_sites()

void label_function_pointer_call_sites

(

goto_modelt &

goto_model

)

This ensures that call instructions can be only one of two things:

1. A "normal" function call to a concrete function
2. A dereference of a symbol expression of a function pointer type

This makes following stages dealing with function calls easier, because they only need to be able to handle these two cases.

It does this by replacing all CALL instructions to function pointers with an assignment to a new function pointer variable followed by a call to that new function pointer. The name of the introduced variable follows the pattern [function_name].function_pointer_call.[N], where N is the nth call to a function pointer in the function function_name.

Definition at line 15 of file label_function_pointer_call_sites.cpp.