Remove unused guard argument from dereference

This argument was never actually used.

Author: romainbrenguier

src/goto-symex/symex_clean_expr.cpp

@@ -125,7 +125,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   value_set_dereferencet dereference(
     ns, state.symbol_table, symex_dereference_state, language_mode, false);
 
-  expr = dereference.dereference(expr, guardt{true_exprt()});
+  expr = dereference.dereference(expr);
 
   ::process_array_expr(expr, symex_config.simplify_opt, ns);
 }

src/goto-symex/symex_dereference.cpp

@@ -234,7 +234,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
       expr_is_not_null);
 
     // std::cout << "**** " << format(tmp1) << '\n';
-    exprt tmp2 = dereference.dereference(tmp1, guardt(true_exprt()));
+    exprt tmp2 = dereference.dereference(tmp1);
     // std::cout << "**** " << format(tmp2) << '\n';
 
     expr.swap(tmp2);

src/pointer-analysis/goto_program_dereference.cpp

@@ -188,7 +188,7 @@ void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
 
     dereference_location=expr.find_source_location();
 
-    exprt tmp = dereference.dereference(expr.op0(), guard);
+    exprt tmp = dereference.dereference(expr.op0());
 
     expr.swap(tmp);
   }
@@ -206,7 +206,7 @@ void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
       exprt tmp1(ID_plus, expr.op0().type());
       tmp1.operands().swap(expr.operands());
 
-      exprt tmp2 = dereference.dereference(tmp1, guard);
+      exprt tmp2 = dereference.dereference(tmp1);
       tmp2.swap(expr);
     }
   }

src/pointer-analysis/goto_program_dereference.h

@@ -19,6 +19,8 @@ Author: Daniel Kroening, [email protected]
 #include "value_sets.h"
 #include "value_set_dereference.h"
 
+class guardt;
+
 /// Wrapper for functions removing dereferences in expressions contained in
 /// a goto program.
 class goto_program_dereferencet:protected dereference_callbackt

src/pointer-analysis/value_set_dereference.cpp

@@ -32,9 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
-exprt value_set_dereferencet::dereference(
-  const exprt &pointer,
-  const guardt &guard)
+exprt value_set_dereferencet::dereference(const exprt &pointer)
 {
   if(pointer.type().id()!=ID_pointer)
     throw "dereference expected pointer type, but got "+
@@ -44,16 +42,8 @@ exprt value_set_dereferencet::dereference(
   if(pointer.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(pointer);
-    // push down the if
-    guardt true_guard=guard;
-    guardt false_guard=guard;
-
-    true_guard.add(if_expr.cond());
-    false_guard.add(not_exprt(if_expr.cond()));
-
-    exprt true_case = dereference(if_expr.true_case(), true_guard);
-    exprt false_case = dereference(if_expr.false_case(), false_guard);
-
+    exprt true_case = dereference(if_expr.true_case());
+    exprt false_case = dereference(if_expr.false_case());
     return if_exprt(if_expr.cond(), true_case, false_case);
   }
 

src/pointer-analysis/value_set_dereference.h

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include "dereference_callback.h"
 
 class symbol_tablet;
-class guardt;
 class optionst;
 class symbolt;
 
@@ -55,7 +54,7 @@ class value_set_dereferencet final
   /// \param pointer: A pointer-typed expression, to
   ///        be dereferenced.
   /// \param guard: A guard, which is assumed to hold when dereferencing.
-  exprt dereference(const exprt &pointer, const guardt &guard);
+  exprt dereference(const exprt &pointer);
 
 private:
   const namespacet &ns;