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