cprover
symex_dereference_state.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
13 #define CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
14 
16 
17 #include "goto_symex.h"
18 
26 {
27 public:
29  : state(_state), ns(ns)
30  {
31  }
32 
33 protected:
35  const namespacet &ns;
36 
37  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
38  void get_value_set(const exprt &expr, value_setst::valuest &value_set)
39  const override;
40 
41  std::vector<exprt> get_value_set(const exprt &expr) const override;
42 
43  const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
44 };
45 
46 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
symex_dereference_statet::state
goto_symext::statet & state
Definition: symex_dereference_state.h:34
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:28
symex_dereference_statet::get_or_create_failed_symbol
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Get or create a failed symbol for the given pointer-typed expression.
Definition: symex_dereference_state.cpp:35
exprt
Base class for all expressions.
Definition: expr.h:53
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_symex.h
Symbolic Execution.
symex_dereference_statet::ns
const namespacet & ns
Definition: symex_dereference_state.h:35
symex_dereference_statet
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Definition: symex_dereference_state.h:26
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
symex_dereference_statet::get_value_set
void get_value_set(const exprt &expr, value_setst::valuest &value_set) const override
Just forwards a value-set query to state.value_set
Definition: symex_dereference_state.cpp:85
value_setst
Definition: value_sets.h:22
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
symbolt
Symbol table entry.
Definition: symbol.h:28
dereference_callback.h
Pointer Dereferencing.
symex_dereference_statet::symex_dereference_statet
symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)
Definition: symex_dereference_state.h:28