dfcc_lift_memory_predicates.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dynamic frame condition checking for function contracts
 
Author: Remi Delmas, delmasrd@amazon.com
Date: November 2022
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
 
#include <util/message.h>
 
#include <goto-programs/goto_program.h>
 
#include <map>
#include <set>
 
class dfcc_libraryt;
class dfcc_instrumentt;
class message_handlert;
class goto_modelt;
class exprt;
class replace_symbolt;
 
class dfcc_lift_memory_predicatest
{
public:
  dfcc_lift_memory_predicatest(
    goto_modelt &goto_model,
    dfcc_libraryt &library,
    dfcc_instrumentt &instrument,
    message_handlert &message_handler);
 
  std::set<irep_idt>
  lift_predicates(std::set<irep_idt> &discovered_function_pointer_contracts);
 
  void fix_calls(goto_programt &program);
 
  void fix_calls(
    goto_programt &program,
    goto_programt::targett first_instruction,
    const goto_programt::targett &last_instruction);
 
protected:
  goto_modelt &goto_model;
  dfcc_libraryt &library;
  dfcc_instrumentt &instrument;
  messaget log;
  // index of lifted parameters for lifted functions
  std::map<irep_idt, std::set<std::size_t>> lifted_parameters;
 
  bool calls_memory_predicates(
    const goto_programt &goto_program,
    const std::set<irep_idt> &predicates);
 
  void lift_predicate(
    const irep_idt &function_id,
    std::set<irep_idt> &discovered_function_pointer_contracts);
 
  void lift_parameters_and_update_body(
    const irep_idt &function_id,
    std::set<irep_idt> &discovered_function_pointer_contracts);
 
  void add_pointer_type(
    const irep_idt &function_id,
    const std::size_t parameter_rank,
    replace_symbolt &replace_lifted_param);
 
  void collect_parameters_to_lift(const irep_idt &function_id);
 
  bool is_lifted_function(const irep_idt &function_id);
};
class dfcc_lift_memory_predicatest {…};
 
#endif