dfcc_is_fresh.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_IS_FRESH_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_IS_FRESH_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_is_fresht
{
public:
  dfcc_is_fresht(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