cprover
three_way_merge_abstract_interpreter.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Variable sensitivity domain
4 
5 Author: Martin Brain, martin.brain@cs.ox.ac.uk
6 
7 Date: August 2020
8 
9 \*******************************************************************/
10 
21 
22 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_THREE_WAY_MERGE_ABSTRACT_INTERPRETER_H
23 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_THREE_WAY_MERGE_ABSTRACT_INTERPRETER_H
24 
25 #include <analyses/ai.h>
26 
28 {
29 public:
31  std::unique_ptr<ai_history_factory_baset> &&hf,
32  std::unique_ptr<ai_domain_factory_baset> &&df,
33  std::unique_ptr<ai_storage_baset> &&st)
34  : ai_recursive_interproceduralt(std::move(hf), std::move(df), std::move(st))
35  {
36  }
37 
38 protected:
39  // Like ai_recursive_interproceduralt we hook the handling of function calls.
40  // Much of this is the same as ai_recursive_interproceduralt's handling but
41  // on function return the three-way merge is used.
43  const irep_idt &calling_function_id,
44  trace_ptrt p_call,
45  locationt l_return,
46  const irep_idt &callee_function_id,
47  working_sett &working_set,
48  const goto_programt &callee,
49  const goto_functionst &goto_functions,
50  const namespacet &ns) override;
51 };
52 
53 #endif
Abstract Interpretation.
goto_programt::const_targett locationt
Definition: ai.h:127
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai.h:124
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition: ai.h:415
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)
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92