Indicate if more checks are required for a member expression

via a Boolean return value. For now these more checks are recursive call of
check_rec on operands, but other checks may occur in the future.

Author: petr-bauch

src/analyses/goto_check.cpp

@@ -124,7 +124,9 @@ class goto_checkt
   /// - check all operands of the expression
   /// \param member: the expression to be checked
   /// \param guard: the condition for the check (unmodified here)
-  void check_rec_member(const member_exprt &member, guardt &guard);
+  /// \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);
 
   /// Check that a division is valid: check for division by zero, overflow and
   ///   NaN (for floating point numbers).
@@ -1574,7 +1576,7 @@ void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
   }
 }
 
-void goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
+bool goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
 {
   const dereference_exprt &deref = to_dereference_expr(member.struct_op());
 
@@ -1583,7 +1585,7 @@ void goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
   // avoid building the following expressions when pointer_validity_check
   // would return immediately anyway
   if(!enable_pointer_check)
-    return;
+    return true;
 
   // we rewrite s->member into *(s+member_offset)
   // to avoid requiring memory safety of the entire struct
@@ -1609,11 +1611,9 @@ void goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
     new_deref.add_source_location() = deref.source_location();
     pointer_validity_check(new_deref, guard);
 
-    return;
+    return true;
   }
-
-  for(const auto &operand : member.operands())
-    check_rec(operand, guard);
+  return false;
 }
 
 void goto_checkt::check_rec_div(const div_exprt &div_expr, guardt &guard)
@@ -1671,8 +1671,8 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
     expr.id() == ID_member &&
     to_member_expr(expr).struct_op().id() == ID_dereference)
   {
-    check_rec_member(to_member_expr(expr), guard);
-    return;
+    if(check_rec_member(to_member_expr(expr), guard))
+      return;
   }
 
   forall_operands(it, expr)