dfcc_pointer_equals.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dynamic frame condition checking for function contracts
 
Author: Remi Delmas, delmasrd@amazon.com
Date: Jan 2025
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H
 
#include <util/message.h>
 
#include <goto-programs/goto_program.h>
 
class goto_modelt;
class message_handlert;
class dfcc_libraryt;
class dfcc_cfg_infot;
class exprt;

void rewrite_equal_exprt_to_pointer_equals(exprt &expr);

class dfcc_pointer_equalst
{
public:
  dfcc_pointer_equalst(
    dfcc_libraryt &library,
    message_handlert &message_handler);

  void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info);

  void rewrite_calls(
    goto_programt &program,
    goto_programt::targett first_instruction,
    const goto_programt::targett &last_instruction,
    dfcc_cfg_infot cfg_info);
 
protected:
  dfcc_libraryt &library;
  message_handlert &message_handler;
  messaget log;
};
 
#endif