Remove guardt default constructor

This makes the code clearer when it assumes that the default guard
corresponds to true.

Author: romainbrenguier

src/analyses/goto_check.cpp

@@ -1632,7 +1632,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 
 void goto_checkt::check(const exprt &expr)
 {
-  guardt guard;
+  guardt guard{true_exprt{}};
   check_rec(expr, guard, false);
 }
 
@@ -1762,7 +1762,7 @@ void goto_checkt::goto_check(
             "pointer dereference",
             i.source_location,
             pointer,
-            guardt());
+            guardt(true_exprt()));
         }
       }
 
@@ -1800,7 +1800,7 @@ void goto_checkt::goto_check(
           "pointer dereference",
           i.source_location,
           pointer,
-          guardt());
+          guardt(true_exprt()));
       }
 
       // this has no successor
@@ -1881,7 +1881,7 @@ void goto_checkt::goto_check(
           "memory-leak",
           source_location,
           eq,
-          guardt());
+          guardt(true_exprt()));
       }
     }
 

src/analyses/goto_rw.h

@@ -370,7 +370,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
     get_modet mode,
     const exprt &expr) override
   {
-    guard = guardt();
+    guard = guardt(true_exprt());
 
     rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
   }
@@ -384,7 +384,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
   }
 
 protected:
-  guardt guard;
+  guardt guard = guardt(true_exprt());
 
   using rw_range_sett::get_objects_rec;
 

src/goto-instrument/rw_set.cpp

@@ -79,7 +79,7 @@ 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());
+  read_write_rec(lhs, false, true, "", guardt(true_exprt()));
 }
 
 void _rw_set_loct::read_write_rec(

src/goto-instrument/rw_set.h

@@ -149,7 +149,7 @@ class _rw_set_loct:public rw_set_baset
 
   void read(const exprt &expr)
   {
-    read_write_rec(expr, true, false, "", guardt());
+    read_write_rec(expr, true, false, "", guardt(true_exprt()));
   }
 
   void read(const exprt &expr, const guardt &guard)
@@ -159,7 +159,7 @@ class _rw_set_loct:public rw_set_baset
 
   void write(const exprt &expr)
   {
-    read_write_rec(expr, false, true, "", guardt());
+    read_write_rec(expr, false, true, "", guardt(true_exprt()));
   }
 
   void compute();

src/goto-symex/goto_symex_state.cpp

@@ -389,8 +389,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // see whether we are within an atomic section
   if(atomic_section_id!=0)
   {
-    guardt write_guard;
-    write_guard.add(false_exprt());
+    guardt write_guard{false_exprt{}};
 
     const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
     if(a_s_writes!=written_in_atomic_section.end())
@@ -414,8 +413,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     // we cannot determine for sure that there has been a write already
     // so generate a read even if l1_identifier has been written on
     // all branches flowing into this read
-    guardt read_guard;
-    read_guard.add(false_exprt());
+    guardt read_guard{false_exprt{}};
 
     a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
     for(const auto &a_s_read_guard : a_s_read.second)
@@ -433,11 +431,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
     guardt cond = read_guard;
     if(!no_write.op().is_false())
-    {
-      guardt no_write_guard;
-      no_write_guard.add(no_write.op());
-      cond |= no_write_guard;
-    }
+      cond |= guardt{no_write.op()};
 
     if_exprt tmp(cond.as_expr(), ssa_l1, ssa_l1);
     set_l2_indices(to_ssa_expr(tmp.true_case()), ns);

src/goto-symex/goto_symex_state.h

@@ -54,7 +54,7 @@ class goto_symex_statet final
   /// distance from entry
   unsigned depth;
 
-  guardt guard;
+  guardt guard{true_exprt{}};
   symex_targett::sourcet source;
   symex_target_equationt *symex_target;
 
@@ -254,7 +254,7 @@ class goto_symex_statet final
   struct threadt
   {
     goto_programt::const_targett pc;
-    guardt guard;
+    guardt guard{true_exprt{}};
     call_stackt call_stack;
     std::map<irep_idt, unsigned> function_frame;
     unsigned atomic_section_id = 0;

src/goto-symex/symex_assign.cpp

@@ -89,7 +89,7 @@ void goto_symext::symex_assign(
     if(state.source.pc->source_location.get_hide())
       assignment_type=symex_targett::assignment_typet::HIDDEN;
 
-    guardt guard; // NOT the state guard!
+    guardt guard{true_exprt{}}; // NOT the state guard!
     symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
   }
 }

src/goto-symex/symex_dereference.cpp

@@ -384,7 +384,7 @@ void goto_symext::dereference(
   state.rename(expr, ns, goto_symex_statet::L1);
 
   // start the recursion!
-  guardt guard;
+  guardt guard{true_exprt{}};
   dereference_rec(expr, state, guard, write);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)

src/goto-symex/symex_function_call.cpp

@@ -139,7 +139,7 @@ void goto_symext::parameter_assignments(
       clean_expr(lhs, state, true);
       clean_expr(rhs, state, false);
 
-      guardt guard;
+      guardt guard{true_exprt{}};
       symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
     }
 

src/goto-symex/symex_goto.cpp

@@ -249,7 +249,7 @@ void goto_symext::symex_goto(statet &state)
       state.rename(new_lhs, ns, goto_symex_statet::L1);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
-      guardt guard;
+      guardt guard{true_exprt{}};
 
       log.conditional_output(
         log.debug(),

src/goto-symex/symex_other.cpp

@@ -275,7 +275,7 @@ void goto_symext::symex_other(
     dereference_exprt object(code.op0(), empty_typet());
     clean_expr(object, state, true);
 
-    havoc_rec(state, guardt(), object);
+    havoc_rec(state, guardt(true_exprt()), object);
   }
   else
     UNREACHABLE;

src/goto-symex/symex_start_thread.cpp

@@ -81,7 +81,7 @@ void goto_symext::symex_start_thread(statet &state)
     // make copy
     ssa_exprt rhs=c_it->second.first;
 
-    guardt guard;
+    guardt guard{true_exprt{}};
     const bool record_events=state.record_events;
     state.record_events=false;
     symex_assign_symbol(
@@ -120,7 +120,7 @@ void goto_symext::symex_start_thread(statet &state)
       rhs = *zero;
     }
 
-    guardt guard;
+    guardt guard{true_exprt{}};
     symex_assign_symbol(
       state,
       lhs,

src/pointer-analysis/goto_program_dereference.cpp

@@ -251,7 +251,7 @@ void goto_program_dereferencet::dereference_expr(
   const bool checks_only,
   const value_set_dereferencet::modet mode)
 {
-  guardt guard;
+  guardt guard{true_exprt{}};
 
   if(checks_only)
   {

src/util/guard.h

@@ -19,10 +19,6 @@ Author: Daniel Kroening, [email protected]
 class guardt
 {
 public:
-  guardt() : expr(true_exprt())
-  {
-  }
-
   explicit guardt(const exprt &e) : expr(e)
   {
   }