Merge pull request #4188 from romainbrenguier/clean-up/unused-guards

Clean-up use of guards

Author: romainbrenguier

src/goto-instrument/rw_set.cpp

@@ -79,14 +79,15 @@ void _rw_set_loct::compute()
 void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)
 {
   read(rhs);
-  read_write_rec(lhs, false, true, "", guardt(true_exprt()));
+  read_write_rec(lhs, false, true, "", exprt::operandst());
 }
 
 void _rw_set_loct::read_write_rec(
   const exprt &expr,
-  bool r, bool w,
+  bool r,
+  bool w,
   const std::string &suffix,
-  const guardt &guard)
+  const exprt::operandst &guard_conjuncts)
 {
   if(expr.id()==ID_symbol)
   {
@@ -96,16 +97,16 @@ void _rw_set_loct::read_write_rec(
 
     if(r)
     {
-      const auto &entry =
-        r_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr()));
+      const auto &entry = r_entries.emplace(
+        object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
 
       track_deref(entry.first->second, true);
     }
 
     if(w)
     {
-      const auto &entry =
-        w_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr()));
+      const auto &entry = w_entries.emplace(
+        object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
 
       track_deref(entry.first->second, false);
     }
@@ -114,20 +115,21 @@ void _rw_set_loct::read_write_rec(
   {
     assert(expr.operands().size()==1);
     const std::string &component_name=expr.get_string(ID_component_name);
-    read_write_rec(expr.op0(), r, w, "."+component_name+suffix, guard);
+    read_write_rec(
+      expr.op0(), r, w, "." + component_name + suffix, guard_conjuncts);
   }
   else if(expr.id()==ID_index)
   {
     // we don't distinguish the array elements for now
     assert(expr.operands().size()==2);
-    read_write_rec(expr.op0(), r, w, "[]"+suffix, guard);
-    read(expr.op1(), guard);
+    read_write_rec(expr.op0(), r, w, "[]" + suffix, guard_conjuncts);
+    read(expr.op1(), guard_conjuncts);
   }
   else if(expr.id()==ID_dereference)
   {
     assert(expr.operands().size()==1);
     set_track_deref();
-    read(expr.op0(), guard);
+    read(expr.op0(), guard_conjuncts);
 
     exprt tmp=expr;
     #ifdef LOCAL_MAY
@@ -147,25 +149,25 @@ void _rw_set_loct::read_write_rec(
         entryt &entry=r_entries[object];
         entry.object=object;
         entry.symbol_expr=symbol_exprt(ID_unknown);
-        entry.guard=guard.as_expr(); // should 'OR'
+        entry.guard = conjunction(guard_conjuncts); // should 'OR'
 
         continue;
       }
       #endif
-      read_write_rec(*it, r, w, suffix, guard);
+      read_write_rec(*it, r, w, suffix, guard_conjuncts);
     }
     #else
     dereference(function_id, target, tmp, ns, value_sets);
 
-    read_write_rec(tmp, r, w, suffix, guard);
-    #endif
+    read_write_rec(tmp, r, w, suffix, guard_conjuncts);
+#endif
 
     reset_track_deref();
   }
   else if(expr.id()==ID_typecast)
   {
     assert(expr.operands().size()==1);
-    read_write_rec(expr.op0(), r, w, suffix, guard);
+    read_write_rec(expr.op0(), r, w, suffix, guard_conjuncts);
   }
   else if(expr.id()==ID_address_of)
   {
@@ -174,20 +176,20 @@ void _rw_set_loct::read_write_rec(
   else if(expr.id()==ID_if)
   {
     assert(expr.operands().size()==3);
-    read(expr.op0(), guard);
+    read(expr.op0(), guard_conjuncts);
 
-    guardt true_guard(guard);
-    true_guard.add(expr.op0());
+    exprt::operandst true_guard = guard_conjuncts;
+    true_guard.push_back(expr.op0());
     read_write_rec(expr.op1(), r, w, suffix, true_guard);
 
-    guardt false_guard(guard);
-    false_guard.add(not_exprt(expr.op0()));
+    exprt::operandst false_guard = guard_conjuncts;
+    false_guard.push_back(not_exprt(expr.op0()));
     read_write_rec(expr.op2(), r, w, suffix, false_guard);
   }
   else
   {
     forall_operands(it, expr)
-      read_write_rec(*it, r, w, suffix, guard);
+      read_write_rec(*it, r, w, suffix, guard_conjuncts);
   }
 }
 

src/goto-instrument/rw_set.h

@@ -18,7 +18,6 @@ Date: February 2006
 #include <vector>
 #include <set>
 
-#include <util/guard.h>
 #include <util/std_expr.h>
 
 #include <goto-programs/goto_model.h>
@@ -158,17 +157,17 @@ class _rw_set_loct:public rw_set_baset
 
   void read(const exprt &expr)
   {
-    read_write_rec(expr, true, false, "", guardt(true_exprt()));
+    read_write_rec(expr, true, false, "", exprt::operandst());
   }
 
-  void read(const exprt &expr, const guardt &guard)
+  void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
   {
-    read_write_rec(expr, true, false, "", guard);
+    read_write_rec(expr, true, false, "", guard_conjuncts);
   }
 
   void write(const exprt &expr)
   {
-    read_write_rec(expr, false, true, "", guardt(true_exprt()));
+    read_write_rec(expr, false, true, "", exprt::operandst());
   }
 
   void compute();
@@ -177,9 +176,10 @@ class _rw_set_loct:public rw_set_baset
 
   void read_write_rec(
     const exprt &expr,
-    bool r, bool w,
+    bool r,
+    bool w,
     const std::string &suffix,
-    const guardt &guard);
+    const exprt::operandst &guard_conjuncts);
 };
 
 class rw_set_loct:public _rw_set_loct

src/goto-programs/goto_convert_class.h

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 
 #include <util/allocate_objects.h>
-#include <util/guard.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/replace_expr.h>

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);