dfcc_contract_functions.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_CONTRACT_FUNCTIONS_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
 
#include <util/message.h>
#include <util/namespace.h>
 
class code_with_contract_typet;
class dfcc_contract_clauses_codegent;
class dfcc_instrumentt;
class dfcc_libraryt;
class dfcc_spec_functionst;
class goto_modelt;

class dfcc_contract_functionst
{
public:
  dfcc_contract_functionst(
    const symbolt &pure_contract_symbol,
    goto_modelt &goto_model,
    message_handlert &message_handler,
    dfcc_libraryt &library,
    dfcc_spec_functionst &spec_functions,
    dfcc_contract_clauses_codegent &contract_clauses_codegen,
    dfcc_instrumentt &instrument);

  void instrument_without_loop_contracts_check_no_pointer_contracts(
    const irep_idt &spec_function_id);

  const symbolt &get_spec_assigns_function_symbol() const;

  const symbolt &get_spec_assigns_havoc_function_symbol() const;

  const symbolt &get_spec_frees_function_symbol() const;

  const std::size_t get_nof_assigns_targets() const;

  const std::size_t get_nof_frees_targets() const;

  const symbolt &pure_contract_symbol;

  const code_with_contract_typet &code_with_contract;

  const irep_idt spec_assigns_function_id;

  const irep_idt spec_assigns_havoc_function_id;

  const irep_idt spec_frees_function_id;

  const irep_idt &language_mode;
 
protected:
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
  dfcc_libraryt &library;
  dfcc_spec_functionst &spec_functions;
  dfcc_contract_clauses_codegent &contract_clauses_codegen;
  dfcc_instrumentt &instrument;
  namespacet ns;
  std::size_t nof_assigns_targets;
  std::size_t nof_frees_targets;

  void gen_spec_assigns_function();

  void gen_spec_frees_function();
};
 
#endif