Make guard_expr return a value

This avoids having an argument that is both input and output and makes
using this function nicer.

Author: romainbrenguier

src/analyses/guard_bdd.cpp

@@ -44,24 +44,22 @@ guard_bddt &guard_bddt::operator=(guard_bddt &&other)
   return *this;
 }
 
-void guard_bddt::guard_expr(exprt &dest) const
+exprt guard_bddt::guard_expr(exprt expr) const
 {
   if(is_true())
   {
     // do nothing
+    return expr;
   }
   else
   {
-    if(dest.is_false())
+    if(expr.is_false())
     {
-      dest = boolean_negate(as_expr());
+      return boolean_negate(as_expr());
     }
     else
     {
-      implies_exprt tmp;
-      tmp.op0() = as_expr();
-      tmp.op1().swap(dest);
-      dest.swap(tmp);
+      return implies_exprt{as_expr(), expr};
     }
   }
 }

src/analyses/guard_bdd.h

@@ -40,8 +40,9 @@ class guard_bddt
   /// This can vary according to the guard implementation.
   static constexpr bool is_always_simplified = true;
 
-  /// Assign dest to `guard => dest` unless guard or dest are trivial.
-  void guard_expr(exprt &dest) const;
+  /// Return `guard => dest` or a simplified variant thereof if either guard or
+  /// dest are trivial.
+  exprt guard_expr(exprt expr) const;
 
   bool is_true() const
   {

src/analyses/guard_expr.cpp

@@ -18,22 +18,22 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_utils.h>
 #include <util/std_expr.h>
 
-void guard_exprt::guard_expr(exprt &dest) const
+exprt guard_exprt::guard_expr(exprt expr) const
 {
   if(is_true())
   {
     // do nothing
+    return expr;
   }
   else
   {
-    if(dest.is_false())
+    if(expr.is_false())
     {
-      dest = boolean_negate(as_expr());
+      return boolean_negate(as_expr());
     }
     else
     {
-      implies_exprt tmp(as_expr(), dest);
-      dest.swap(tmp);
+      return implies_exprt{as_expr(), expr};
     }
   }
 }

src/analyses/guard_expr.h

@@ -55,7 +55,9 @@ class guard_exprt
   /// This can vary according to the guard implementation.
   static constexpr bool is_always_simplified = false;
 
-  void guard_expr(exprt &dest) const;
+  /// Return `guard => dest` or a simplified variant thereof if either guard or
+  /// dest are trivial.
+  exprt guard_expr(exprt expr) const;
 
   bool is_true() const
   {

src/goto-symex/symex_main.cpp

@@ -116,8 +116,7 @@ void goto_symext::vcc(
   if(condition.is_true())
     return;
 
-  exprt guarded_condition = condition;
-  state.guard.guard_expr(guarded_condition);
+  const exprt guarded_condition = state.guard.guard_expr(condition);
 
   state.remaining_vccs++;
   target.assertion(state.guard.as_expr(), guarded_condition, msg, state.source);
@@ -146,8 +145,7 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
 
   if(state.threads.size()==1)
   {
-    exprt tmp = rewritten_cond;
-    state.guard.guard_expr(tmp);
+    exprt tmp = state.guard.guard_expr(rewritten_cond);
     target.assumption(state.guard.as_expr(), tmp, state.source);
   }
   // symex_target_equationt::convert_assertions would fail to