remove_function_pointers.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Remove Indirect Function Calls
 
Author: Daniel Kroening
 
Date: June 2003
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
#define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
 
#include "goto_program.h"
 
#include <unordered_set>
 
class goto_functionst;
class goto_modelt;
class message_handlert;
class symbol_tablet;
 
// remove indirect function calls
// and replace by case-split
void remove_function_pointers(
  message_handlert &_message_handler,
  goto_modelt &goto_model,
  bool only_remove_const_fps);
 
void remove_function_pointer(
  message_handlert &message_handler,
  symbol_tablet &symbol_table,
  goto_programt &goto_program,
  const irep_idt &function_id,
  goto_programt::targett target,
  const std::unordered_set<symbol_exprt, irep_hash> &functions);
 
bool function_is_type_compatible(
  bool return_value_used,
  const code_typet &call_type,
  const code_typet &function_type,
  const namespacet &ns);
 
bool has_function_pointers(const goto_functionst &);
 
bool has_function_pointers(const goto_modelt &);
 
#endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H