dfcc_obeys_contract.h

Go to the documentation of this file.

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

 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_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;

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

  void rewrite_calls(
    goto_programt &program,
    dfcc_cfg_infot &cfg_info,
    std::set<irep_idt> &function_pointer_contracts);

  void rewrite_calls(
    goto_programt &program,
    goto_programt::targett first_instruction,
    const goto_programt::targett &last_instruction,
    dfcc_cfg_infot &cfg_info,
    std::set<irep_idt> &function_pointer_contracts);
 
protected:
  dfcc_libraryt &library;
  message_handlert &message_handler;
  messaget log;

  void get_contract_name(
    const exprt &expr,
    std::set<irep_idt> &function_pointer_contracts);
};
 
#endif