CBMC
label_function_pointer_call_sites.h
Go to the documentation of this file.
1 /*******************************************************************\
2 Module: Label function pointer call sites
3 Author: Diffblue Ltd.
4 \*******************************************************************/
5 
9 
10 #ifndef CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H
11 #define CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H
12 
13 class goto_modelt;
14 
28 void label_function_pointer_call_sites(goto_modelt &goto_model);
29 
30 #endif // CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H
goto_modelt
Definition: goto_model.h:27
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:
Definition: label_function_pointer_call_sites.cpp:15