Merge pull request #3820 from romainbrenguier/clean-up/guards

romainbrenguier · web-flow · commit 970cbc16eb06 · 2019-01-20T14:30:35.000Z
Remove guardt inheritance on exprt [TG-5977]
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -1407,16 +1407,15 @@ void goto_checkt::add_guarded_claim(
     return;
 
   // add the guard
-  exprt guard_expr=guard.as_expr();
 
   exprt new_expr;
 
-  if(guard_expr.is_true())
+  if(guard.is_true())
     new_expr.swap(expr);
   else
   {
     new_expr=exprt(ID_implies, bool_typet());
-    new_expr.move_to_operands(guard_expr, expr);
+    new_expr.add_to_operands(guard.as_expr(), std::move(expr));
   }
 
   if(assertions.insert(new_expr).second)
@@ -1491,8 +1490,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
         guard.add(op);
     }
 
-    guard.swap(old_guard);
-
+    guard = std::move(old_guard);
     return;
   }
   else if(expr.id()==ID_if)
@@ -1514,14 +1512,14 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
       guardt old_guard=guard;
       guard.add(expr.op0());
       check_rec(expr.op1(), guard, false);
-      guard.swap(old_guard);
+      guard = std::move(old_guard);
     }
 
     {
       guardt old_guard=guard;
       guard.add(not_exprt(expr.op0()));
       check_rec(expr.op2(), guard, false);
-      guard.swap(old_guard);
+      guard = std::move(old_guard);
     }
 
     return;
@@ -1634,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);
 }
 
@@ -1764,7 +1762,7 @@ void goto_checkt::goto_check(
             "pointer dereference",
             i.source_location,
             pointer,
-            guardt());
+            guardt(true_exprt()));
         }
       }
 
@@ -1802,7 +1800,7 @@ void goto_checkt::goto_check(
           "pointer dereference",
           i.source_location,
           pointer,
-          guardt());
+          guardt(true_exprt()));
       }
 
       // this has no successor
@@ -1883,7 +1881,7 @@ void goto_checkt::goto_check(
           "memory-leak",
           source_location,
           eq,
-          guardt());
+          guardt(true_exprt()));
       }
     }
 
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
@@ -685,15 +685,15 @@ void rw_guarded_range_set_value_sett::get_objects_if(
   {
     get_objects_rec(get_modet::READ, if_expr.cond());
 
-    guardt guard_bak1(guard), guard_bak2(guard);
+    guardt copy = guard;
 
     guard.add(not_exprt(if_expr.cond()));
     get_objects_rec(mode, if_expr.false_case(), range_start, size);
-    guard.swap(guard_bak1);
+    guard = copy;
 
     guard.add(if_expr.cond());
     get_objects_rec(mode, if_expr.true_case(), range_start, size);
-    guard.swap(guard_bak2);
+    guard = std::move(copy);
   }
 }
 
diff --git a/src/analyses/goto_rw.h b/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 = true_exprt();
+    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;
 
diff --git a/src/goto-instrument/rw_set.cpp b/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(
diff --git a/src/goto-instrument/rw_set.h b/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();
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -384,12 +384,12 @@ bool goto_symex_statet::l2_thread_read_encoding(
   ssa_exprt ssa_l1=expr;
   ssa_l1.remove_level_2();
   const irep_idt &l1_identifier=ssa_l1.get_identifier();
+  const exprt guard_as_expr = guard.as_expr();
 
   // 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())
@@ -413,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)
@@ -430,11 +429,11 @@ bool goto_symex_statet::l2_thread_read_encoding(
       read_guard |= a_s_read_guard;
     }
 
-    exprt cond=read_guard.as_expr();
+    guardt cond = read_guard;
     if(!no_write.op().is_false())
-      cond=or_exprt(no_write.op(), cond);
+      cond |= guardt{no_write.op()};
 
-    if_exprt tmp(cond, ssa_l1, ssa_l1);
+    if_exprt tmp(cond.as_expr(), ssa_l1, ssa_l1);
     set_l2_indices(to_ssa_expr(tmp.true_case()), ns);
 
     if(a_s_read.second.empty())
@@ -460,7 +459,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     record_events=record_events_bak;
 
     symex_target->assignment(
-      guard.as_expr(),
+      guard_as_expr,
       ssa_l1,
       ssa_l1,
       ssa_l1.get_original_expr(),
@@ -498,11 +497,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // and record that
   INVARIANT_STRUCTURED(
     symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
-  symex_target->shared_read(
-    guard.as_expr(),
-    expr,
-    atomic_section_id,
-    source);
+  symex_target->shared_read(guard_as_expr, expr, atomic_section_id, source);
 
   return true;
 }
diff --git a/src/goto-symex/goto_symex_state.h b/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;
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
@@ -85,13 +85,12 @@ void symex_slice_by_tracet::slice_by_trace(
 
   slice_SSA_steps(equation, implications); // Slice based on implications
 
-  guardt t_guard;
   symex_targett::sourcet empty_source;
   equation.SSA_steps.emplace_front(
     empty_source, goto_trace_stept::typet::ASSUME);
   symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
 
-  SSA_step.guard=t_guard.as_expr();
+  SSA_step.guard = true_exprt();
   SSA_step.ssa_lhs.make_nil();
   SSA_step.cond_expr.swap(trace_condition);
 
@@ -485,7 +484,6 @@ void symex_slice_by_tracet::assign_merges(
     ssa_exprt merge_sym(merge_symbol);
     merge_sym.set_level_2(merge_count);
     merge_count--;
-    guardt t_guard;
     symex_targett::sourcet empty_source;
 
     exprt merge_copy(*i);
@@ -494,7 +492,7 @@ void symex_slice_by_tracet::assign_merges(
       empty_source, goto_trace_stept::typet::ASSIGNMENT);
     symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
 
-    SSA_step.guard=t_guard.as_expr();
+    SSA_step.guard = true_exprt();
     SSA_step.ssa_lhs=merge_sym;
     SSA_step.ssa_rhs.swap(merge_copy);
     SSA_step.assignment_type=symex_targett::assignment_typet::HIDDEN;
diff --git a/src/goto-symex/symex_assign.cpp b/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);
   }
 }
@@ -431,15 +431,15 @@ void goto_symext::symex_assign_if(
     guard.add(renamed_guard);
     symex_assign_rec(
       state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);
-    guard.swap(old_guard);
+    guard = std::move(old_guard);
   }
 
   if(!renamed_guard.is_true())
   {
     guard.add(not_exprt(renamed_guard));
     symex_assign_rec(
       state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
-    guard.swap(old_guard);
+    guard = std::move(old_guard);
   }
 }
 
diff --git a/src/goto-symex/symex_dereference.cpp b/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)
diff --git a/src/goto-symex/symex_function_call.cpp b/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);
     }
 
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
@@ -225,7 +225,7 @@ void goto_symext::symex_goto(statet &state)
   // adjust guards
   if(new_guard.is_true())
   {
-    state.guard = false_exprt();
+    state.guard = guardt(false_exprt());
   }
   else
   {
@@ -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(),
diff --git a/src/goto-symex/symex_other.cpp b/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;
diff --git a/src/goto-symex/symex_start_thread.cpp b/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,
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
@@ -132,8 +132,7 @@ void goto_program_dereferencet::dereference_rec(
         guard.add(op);
     }
 
-    guard.swap(old_guard);
-
+    guard = std::move(old_guard);
     return;
   }
   else if(expr.id()==ID_if)
@@ -159,15 +158,15 @@ void goto_program_dereferencet::dereference_rec(
       guardt old_guard=guard;
       guard.add(expr.op0());
       dereference_rec(expr.op1(), guard, mode);
-      guard.swap(old_guard);
+      guard = std::move(old_guard);
     }
 
     if(o2)
     {
       guardt old_guard=guard;
       guard.add(boolean_negate(expr.op0()));
       dereference_rec(expr.op2(), guard, mode);
-      guard.swap(old_guard);
+      guard = std::move(old_guard);
     }
 
     return;
@@ -252,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)
   {
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
diff --git a/src/util/guard.h b/src/util/guard.h

Original file line number	Diff line number	Diff line change
`@@ -1407,16 +1407,15 @@ void goto_checkt::add_guarded_claim(`
`1407`	`1407`	`return;`
`1408`	`1408`
`1409`	`1409`	`// add the guard`
`1410`		`- exprt guard_expr=guard.as_expr();`
`1411`	`1410`
`1412`	`1411`	`exprt new_expr;`
`1413`	`1412`
`1414`		`- if(guard_expr.is_true())`
	`1413`	`+ if(guard.is_true())`
`1415`	`1414`	`new_expr.swap(expr);`
`1416`	`1415`	`else`
`1417`	`1416`	`{`
`1418`	`1417`	`new_expr=exprt(ID_implies, bool_typet());`
`1419`		`- new_expr.move_to_operands(guard_expr, expr);`
	`1418`	`+ new_expr.add_to_operands(guard.as_expr(), std::move(expr));`
`1420`	`1419`	`}`
`1421`	`1420`
`1422`	`1421`	`if(assertions.insert(new_expr).second)`
`@@ -1491,8 +1490,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)`
`1491`	`1490`	`guard.add(op);`
`1492`	`1491`	`}`
`1493`	`1492`
`1494`		`- guard.swap(old_guard);`
`1495`		`-`
	`1493`	`+ guard = std::move(old_guard);`
`1496`	`1494`	`return;`
`1497`	`1495`	`}`
`1498`	`1496`	`else if(expr.id()==ID_if)`
`@@ -1514,14 +1512,14 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)`
`1514`	`1512`	`guardt old_guard=guard;`
`1515`	`1513`	`guard.add(expr.op0());`
`1516`	`1514`	`check_rec(expr.op1(), guard, false);`
`1517`		`- guard.swap(old_guard);`
	`1515`	`+ guard = std::move(old_guard);`
`1518`	`1516`	`}`
`1519`	`1517`
`1520`	`1518`	`{`
`1521`	`1519`	`guardt old_guard=guard;`
`1522`	`1520`	`guard.add(not_exprt(expr.op0()));`
`1523`	`1521`	`check_rec(expr.op2(), guard, false);`
`1524`		`- guard.swap(old_guard);`
	`1522`	`+ guard = std::move(old_guard);`
`1525`	`1523`	`}`
`1526`	`1524`
`1527`	`1525`	`return;`
`@@ -1634,7 +1632,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)`
`1634`	`1632`
`1635`	`1633`	`void goto_checkt::check(const exprt &expr)`
`1636`	`1634`	`{`
`1637`		`- guardt guard;`
	`1635`	`+ guardt guard{true_exprt{}};`
`1638`	`1636`	`check_rec(expr, guard, false);`
`1639`	`1637`	`}`
`1640`	`1638`
`@@ -1764,7 +1762,7 @@ void goto_checkt::goto_check(`
`1764`	`1762`	`"pointer dereference",`
`1765`	`1763`	`i.source_location,`
`1766`	`1764`	`pointer,`
`1767`		`- guardt());`
	`1765`	`+ guardt(true_exprt()));`
`1768`	`1766`	`}`
`1769`	`1767`	`}`
`1770`	`1768`
`@@ -1802,7 +1800,7 @@ void goto_checkt::goto_check(`
`1802`	`1800`	`"pointer dereference",`
`1803`	`1801`	`i.source_location,`
`1804`	`1802`	`pointer,`
`1805`		`- guardt());`
	`1803`	`+ guardt(true_exprt()));`
`1806`	`1804`	`}`
`1807`	`1805`
`1808`	`1806`	`// this has no successor`
`@@ -1883,7 +1881,7 @@ void goto_checkt::goto_check(`
`1883`	`1881`	`"memory-leak",`
`1884`	`1882`	`source_location,`
`1885`	`1883`	`eq,`
`1886`		`- guardt());`
	`1884`	`+ guardt(true_exprt()));`
`1887`	`1885`	`}`
`1888`	`1886`	`}`
`1889`	`1887`
Original file line number	Diff line number	Diff line change
`@@ -685,15 +685,15 @@ void rw_guarded_range_set_value_sett::get_objects_if(`
`685`	`685`	`{`
`686`	`686`	`get_objects_rec(get_modet::READ, if_expr.cond());`
`687`	`687`
`688`		`- guardt guard_bak1(guard), guard_bak2(guard);`
	`688`	`+ guardt copy = guard;`
`689`	`689`
`690`	`690`	`guard.add(not_exprt(if_expr.cond()));`
`691`	`691`	`get_objects_rec(mode, if_expr.false_case(), range_start, size);`
`692`		`- guard.swap(guard_bak1);`
	`692`	`+ guard = copy;`
`693`	`693`
`694`	`694`	`guard.add(if_expr.cond());`
`695`	`695`	`get_objects_rec(mode, if_expr.true_case(), range_start, size);`
`696`		`- guard.swap(guard_bak2);`
	`696`	`+ guard = std::move(copy);`
`697`	`697`	`}`
`698`	`698`	`}`
`699`	`699`
Original file line number	Diff line number	Diff line change
`@@ -370,7 +370,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett`
`370`	`370`	`get_modet mode,`
`371`	`371`	`const exprt &expr) override`
`372`	`372`	`{`
`373`		`- guard = true_exprt();`
	`373`	`+ guard = guardt(true_exprt());`
`374`	`374`
`375`	`375`	`rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);`
`376`	`376`	`}`
`@@ -384,7 +384,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett`
`384`	`384`	`}`
`385`	`385`
`386`	`386`	`protected:`
`387`		`- guardt guard;`
	`387`	`+ guardt guard = guardt(true_exprt());`
`388`	`388`
`389`	`389`	`using rw_range_sett::get_objects_rec;`
`390`	`390`
Original file line number	Diff line number	Diff line change
`@@ -79,7 +79,7 @@ void _rw_set_loct::compute()`
`79`	`79`	`void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)`
`80`	`80`	`{`
`81`	`81`	`read(rhs);`
`82`		`- read_write_rec(lhs, false, true, "", guardt());`
	`82`	`+ read_write_rec(lhs, false, true, "", guardt(true_exprt()));`
`83`	`83`	`}`
`84`	`84`
`85`	`85`	`void _rw_set_loct::read_write_rec(`
Original file line number	Diff line number	Diff line change
`@@ -149,7 +149,7 @@ class _rw_set_loct:public rw_set_baset`
`149`	`149`
`150`	`150`	`void read(const exprt &expr)`
`151`	`151`	`{`
`152`		`- read_write_rec(expr, true, false, "", guardt());`
	`152`	`+ read_write_rec(expr, true, false, "", guardt(true_exprt()));`
`153`	`153`	`}`
`154`	`154`
`155`	`155`	`void read(const exprt &expr, const guardt &guard)`
`@@ -159,7 +159,7 @@ class _rw_set_loct:public rw_set_baset`
`159`	`159`
`160`	`160`	`void write(const exprt &expr)`
`161`	`161`	`{`
`162`		`- read_write_rec(expr, false, true, "", guardt());`
	`162`	`+ read_write_rec(expr, false, true, "", guardt(true_exprt()));`
`163`	`163`	`}`
`164`	`164`
`165`	`165`	`void compute();`
Original file line number	Diff line number	Diff line change
`@@ -89,7 +89,7 @@ void goto_symext::symex_assign(`
`89`	`89`	`if(state.source.pc->source_location.get_hide())`
`90`	`90`	`assignment_type=symex_targett::assignment_typet::HIDDEN;`
`91`	`91`
`92`		`- guardt guard; // NOT the state guard!`
	`92`	`+ guardt guard{true_exprt{}}; // NOT the state guard!`
`93`	`93`	`symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);`
`94`	`94`	`}`
`95`	`95`	`}`
`@@ -431,15 +431,15 @@ void goto_symext::symex_assign_if(`
`431`	`431`	`guard.add(renamed_guard);`
`432`	`432`	`symex_assign_rec(`
`433`	`433`	`state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);`
`434`		`- guard.swap(old_guard);`
	`434`	`+ guard = std::move(old_guard);`
`435`	`435`	`}`
`436`	`436`
`437`	`437`	`if(!renamed_guard.is_true())`
`438`	`438`	`{`
`439`	`439`	`guard.add(not_exprt(renamed_guard));`
`440`	`440`	`symex_assign_rec(`
`441`	`441`	`state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);`
`442`		`- guard.swap(old_guard);`
	`442`	`+ guard = std::move(old_guard);`
`443`	`443`	`}`
`444`	`444`	`}`
`445`	`445`
Original file line number	Diff line number	Diff line change
`@@ -139,7 +139,7 @@ void goto_symext::parameter_assignments(`
`139`	`139`	`clean_expr(lhs, state, true);`
`140`	`140`	`clean_expr(rhs, state, false);`
`141`	`141`
`142`		`- guardt guard;`
	`142`	`+ guardt guard{true_exprt{}};`
`143`	`143`	`symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);`
`144`	`144`	`}`
`145`	`145`
Original file line number	Diff line number	Diff line change
`@@ -225,7 +225,7 @@ void goto_symext::symex_goto(statet &state)`
`225`	`225`	`// adjust guards`
`226`	`226`	`if(new_guard.is_true())`
`227`	`227`	`{`
`228`		`- state.guard = false_exprt();`
	`228`	`+ state.guard = guardt(false_exprt());`
`229`	`229`	`}`
`230`	`230`	`else`
`231`	`231`	`{`
`@@ -249,7 +249,7 @@ void goto_symext::symex_goto(statet &state)`
`249`	`249`	`state.rename(new_lhs, ns, goto_symex_statet::L1);`
`250`	`250`	`state.assignment(new_lhs, new_rhs, ns, true, false);`
`251`	`251`
`252`		`- guardt guard;`
	`252`	`+ guardt guard{true_exprt{}};`
`253`	`253`
`254`	`254`	`log.conditional_output(`
`255`	`255`	`log.debug(),`
Original file line number	Diff line number	Diff line change
`@@ -275,7 +275,7 @@ void goto_symext::symex_other(`
`275`	`275`	`dereference_exprt object(code.op0(), empty_typet());`
`276`	`276`	`clean_expr(object, state, true);`
`277`	`277`
`278`		`- havoc_rec(state, guardt(), object);`
	`278`	`+ havoc_rec(state, guardt(true_exprt()), object);`
`279`	`279`	`}`
`280`	`280`	`else`
`281`	`281`	`UNREACHABLE;`
Original file line number	Diff line number	Diff line change
`@@ -132,8 +132,7 @@ void goto_program_dereferencet::dereference_rec(`
`132`	`132`	`guard.add(op);`
`133`	`133`	`}`
`134`	`134`
`135`		`- guard.swap(old_guard);`
`136`		`-`
	`135`	`+ guard = std::move(old_guard);`
`137`	`136`	`return;`
`138`	`137`	`}`
`139`	`138`	`else if(expr.id()==ID_if)`
`@@ -159,15 +158,15 @@ void goto_program_dereferencet::dereference_rec(`
`159`	`158`	`guardt old_guard=guard;`
`160`	`159`	`guard.add(expr.op0());`
`161`	`160`	`dereference_rec(expr.op1(), guard, mode);`
`162`		`- guard.swap(old_guard);`
	`161`	`+ guard = std::move(old_guard);`
`163`	`162`	`}`
`164`	`163`
`165`	`164`	`if(o2)`
`166`	`165`	`{`
`167`	`166`	`guardt old_guard=guard;`
`168`	`167`	`guard.add(boolean_negate(expr.op0()));`
`169`	`168`	`dereference_rec(expr.op2(), guard, mode);`
`170`		`- guard.swap(old_guard);`
	`169`	`+ guard = std::move(old_guard);`
`171`	`170`	`}`
`172`	`171`
`173`	`172`	`return;`
`@@ -252,7 +251,7 @@ void goto_program_dereferencet::dereference_expr(`
`252`	`251`	`const bool checks_only,`
`253`	`252`	`const value_set_dereferencet::modet mode)`
`254`	`253`	`{`
`255`		`- guardt guard;`
	`254`	`+ guardt guard{true_exprt{}};`
`256`	`255`
`257`	`256`	`if(checks_only)`
`258`	`257`	`{`