Label function pointer call sites across a goto model. More...
#include "label_function_pointer_call_sites.h"#include <util/pointer_expr.h>#include "goto_model.h"
Include dependency graph for label_function_pointer_call_sites.cpp: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.
Definition in file label_function_pointer_call_sites.cpp.
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:
- A "normal" function call to a concrete function
- 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.
