From 60e119de67c4625de2c165b3c57bb6983cc6b28c Mon Sep 17 00:00:00 2001
From: Petr Bauch <petr.bauch@gmail.com>
Date: Fri, 3 May 2019 10:11:01 +0100
Subject: [PATCH 01/13] Separate checking address-of expressions

from check_rec into stand-alone function. Getting rid of the flag.
---
 src/analyses/goto_check.cpp | 66 +++++++++++++++++++------------------
 1 file changed, 34 insertions(+), 32 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index b54831c7962..3c30cc95dfd 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -87,10 +87,9 @@ class goto_checkt
   goto_programt::const_targett current_target;
   guard_managert guard_manager;
 
-  void check_rec(
-    const exprt &expr,
-    guardt &guard,
-    bool address);
+  void check_rec_address(const exprt &expr, guardt &guard);
+
+  void check_rec(const exprt &expr, guardt &guard);
   void check(const exprt &expr);
 
   struct conditiont
@@ -1454,37 +1453,40 @@ void goto_checkt::add_guarded_claim(
   }
 }
 
-void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
+void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
 {
   // we don't look into quantifiers
-  if(expr.id()==ID_exists || expr.id()==ID_forall)
+  if(expr.id() == ID_exists || expr.id() == ID_forall)
     return;
 
-  if(address)
+  if(expr.id() == ID_dereference)
   {
-    if(expr.id()==ID_dereference)
-    {
-      assert(expr.operands().size()==1);
-      check_rec(expr.op0(), guard, false);
-    }
-    else if(expr.id()==ID_index)
-    {
-      assert(expr.operands().size()==2);
-      check_rec(expr.op0(), guard, true);
-      check_rec(expr.op1(), guard, false);
-    }
-    else
-    {
-      forall_operands(it, expr)
-        check_rec(*it, guard, true);
-    }
-    return;
+    assert(expr.operands().size() == 1);
+    check_rec(expr.op0(), guard);
   }
+  else if(expr.id() == ID_index)
+  {
+    assert(expr.operands().size() == 2);
+    check_rec_address(expr.op0(), guard);
+    check_rec(expr.op1(), guard);
+  }
+  else
+  {
+    forall_operands(it, expr)
+      check_rec_address(*it, guard);
+  }
+}
+
+void goto_checkt::check_rec(const exprt &expr, guardt &guard)
+{
+  // we don't look into quantifiers
+  if(expr.id() == ID_exists || expr.id() == ID_forall)
+    return;
 
   if(expr.id()==ID_address_of)
   {
     assert(expr.operands().size()==1);
-    check_rec(expr.op0(), guard, true);
+    check_rec_address(expr.op0(), guard);
     return;
   }
   else if(expr.id()==ID_and || expr.id()==ID_or)
@@ -1501,7 +1503,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
         throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
               op.pretty();
 
-      check_rec(op, guard, false);
+      check_rec(op, guard);
 
       if(expr.id()==ID_or)
         guard.add(not_exprt(op));
@@ -1525,19 +1527,19 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
       throw msg;
     }
 
-    check_rec(expr.op0(), guard, false);
+    check_rec(expr.op0(), guard);
 
     {
       guardt old_guard=guard;
       guard.add(expr.op0());
-      check_rec(expr.op1(), guard, false);
+      check_rec(expr.op1(), guard);
       guard = std::move(old_guard);
     }
 
     {
       guardt old_guard=guard;
       guard.add(not_exprt(expr.op0()));
-      check_rec(expr.op2(), guard, false);
+      check_rec(expr.op2(), guard);
       guard = std::move(old_guard);
     }
 
@@ -1550,7 +1552,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
     const dereference_exprt &deref=
       to_dereference_expr(member.struct_op());
 
-    check_rec(deref.pointer(), guard, false);
+    check_rec(deref.pointer(), guard);
 
     // avoid building the following expressions when pointer_validity_check
     // would return immediately anyway
@@ -1589,7 +1591,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
   }
 
   forall_operands(it, expr)
-    check_rec(*it, guard, false);
+    check_rec(*it, guard);
 
   if(expr.id()==ID_index)
   {
@@ -1652,7 +1654,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 void goto_checkt::check(const exprt &expr)
 {
   guardt guard{true_exprt{}, guard_manager};
-  check_rec(expr, guard, false);
+  check_rec(expr, guard);
 }
 
 /// expand the r_ok and w_ok predicates

From a3f70a7217eb97bc4371b1320fd079c57933ee99 Mon Sep 17 00:00:00 2001
From: Petr Bauch <petr.bauch@gmail.com>
Date: Fri, 3 May 2019 10:12:22 +0100
Subject: [PATCH 02/13] Clean-up and document check_rec_address

Using the checks inside to_expr methods.
---
 src/analyses/goto_check.cpp | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 3c30cc95dfd..daeae54f8da 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -87,6 +87,11 @@ class goto_checkt
   goto_programt::const_targett current_target;
   guard_managert guard_manager;
 
+  /// Check an address-of expression:
+  ///  if it is a dereference then check the pointer
+  ///  if it is an index then address-check the array and then check the index
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
   void check_rec_address(const exprt &expr, guardt &guard);
 
   void check_rec(const exprt &expr, guardt &guard);
@@ -1461,19 +1466,18 @@ void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
 
   if(expr.id() == ID_dereference)
   {
-    assert(expr.operands().size() == 1);
-    check_rec(expr.op0(), guard);
+    check_rec(to_dereference_expr(expr).pointer(), guard);
   }
   else if(expr.id() == ID_index)
   {
-    assert(expr.operands().size() == 2);
-    check_rec_address(expr.op0(), guard);
-    check_rec(expr.op1(), guard);
+    const index_exprt &index_expr = to_index_expr(expr);
+    check_rec_address(index_expr.array(), guard);
+    check_rec(index_expr.index(), guard);
   }
   else
   {
-    forall_operands(it, expr)
-      check_rec_address(*it, guard);
+    for(const auto &operand : expr.operands())
+      check_rec_address(operand, guard);
   }
 }
 

From 41f7f4607a29f0cf115a2221dcd7231b52c65650 Mon Sep 17 00:00:00 2001
From: Petr Bauch <petr.bauch@gmail.com>
Date: Fri, 3 May 2019 10:15:21 +0100
Subject: [PATCH 03/13] Separate checking logical operators

into a stand-alone function.
---
 src/analyses/goto_check.cpp | 49 +++++++++++++++++++++----------------
 1 file changed, 28 insertions(+), 21 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index daeae54f8da..c610fd7a908 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -94,6 +94,8 @@ class goto_checkt
   /// \param guard: the condition for the check (unmodified here)
   void check_rec_address(const exprt &expr, guardt &guard);
 
+  void check_rec_logical_op(const exprt &expr, guardt &guard);
+
   void check_rec(const exprt &expr, guardt &guard);
   void check(const exprt &expr);
 
@@ -1481,6 +1483,31 @@ void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
   }
 }
 
+void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
+{
+  if(!expr.is_boolean())
+    throw "`"+expr.id_string()+"' must be Boolean, but got "+
+      expr.pretty();
+
+  guardt old_guard=guard;
+
+  for(const auto &op : expr.operands())
+  {
+    if(!op.is_boolean())
+      throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
+        op.pretty();
+
+    check_rec(op, guard);
+
+    if(expr.id()==ID_or)
+      guard.add(not_exprt(op));
+    else
+      guard.add(op);
+  }
+
+  guard = std::move(old_guard);
+}
+
 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
 {
   // we don't look into quantifiers
@@ -1495,27 +1522,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   }
   else if(expr.id()==ID_and || expr.id()==ID_or)
   {
-    if(!expr.is_boolean())
-      throw "`"+expr.id_string()+"' must be Boolean, but got "+
-            expr.pretty();
-
-    guardt old_guard=guard;
-
-    for(const auto &op : expr.operands())
-    {
-      if(!op.is_boolean())
-        throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
-              op.pretty();
-
-      check_rec(op, guard);
-
-      if(expr.id()==ID_or)
-        guard.add(not_exprt(op));
-      else
-        guard.add(op);
-    }
-
-    guard = std::move(old_guard);
+    check_rec_logical_op(expr, guard);
     return;
   }
   else if(expr.id()==ID_if)

From 102b5b0d6660d9cf9e7739a8b4d062707f84abf4 Mon Sep 17 00:00:00 2001
From: Petr Bauch <petr.bauch@gmail.com>
Date: Fri, 3 May 2019 10:17:36 +0100
Subject: [PATCH 04/13] Clean-up and document check_rec_logical_op

Using invariants instead of exceptions.
---
 src/analyses/goto_check.cpp | 28 ++++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index c610fd7a908..fef05deb0c8 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -94,6 +94,13 @@ class goto_checkt
   /// \param guard: the condition for the check (unmodified here)
   void check_rec_address(const exprt &expr, guardt &guard);
 
+  /// Check a logical operation: check each operand in separation while
+  /// extending the guarding condition as follows.
+  ///  a /\ b /\ c ==> check(a, TRUE), check(b, a), check (c, a /\ b)
+  ///  a \/ b \/ c ==> check(a, TRUE), check(b, ~a), check (c, ~a /\ ~b)
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for the check (extended with the previous
+  ///   operands (or their negations) for recursively calls)
   void check_rec_logical_op(const exprt &expr, guardt &guard);
 
   void check_rec(const exprt &expr, guardt &guard);
@@ -1485,24 +1492,21 @@ void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
 
 void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
 {
-  if(!expr.is_boolean())
-    throw "`"+expr.id_string()+"' must be Boolean, but got "+
-      expr.pretty();
+  INVARIANT(
+    expr.is_boolean(),
+    "`" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
 
-  guardt old_guard=guard;
+  guardt old_guard = guard;
 
   for(const auto &op : expr.operands())
   {
-    if(!op.is_boolean())
-      throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
-        op.pretty();
+    INVARIANT(
+      op.is_boolean(),
+      "`" + expr.id_string() + "' takes Boolean operands only, but got " +
+        op.pretty());
 
     check_rec(op, guard);
-
-    if(expr.id()==ID_or)
-      guard.add(not_exprt(op));
-    else
-      guard.add(op);
+    guard.add(expr.id() == ID_or ? not_exprt(op) : op);
   }
 
   guard = std::move(old_guard);

From 1f105fe27b047de5a9106e1aabc99e6831d7d755 Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:09:17 +0100
Subject: [PATCH 05/13] Refactor, rename, and document add_guarded_claim

into add_guarded_property.
---
 src/analyses/goto_check.cpp | 107 ++++++++++++++++++------------------
 1 file changed, 55 insertions(+), 52 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index fef05deb0c8..1b4411096d8 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -136,11 +136,19 @@ class goto_checkt
 
   std::string array_name(const exprt &);
 
-  void add_guarded_claim(
-    const exprt &expr,
+  /// Include the \p asserted_expr in the code conditioned by the \p guard.
+  /// \param asserted_expr: expression to be asserted
+  /// \param comment: human readable comment
+  /// \param property_class: classification of the property
+  /// \param source_location: the source location of the original expression
+  /// \param src_expr: the original expression to be included in the comment
+  /// \param guard: the condition under which the asserted expression should be
+  ///   taken into account
+  void add_guarded_property(
+    const exprt &asserted_expr,
     const std::string &comment,
     const std::string &property_class,
-    const source_locationt &,
+    const source_locationt &source_location,
     const exprt &src_expr,
     const guardt &guard);
 
@@ -257,7 +265,7 @@ void goto_checkt::div_by_zero_check(
   exprt zero=from_integer(0, expr.op1().type());
   const notequal_exprt inequality(expr.op1(), std::move(zero));
 
-  add_guarded_claim(
+  add_guarded_property(
     inequality,
     "division by zero",
     "division-by-zero",
@@ -283,7 +291,7 @@ void goto_checkt::undefined_shift_check(
     binary_relation_exprt inequality(
       expr.distance(), ID_ge, from_integer(0, distance_type));
 
-    add_guarded_claim(
+    add_guarded_property(
       inequality,
       "shift distance is negative",
       "undefined-shift",
@@ -299,7 +307,7 @@ void goto_checkt::undefined_shift_check(
     exprt width_expr=
       from_integer(to_bitvector_type(op_type).get_width(), distance_type);
 
-    add_guarded_claim(
+    add_guarded_property(
       binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
       "shift distance too large",
       "undefined-shift",
@@ -312,7 +320,7 @@ void goto_checkt::undefined_shift_check(
       binary_relation_exprt inequality(
         expr.op(), ID_ge, from_integer(0, op_type));
 
-      add_guarded_claim(
+      add_guarded_property(
         inequality,
         "shift operand is negative",
         "undefined-shift",
@@ -323,7 +331,7 @@ void goto_checkt::undefined_shift_check(
   }
   else
   {
-    add_guarded_claim(
+    add_guarded_property(
       false_exprt(),
       "shift of non-integer type",
       "undefined-shift",
@@ -345,7 +353,7 @@ void goto_checkt::mod_by_zero_check(
   exprt zero=from_integer(0, expr.op1().type());
   const notequal_exprt inequality(expr.op1(), std::move(zero));
 
-  add_guarded_claim(
+  add_guarded_property(
     inequality,
     "division by zero",
     "division-by-zero",
@@ -375,7 +383,7 @@ void goto_checkt::mod_overflow_check(const mod_exprt &expr, const guardt &guard)
     notequal_exprt minus_one_neq(
       expr.op1(), from_integer(-1, expr.op1().type()));
 
-    add_guarded_claim(
+    add_guarded_property(
       or_exprt(int_min_neq, minus_one_neq),
       "result of signed mod is not representable",
       "overflow",
@@ -426,7 +434,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_lower(
           expr.op0(), ID_ge, from_integer(-power(2, new_width - 1), old_type));
 
-        add_guarded_claim(
+        add_guarded_property(
           and_exprt(no_overflow_lower, no_overflow_upper),
           "arithmetic overflow on signed type conversion",
           "overflow",
@@ -445,7 +453,7 @@ void goto_checkt::conversion_check(
           ID_le,
           from_integer(power(2, new_width - 1) - 1, old_type));
 
-        add_guarded_claim(
+        add_guarded_property(
           no_overflow_upper,
           "arithmetic overflow on unsigned to signed type conversion",
           "overflow",
@@ -466,7 +474,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_lower(
           expr.op0(), ID_gt, lower.to_expr());
 
-        add_guarded_claim(
+        add_guarded_property(
           and_exprt(no_overflow_lower, no_overflow_upper),
           "arithmetic overflow on float to signed integer type conversion",
           "overflow",
@@ -489,7 +497,7 @@ void goto_checkt::conversion_check(
           const binary_relation_exprt no_overflow_lower(
             expr.op0(), ID_ge, from_integer(0, old_type));
 
-          add_guarded_claim(
+          add_guarded_property(
             no_overflow_lower,
             "arithmetic overflow on signed to unsigned type conversion",
             "overflow",
@@ -506,7 +514,7 @@ void goto_checkt::conversion_check(
           const binary_relation_exprt no_overflow_lower(
             expr.op0(), ID_ge, from_integer(0, old_type));
 
-          add_guarded_claim(
+          add_guarded_property(
             and_exprt(no_overflow_lower, no_overflow_upper),
             "arithmetic overflow on signed to unsigned type conversion",
             "overflow",
@@ -524,7 +532,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_upper(
           expr.op0(), ID_le, from_integer(power(2, new_width) - 1, old_type));
 
-        add_guarded_claim(
+        add_guarded_property(
           no_overflow_upper,
           "arithmetic overflow on unsigned to unsigned type conversion",
           "overflow",
@@ -545,7 +553,7 @@ void goto_checkt::conversion_check(
         const binary_relation_exprt no_overflow_lower(
           expr.op0(), ID_gt, lower.to_expr());
 
-        add_guarded_claim(
+        add_guarded_property(
           and_exprt(no_overflow_lower, no_overflow_upper),
           "arithmetic overflow on float to unsigned integer type conversion",
           "overflow",
@@ -589,7 +597,7 @@ void goto_checkt::integer_overflow_check(
       equal_exprt minus_one_eq(
         expr.op1(), from_integer(-1, type));
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(and_exprt(int_min_eq, minus_one_eq)),
         "arithmetic overflow on signed division",
         "overflow",
@@ -610,7 +618,7 @@ void goto_checkt::integer_overflow_check(
       equal_exprt int_min_eq(
         expr.op0(), to_signedbv_type(type).smallest_expr());
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(int_min_eq),
         "arithmetic overflow on signed unary minus",
         "overflow",
@@ -709,7 +717,7 @@ void goto_checkt::integer_overflow_check(
       // a shift that's too far isn't an overflow;
       // a shift of zero isn't overflow;
       // else check the top bits
-      add_guarded_claim(
+      add_guarded_property(
         disjunction({neg_value_shift,
                      neg_dist_shift,
                      dist_too_large,
@@ -752,7 +760,7 @@ void goto_checkt::integer_overflow_check(
       std::string kind=
         type.id()==ID_unsignedbv?"unsigned":"signed";
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(overflow),
         "arithmetic overflow on "+kind+" "+expr.id_string(),
         "overflow",
@@ -766,7 +774,7 @@ void goto_checkt::integer_overflow_check(
     std::string kind=
       type.id()==ID_unsignedbv?"unsigned":"signed";
 
-    add_guarded_claim(
+    add_guarded_property(
       not_exprt(overflow),
       "arithmetic overflow on "+kind+" "+expr.id_string(),
       "overflow",
@@ -805,7 +813,7 @@ void goto_checkt::float_overflow_check(
 
       or_exprt overflow_check(op0_inf, not_exprt(new_inf));
 
-      add_guarded_claim(
+      add_guarded_property(
         overflow_check,
         "arithmetic overflow on floating-point typecast",
         "overflow",
@@ -818,7 +826,7 @@ void goto_checkt::float_overflow_check(
       // non-float-to-float
       const isinf_exprt new_inf(expr);
 
-      add_guarded_claim(
+      add_guarded_property(
         not_exprt(new_inf),
         "arithmetic overflow on floating-point typecast",
         "overflow",
@@ -839,7 +847,7 @@ void goto_checkt::float_overflow_check(
 
     or_exprt overflow_check(op0_inf, not_exprt(new_inf));
 
-    add_guarded_claim(
+    add_guarded_property(
       overflow_check,
       "arithmetic overflow on floating-point division",
       "overflow",
@@ -876,7 +884,7 @@ void goto_checkt::float_overflow_check(
         expr.id()==ID_minus?"subtraction":
         expr.id()==ID_mult?"multiplication":"";
 
-      add_guarded_claim(
+      add_guarded_property(
         overflow_check,
         "arithmetic overflow on floating-point "+kind,
         "overflow",
@@ -996,7 +1004,7 @@ void goto_checkt::nan_check(
   else
     UNREACHABLE;
 
-  add_guarded_claim(
+  add_guarded_property(
     boolean_negate(isnan),
     "NaN on " + expr.id_string(),
     "NaN",
@@ -1024,7 +1032,7 @@ void goto_checkt::pointer_rel_check(
     {
       exprt same_object=::same_object(expr.op0(), expr.op1());
 
-      add_guarded_claim(
+      add_guarded_property(
         same_object,
         "same object violation",
         "pointer",
@@ -1052,7 +1060,7 @@ void goto_checkt::pointer_overflow_check(
   exprt overflow("overflow-" + expr.id_string(), bool_typet());
   overflow.operands() = expr.operands();
 
-  add_guarded_claim(
+  add_guarded_property(
     not_exprt(overflow),
     "pointer arithmetic overflow on " + expr.id_string(),
     "overflow",
@@ -1077,7 +1085,7 @@ void goto_checkt::pointer_validity_check(
 
   for(const auto &c : conditions)
   {
-    add_guarded_claim(
+    add_guarded_property(
       c.assertion,
       "dereference failure: "+c.description,
       "pointer dereference",
@@ -1276,7 +1284,7 @@ void goto_checkt::bounds_check(
         binary_relation_exprt inequality(
           effective_offset, ID_ge, std::move(zero));
 
-        add_guarded_claim(
+        add_guarded_property(
           inequality,
           name+" lower bound",
           "array bounds",
@@ -1333,7 +1341,7 @@ void goto_checkt::bounds_check(
       and_exprt(dynamic_object(pointer), not_exprt(malloc_object(pointer, ns))),
       inequality);
 
-    add_guarded_claim(
+    add_guarded_property(
       precond,
       name+" dynamic object upper bound",
       "array bounds",
@@ -1394,7 +1402,7 @@ void goto_checkt::bounds_check(
       ID_lt,
       type_size_opt.value());
 
-    add_guarded_claim(
+    add_guarded_property(
       implies_exprt(type_matches_size, inequality),
       name + " upper bound",
       "array bounds",
@@ -1410,7 +1418,7 @@ void goto_checkt::bounds_check(
     inequality.op1() = typecast_exprt::conditional_cast(
       inequality.op1(), inequality.op0().type());
 
-    add_guarded_claim(
+    add_guarded_property(
       implies_exprt(type_matches_size, inequality),
       name+" upper bound",
       "array bounds",
@@ -1420,34 +1428,29 @@ void goto_checkt::bounds_check(
   }
 }
 
-void goto_checkt::add_guarded_claim(
-  const exprt &_expr,
+void goto_checkt::add_guarded_property(
+  const exprt &asserted_expr,
   const std::string &comment,
   const std::string &property_class,
   const source_locationt &source_location,
   const exprt &src_expr,
   const guardt &guard)
 {
-  exprt expr(_expr);
-
   // first try simplifier on it
-  if(enable_simplify)
-    simplify(expr, ns);
+  exprt simplified_expr =
+    enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
 
   // throw away trivial properties?
-  if(!retain_trivial && expr.is_true())
+  if(!retain_trivial && simplified_expr.is_true())
     return;
 
   // add the guard
+  exprt guarded_expr =
+    guard.is_true()
+      ? std::move(simplified_expr)
+      : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
 
-  exprt new_expr;
-
-  if(guard.is_true())
-    new_expr.swap(expr);
-  else
-    new_expr = implies_exprt(guard.as_expr(), std::move(expr));
-
-  if(assertions.insert(new_expr).second)
+  if(assertions.insert(guarded_expr).second)
   {
     goto_program_instruction_typet type=
       enable_assert_to_assume?ASSUME:ASSERT;
@@ -1890,7 +1893,7 @@ void goto_checkt::goto_check(
             pointer,
             null_pointer_exprt(to_pointer_type(pointer.type())));
 
-          add_guarded_claim(
+          add_guarded_property(
             not_eq_null,
             "this is null on method invocation",
             "pointer dereference",
@@ -1939,7 +1942,7 @@ void goto_checkt::goto_check(
         const notequal_exprt not_eq_null(
           pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
 
-        add_guarded_claim(
+        add_guarded_property(
           not_eq_null,
           "throwing null",
           "pointer dereference",
@@ -2014,7 +2017,7 @@ void goto_checkt::goto_check(
         equal_exprt eq(
           leak_expr,
           null_pointer_exprt(to_pointer_type(leak.type)));
-        add_guarded_claim(
+        add_guarded_property(
           eq,
           "dynamically allocated memory never freed",
           "memory-leak",

From d74ef718efa4a1deb4e199668607cd74fedb6379 Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:10:57 +0100
Subject: [PATCH 06/13] Separate and refactor checking if

Using invariants, to-conversion and a bit of clang-formatting.
---
 src/analyses/goto_check.cpp | 61 ++++++++++++++++++++-----------------
 1 file changed, 33 insertions(+), 28 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 1b4411096d8..a4152d9e0c8 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -103,6 +103,14 @@ class goto_checkt
   ///   operands (or their negations) for recursively calls)
   void check_rec_logical_op(const exprt &expr, guardt &guard);
 
+  /// Check an if expression: check the if-condition alone, and then check the
+  ///   true/false-cases with the guard extended with if-condition and it's
+  ///   negation, respectively.
+  /// \param if_expr: the expression to be checked
+  /// \param guard: the condition for the check (extended with the (negation of
+  ///   the) if-condition for recursively calls)
+  void check_rec_if(const if_exprt &if_expr, guardt &guard);
+
   void check_rec(const exprt &expr, guardt &guard);
   void check(const exprt &expr);
 
@@ -1515,6 +1523,29 @@ void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
   guard = std::move(old_guard);
 }
 
+void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
+{
+  INVARIANT(
+    if_expr.cond().is_boolean(),
+    "first argument of if must be boolean, but got " + if_expr.cond().pretty());
+
+  check_rec(if_expr.cond(), guard);
+
+  {
+    guardt old_guard = guard;
+    guard.add(if_expr.cond());
+    check_rec(if_expr.true_case(), guard);
+    guard = std::move(old_guard);
+  }
+
+  {
+    guardt old_guard = guard;
+    guard.add(not_exprt{if_expr.cond()});
+    check_rec(if_expr.false_case(), guard);
+    guard = std::move(old_guard);
+  }
+}
+
 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
 {
   // we don't look into quantifiers
@@ -1532,35 +1563,9 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
     check_rec_logical_op(expr, guard);
     return;
   }
-  else if(expr.id()==ID_if)
+  else if(expr.id() == ID_if)
   {
-    if(expr.operands().size()!=3)
-      throw "if takes three arguments";
-
-    if(!expr.op0().is_boolean())
-    {
-      std::string msg=
-        "first argument of if must be boolean, but got "
-        +expr.op0().pretty();
-      throw msg;
-    }
-
-    check_rec(expr.op0(), guard);
-
-    {
-      guardt old_guard=guard;
-      guard.add(expr.op0());
-      check_rec(expr.op1(), guard);
-      guard = std::move(old_guard);
-    }
-
-    {
-      guardt old_guard=guard;
-      guard.add(not_exprt(expr.op0()));
-      check_rec(expr.op2(), guard);
-      guard = std::move(old_guard);
-    }
-
+    check_rec_if(to_if_expr(expr), guard);
     return;
   }
   else if(expr.id()==ID_member &&

From 266f00b381fac9fc4e4564680574fde5244c069f Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:12:05 +0100
Subject: [PATCH 07/13] Separate and refactor checking member

Only clang-format, inline expr-construction, and for-each loop.
---
 src/analyses/goto_check.cpp | 97 +++++++++++++++++++++----------------
 1 file changed, 56 insertions(+), 41 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index a4152d9e0c8..42e582ce7e1 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -111,6 +111,18 @@ class goto_checkt
   ///   the) if-condition for recursively calls)
   void check_rec_if(const if_exprt &if_expr, guardt &guard);
 
+  /// Check that a member expression is valid:
+  /// - check the structure this expression is a member of (via pointer of its
+  ///   dereference)
+  /// - run pointer-validity check on `*(s+member_offset)' instead of
+  ///   `s->member' to avoid checking safety of `s'
+  /// - check all operands of the expression
+  /// \param member: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  /// \return true if no more checks are required for \p member or its
+  ///   sub-expressions
+  bool check_rec_member(const member_exprt &member, guardt &guard);
+
   void check_rec(const exprt &expr, guardt &guard);
   void check(const exprt &expr);
 
@@ -1546,6 +1558,46 @@ void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
   }
 }
 
+bool goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
+{
+  const dereference_exprt &deref = to_dereference_expr(member.struct_op());
+
+  check_rec(deref.pointer(), guard);
+
+  // avoid building the following expressions when pointer_validity_check
+  // would return immediately anyway
+  if(!enable_pointer_check)
+    return true;
+
+  // we rewrite s->member into *(s+member_offset)
+  // to avoid requiring memory safety of the entire struct
+  auto member_offset_opt = member_offset_expr(member, ns);
+
+  if(member_offset_opt.has_value())
+  {
+    pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
+    new_pointer_type.subtype() = member.type();
+
+    const exprt char_pointer = typecast_exprt::conditional_cast(
+      deref.pointer(), pointer_type(char_type()));
+
+    const exprt new_address_casted = typecast_exprt::conditional_cast(
+      typecast_exprt{
+        plus_exprt{char_pointer,
+                   typecast_exprt::conditional_cast(
+                     member_offset_opt.value(), pointer_diff_type())},
+        char_pointer.type()},
+      new_pointer_type);
+
+    dereference_exprt new_deref{new_address_casted};
+    new_deref.add_source_location() = deref.source_location();
+    pointer_validity_check(new_deref, guard);
+
+    return true;
+  }
+  return false;
+}
+
 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
 {
   // we don't look into quantifiers
@@ -1568,49 +1620,12 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
     check_rec_if(to_if_expr(expr), guard);
     return;
   }
-  else if(expr.id()==ID_member &&
-          to_member_expr(expr).struct_op().id()==ID_dereference)
+  else if(
+    expr.id() == ID_member &&
+    to_member_expr(expr).struct_op().id() == ID_dereference)
   {
-    const member_exprt &member=to_member_expr(expr);
-    const dereference_exprt &deref=
-      to_dereference_expr(member.struct_op());
-
-    check_rec(deref.pointer(), guard);
-
-    // avoid building the following expressions when pointer_validity_check
-    // would return immediately anyway
-    if(!enable_pointer_check)
-      return;
-
-    // we rewrite s->member into *(s+member_offset)
-    // to avoid requiring memory safety of the entire struct
-    auto member_offset_opt = member_offset_expr(member, ns);
-
-    if(member_offset_opt.has_value())
-    {
-      pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
-      new_pointer_type.subtype() = expr.type();
-
-      const exprt char_pointer =
-        typecast_exprt::conditional_cast(
-          deref.pointer(), pointer_type(char_type()));
-
-      const exprt new_address = typecast_exprt(
-        plus_exprt(
-          char_pointer,
-          typecast_exprt::conditional_cast(
-            member_offset_opt.value(), pointer_diff_type())),
-        char_pointer.type());
-
-      const exprt new_address_casted =
-        typecast_exprt::conditional_cast(new_address, new_pointer_type);
-
-      dereference_exprt new_deref{new_address_casted};
-      new_deref.add_source_location() = deref.source_location();
-      pointer_validity_check(new_deref, guard);
-
+    if(check_rec_member(to_member_expr(expr), guard))
       return;
-    }
   }
 
   forall_operands(it, expr)

From 2662f2b12e639c8667aec4341eecf0595b25e416 Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:13:17 +0100
Subject: [PATCH 08/13] Separate and document checking arithmetic ops

Into check_rec_div and check_rec_arithmetic_op.
---
 src/analyses/goto_check.cpp | 67 ++++++++++++++++++++++++-------------
 1 file changed, 44 insertions(+), 23 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 42e582ce7e1..fae4b1e4f88 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -123,6 +123,18 @@ class goto_checkt
   ///   sub-expressions
   bool check_rec_member(const member_exprt &member, guardt &guard);
 
+  /// Check that a division is valid: check for division by zero, overflow and
+  ///   NaN (for floating point numbers).
+  /// \param div_expr: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  void check_rec_div(const div_exprt &div_expr, guardt &guard);
+
+  /// Check that an arithmetic operation is valid: overflow check, NaN-check
+  ///   (for floating point numbers), and pointer overflow check.
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  void check_rec_arithmetic_op(const exprt &expr, guardt &guard);
+
   void check_rec(const exprt &expr, guardt &guard);
   void check(const exprt &expr);
 
@@ -1598,6 +1610,36 @@ bool goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
   return false;
 }
 
+void goto_checkt::check_rec_div(const div_exprt &div_expr, guardt &guard)
+{
+  div_by_zero_check(to_div_expr(div_expr), guard);
+
+  if(div_expr.type().id() == ID_signedbv)
+    integer_overflow_check(div_expr, guard);
+  else if(div_expr.type().id() == ID_floatbv)
+  {
+    nan_check(div_expr, guard);
+    float_overflow_check(div_expr, guard);
+  }
+}
+
+void goto_checkt::check_rec_arithmetic_op(const exprt &expr, guardt &guard)
+{
+  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
+  {
+    integer_overflow_check(expr, guard);
+  }
+  else if(expr.type().id() == ID_floatbv)
+  {
+    nan_check(expr, guard);
+    float_overflow_check(expr, guard);
+  }
+  else if(expr.type().id() == ID_pointer)
+  {
+    pointer_overflow_check(expr, guard);
+  }
+}
+
 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
 {
   // we don't look into quantifiers
@@ -1637,15 +1679,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   }
   else if(expr.id()==ID_div)
   {
-    div_by_zero_check(to_div_expr(expr), guard);
-
-    if(expr.type().id()==ID_signedbv)
-      integer_overflow_check(expr, guard);
-    else if(expr.type().id()==ID_floatbv)
-    {
-      nan_check(expr, guard);
-      float_overflow_check(expr, guard);
-    }
+    check_rec_div(to_div_expr(expr), guard);
   }
   else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
   {
@@ -1663,20 +1697,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
           expr.id()==ID_mult ||
           expr.id()==ID_unary_minus)
   {
-    if(expr.type().id()==ID_signedbv ||
-       expr.type().id()==ID_unsignedbv)
-    {
-      integer_overflow_check(expr, guard);
-    }
-    else if(expr.type().id()==ID_floatbv)
-    {
-      nan_check(expr, guard);
-      float_overflow_check(expr, guard);
-    }
-    else if(expr.type().id()==ID_pointer)
-    {
-      pointer_overflow_check(expr, guard);
-    }
+    check_rec_arithmetic_op(expr, guard);
   }
   else if(expr.id()==ID_typecast)
     conversion_check(expr, guard);

From f931965d8d74335e824e1cb39d157ef4b6d50bb2 Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:14:12 +0100
Subject: [PATCH 09/13] Document and refactor invalidate

Using the initializer-list constructor for sets and and standard idiom for
erase_if.
---
 src/analyses/goto_check.cpp | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index fae4b1e4f88..a168ea8f4ec 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -188,6 +188,10 @@ class goto_checkt
   typedef std::set<exprt> assertionst;
   assertionst assertions;
 
+  /// Remove all assertions containing the symbol in \p lhs as well as all
+  ///   assertions containing dereference.
+  /// \param lhs: the left-hand-side expression whose symbol should be
+  ///   invalidated
   void invalidate(const exprt &lhs);
 
   bool enable_bounds_check;
@@ -261,21 +265,14 @@ void goto_checkt::invalidate(const exprt &lhs)
   else if(lhs.id()==ID_symbol)
   {
     // clear all assertions about 'symbol'
-    find_symbols_sett find_symbols_set;
-    find_symbols_set.insert(to_symbol_expr(lhs).get_identifier());
+    find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
 
-    for(assertionst::iterator
-        it=assertions.begin();
-        it!=assertions.end();
-        ) // no it++
+    for(auto it = assertions.begin(); it != assertions.end();)
     {
-      assertionst::iterator next=it;
-      next++;
-
       if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference))
-        assertions.erase(it);
-
-      it=next;
+        it = assertions.erase(it);
+      else
+        ++it;
     }
   }
   else

From c7c94b2cf800413150a289c61cf5084725fe08eb Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:15:18 +0100
Subject: [PATCH 10/13] Use make_assumption/assertion wrappers

instead of instructiont constructor.
---
 src/analyses/goto_check.cpp | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index a168ea8f4ec..687656c32fb 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1481,15 +1481,11 @@ void goto_checkt::add_guarded_property(
 
   if(assertions.insert(guarded_expr).second)
   {
-    goto_program_instruction_typet type=
-      enable_assert_to_assume?ASSUME:ASSERT;
-
-    goto_programt::targett t = new_code.add(goto_programt::instructiont(
-      static_cast<const codet &>(get_nil_irep()),
-      source_location,
-      type,
-      std::move(new_expr),
-      {}));
+    auto t = new_code.add(
+      enable_assert_to_assume ? goto_programt::make_assumption(
+                                  std::move(guarded_expr), source_location)
+                              : goto_programt::make_assertion(
+                                  std::move(guarded_expr), source_location));
 
     std::string source_expr_string;
     get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
@@ -1856,15 +1852,10 @@ void goto_checkt::goto_check(
     {
       if(std::find(i.labels.begin(), i.labels.end(), label)!=i.labels.end())
       {
-        goto_program_instruction_typet type=
-          enable_assert_to_assume?ASSUME:ASSERT;
-
-        goto_programt::targett t = new_code.add(goto_programt::instructiont(
-          static_cast<const codet &>(get_nil_irep()),
-          i.source_location,
-          type,
-          false_exprt(),
-          {}));
+        auto t = new_code.add(
+          enable_assert_to_assume
+            ? goto_programt::make_assumption(false_exprt{}, i.source_location)
+            : goto_programt::make_assertion(false_exprt{}, i.source_location));
 
         t->source_location.set_property_class("error label");
         t->source_location.set_comment("error label "+label);

From cecc28981fda455faa4130015c566ff8f545b7fc Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:16:24 +0100
Subject: [PATCH 11/13] Use built-in methods

to negate boolean expression and to get address_of expression.
---
 src/analyses/goto_check.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 687656c32fb..400db122642 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1534,7 +1534,7 @@ void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
         op.pretty());
 
     check_rec(op, guard);
-    guard.add(expr.id() == ID_or ? not_exprt(op) : op);
+    guard.add(expr.id() == ID_or ? boolean_negate(op) : op);
   }
 
   guard = std::move(old_guard);
@@ -1641,8 +1641,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
 
   if(expr.id()==ID_address_of)
   {
-    assert(expr.operands().size()==1);
-    check_rec_address(expr.op0(), guard);
+    check_rec_address(to_address_of_expr(expr).object(), guard);
     return;
   }
   else if(expr.id()==ID_and || expr.id()==ID_or)

From e0eab84e3d7dff87406e084fe82fd39368409514 Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:18:19 +0100
Subject: [PATCH 12/13] Add documentation

to collect_allocations, check_rec, and check.
---
 src/analyses/goto_check.cpp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 400db122642..98d5688deae 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -79,6 +79,11 @@ class goto_checkt
     const irep_idt &function_identifier,
     goto_functiont &goto_function);
 
+  /// Fill the list of allocations \ref allocationst with <address, size> for
+  ///   every allocation instruction. Also check that each allocation is
+  ///   well-formed.
+  /// \param goto_functions: goto functions from which the allocations are to be
+  ///   collected
   void collect_allocations(const goto_functionst &goto_functions);
 
 protected:
@@ -135,7 +140,15 @@ class goto_checkt
   /// \param guard: the condition for the check (unmodified here)
   void check_rec_arithmetic_op(const exprt &expr, guardt &guard);
 
+  /// Recursively descend into \p expr and run the appropriate check for each
+  ///   sub-expression, while collecting the condition for the check in \p
+  ///   guard.
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for when the check should be made
   void check_rec(const exprt &expr, guardt &guard);
+
+  /// Initiate the recursively analysis of \p expr with its `guard' set to TRUE.
+  /// \param expr: the expression to be checked
   void check(const exprt &expr);
 
   struct conditiont

From b5060ee0fca3fba80d6c977bbf052e2c3a2ada66 Mon Sep 17 00:00:00 2001
From: xbauch <petr.bauch@gmail.com>
Date: Sun, 19 May 2019 08:20:43 +0100
Subject: [PATCH 13/13] Clang-formatting

for the bits we touched in this PR.
---
 src/analyses/goto_check.cpp | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 98d5688deae..99a28ebfaad 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -804,7 +804,7 @@ void goto_checkt::integer_overflow_check(
 
       add_guarded_property(
         not_exprt(overflow),
-        "arithmetic overflow on "+kind+" "+expr.id_string(),
+        "arithmetic overflow on " + kind + " " + expr.id_string(),
         "overflow",
         expr.find_source_location(),
         expr,
@@ -818,7 +818,7 @@ void goto_checkt::integer_overflow_check(
 
     add_guarded_property(
       not_exprt(overflow),
-      "arithmetic overflow on "+kind+" "+expr.id_string(),
+      "arithmetic overflow on " + kind + " " + expr.id_string(),
       "overflow",
       expr.find_source_location(),
       expr,
@@ -928,7 +928,7 @@ void goto_checkt::float_overflow_check(
 
       add_guarded_property(
         overflow_check,
-        "arithmetic overflow on floating-point "+kind,
+        "arithmetic overflow on floating-point " + kind,
         "overflow",
         expr.find_source_location(),
         expr,
@@ -1129,7 +1129,7 @@ void goto_checkt::pointer_validity_check(
   {
     add_guarded_property(
       c.assertion,
-      "dereference failure: "+c.description,
+      "dereference failure: " + c.description,
       "pointer dereference",
       expr.find_source_location(),
       expr,
@@ -1328,7 +1328,7 @@ void goto_checkt::bounds_check(
 
         add_guarded_property(
           inequality,
-          name+" lower bound",
+          name + " lower bound",
           "array bounds",
           expr.find_source_location(),
           expr,
@@ -1385,7 +1385,7 @@ void goto_checkt::bounds_check(
 
     add_guarded_property(
       precond,
-      name+" dynamic object upper bound",
+      name + " dynamic object upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,
@@ -1462,7 +1462,7 @@ void goto_checkt::bounds_check(
 
     add_guarded_property(
       implies_exprt(type_matches_size, inequality),
-      name+" upper bound",
+      name + " upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,
@@ -1503,7 +1503,7 @@ void goto_checkt::add_guarded_property(
     std::string source_expr_string;
     get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
-    t->source_location.set_comment(comment+" in "+source_expr_string);
+    t->source_location.set_comment(comment + " in " + source_expr_string);
     t->source_location.set_property_class(property_class);
   }
 }
@@ -1652,12 +1652,12 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   if(expr.id() == ID_exists || expr.id() == ID_forall)
     return;
 
-  if(expr.id()==ID_address_of)
+  if(expr.id() == ID_address_of)
   {
     check_rec_address(to_address_of_expr(expr).object(), guard);
     return;
   }
-  else if(expr.id()==ID_and || expr.id()==ID_or)
+  else if(expr.id() == ID_and || expr.id() == ID_or)
   {
     check_rec_logical_op(expr, guard);
     return;