dfcc_spec_functions.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dynamic frame condition checking for function contracts
 
Author: Remi Delmas, delmasrd@amazon.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
 
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/message.h>
#include <util/std_expr.h>
#include <util/std_types.h>
 
#include "dfcc_library.h"
#include "dfcc_utils.h"
 
#include <map>
#include <set>
 
class goto_modelt;
class message_handlert;
class symbolt;
class conditional_target_group_exprt;
 
class dfcc_spec_functionst
{
public:
  dfcc_spec_functionst(
    goto_modelt &goto_model,
    message_handlert &message_handler,
    dfcc_libraryt &library);
 
  void generate_havoc_function(
    const irep_idt &function_id,
    const irep_idt &havoc_function_id,
    std::size_t &nof_targets);
 
  void generate_havoc_instructions(
    const irep_idt &function_id,
    const goto_programt &original_program,
    const exprt &write_set_to_havoc,
    goto_programt &havoc_program,
    std::size_t &nof_targets);
 
  void to_spec_assigns_function(
    const irep_idt &function_id,
    std::size_t &nof_targets);
 
  void to_spec_assigns_instructions(
    const exprt &write_set_to_fill,
    const irep_idt &language_mode,
    goto_programt &program,
    std::size_t &nof_targets);
 
  void
  to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets);
 
  void to_spec_frees_instructions(
    const exprt &write_set_to_fill,
    const irep_idt &language_mode,
    goto_programt &program,
    std::size_t &nof_targets);
 
protected:
  goto_modelt &goto_model;
  message_handlert &message_handler;
  messaget log;
  dfcc_libraryt &library;
  namespacet ns;
 
  const typet &get_target_type(const exprt &expr);
};
 
#endif