dfcc_contract_clauses_codegen.h

Go to the documentation of this file.

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

 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
 
#include <util/expr.h>
#include <util/message.h>
#include <util/namespace.h>
 
class conditional_target_group_exprt;
class dfcc_libraryt;
class goto_modelt;
class goto_programt;

class dfcc_contract_clauses_codegent
{
public:
  dfcc_contract_clauses_codegent(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    dfcc_libraryt &library);

  void gen_spec_assigns_instructions(
    const irep_idt &language_mode,
    const exprt::operandst &assigns_clause,
    goto_programt &dest);

  void gen_spec_frees_instructions(
    const irep_idt &language_mode,
    const exprt::operandst &frees_clause,
    goto_programt &dest);
 
protected:
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
  dfcc_libraryt &library;
  namespacet ns;

  void encode_assignable_target_group(
    const irep_idt &language_mode,
    const conditional_target_group_exprt &group,
    goto_programt &dest);

  void encode_assignable_target(
    const irep_idt &language_mode,
    const exprt &target,
    goto_programt &dest);

  void encode_freeable_target_group(
    const irep_idt &language_mode,
    const conditional_target_group_exprt &group,
    goto_programt &dest);

  void encode_freeable_target(
    const irep_idt &language_mode,
    const exprt &target,
    goto_programt &dest);

  void inline_and_check_warnings(goto_programt &goto_program);
};
 
#endif