three_way_merge_abstract_interpreter.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Variable sensitivity domain
 
Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
Date: August 2020
 
\*******************************************************************/

 
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_THREE_WAY_MERGE_ABSTRACT_INTERPRETER_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_THREE_WAY_MERGE_ABSTRACT_INTERPRETER_H
 
#include <analyses/ai.h>
 
class ai_three_way_merget : public ai_recursive_interproceduralt
{
public:
  ai_three_way_merget(
    std::unique_ptr<ai_history_factory_baset> &&hf,
    std::unique_ptr<ai_domain_factory_baset> &&df,
    std::unique_ptr<ai_storage_baset> &&st,
    message_handlert &mh)
    : ai_recursive_interproceduralt(
        std::move(hf),
        std::move(df),
        std::move(st),
        mh)
  {
  }
 
protected:
  // Like ai_recursive_interproceduralt we hook the handling of function calls.
  // Much of this is the same as ai_recursive_interproceduralt's handling but
  // on function return the three-way merge is used.
  bool visit_edge_function_call(
    const irep_idt &calling_function_id,
    trace_ptrt p_call,
    locationt l_return,
    const irep_idt &callee_function_id,
    working_sett &working_set,
    const goto_programt &callee,
    const goto_functionst &goto_functions,
    const namespacet &ns) override;
};
 
#endif