Constify dereference_callbackt

has_failed_symbol is renamed to get_or_create_failed_symbol to emphasise that that method
really *may* have side-effects.

Author: smowton

src/goto-symex/symex_dereference_state.cpp

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 
-bool symex_dereference_statet::has_failed_symbol(
+bool symex_dereference_statet::get_or_create_failed_symbol(
   const exprt &expr,
   const symbolt *&symbol)
 {
@@ -70,7 +70,7 @@ bool symex_dereference_statet::has_failed_symbol(
 
 void symex_dereference_statet::get_value_set(
   const exprt &expr,
-  value_setst::valuest &value_set)
+  value_setst::valuest &value_set) const
 {
   state.value_set.get_value_set(expr, value_set, goto_symex.ns);
 

src/goto-symex/symex_dereference_state.h

@@ -29,13 +29,14 @@ class symex_dereference_statet:
   }
 
 protected:
-  goto_symext &goto_symex;
+  const goto_symext &goto_symex;
   goto_symext::statet &state;
 
-  void
-  get_value_set(const exprt &expr, value_setst::valuest &value_set) override;
+  void get_value_set(const exprt &expr, value_setst::valuest &value_set)
+    const override;
 
-  bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override;
+  bool get_or_create_failed_symbol(const exprt &expr, const symbolt *&symbol)
+    override;
 };
 
 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H

src/pointer-analysis/dereference_callback.h

@@ -29,13 +29,11 @@ class dereference_callbackt
 public:
   virtual ~dereference_callbackt() = default;
 
-  virtual void get_value_set(
-    const exprt &expr,
-    value_setst::valuest &value_set)=0;
+  virtual void
+  get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
 
-  virtual bool has_failed_symbol(
-    const exprt &expr,
-    const symbolt *&symbol)=0;
+  virtual bool
+  get_or_create_failed_symbol(const exprt &expr, const symbolt *&symbol) = 0;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_DEREFERENCE_CALLBACK_H

src/pointer-analysis/goto_program_dereference.cpp

@@ -24,7 +24,7 @@ Author: Daniel Kroening, [email protected]
 ///   `failed_symbol` comment
 /// \return true when `expr` is a symbol, whose type contains a `failed_symbol`
 ///   comment which exists in the namespace.
-bool goto_program_dereferencet::has_failed_symbol(
+bool goto_program_dereferencet::get_or_create_failed_symbol(
   const exprt &expr,
   const symbolt *&symbol)
 {
@@ -225,7 +225,7 @@ void goto_program_dereferencet::dereference_rec(
 /// \param [out] dest: gets the value set
 void goto_program_dereferencet::get_value_set(
   const exprt &expr,
-  value_setst::valuest &dest)
+  value_setst::valuest &dest) const
 {
   value_sets.get_values(current_function, current_target, expr, dest);
 }

src/pointer-analysis/goto_program_dereference.h

@@ -69,15 +69,17 @@ class goto_program_dereferencet:protected dereference_callbackt
   DEPRECATED("Unused")
   virtual bool is_valid_object(const irep_idt &identifier);
 
-  bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override;
+  bool get_or_create_failed_symbol(const exprt &expr, const symbolt *&symbol)
+    override;
 
   DEPRECATED("Unused")
   virtual void dereference_failure(
     const std::string &property,
     const std::string &msg,
     const guardt &guard);
 
-  void get_value_set(const exprt &expr, value_setst::valuest &dest) override;
+  void
+  get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
   void dereference_instruction(
     goto_programt::targett target,

src/pointer-analysis/value_set_dereference.cpp

@@ -126,8 +126,7 @@ exprt value_set_dereferencet::dereference(
     const symbolt *failed_symbol;
     exprt failure_value;
 
-    if(dereference_callback.has_failed_symbol(
-         pointer, failed_symbol))
+    if(dereference_callback.get_or_create_failed_symbol(pointer, failed_symbol))
     {
       // yes!
       failure_value=failed_symbol->symbol_expr();