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 <ansi-c/goto-conversion/goto_convert_class.h>
 
#include <util/message.h>
#include <util/namespace.h>
#include <util/std_expr.h>
 
#include "dfcc_contract_mode.h"
 
#include <set>
 
class goto_modelt;
class message_handlert;
class dfcc_libraryt;
class code_with_contract_typet;
class conditional_target_group_exprt;
 
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