Address review comments

Will be squashed.

Author: petr-bauch

src/analyses/goto_check.cpp

@@ -113,7 +113,7 @@ class goto_checkt
   /// \param 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 exprt &expr, guardt &guard);
+  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
@@ -123,13 +123,13 @@ class goto_checkt
   /// - check all operands of the expression
   /// \param expr: the expression to be checked
   /// \param guard: the condition for the check (unmodified here)
-  void check_rec_member(const exprt &expr, guardt &guard);
+  void 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 expr: the expression to be checked
   /// \param guard: the condition for the check (unmodified here)
-  void check_rec_div(const exprt &expr, guardt &guard);
+  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.
@@ -1486,7 +1486,7 @@ void goto_checkt::add_guarded_claim(
   // add the guard
   exprt guarded_expr =
     guard.is_true()
-      ? simplified_expr
+      ? std::move(simplified_expr)
       : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
 
   if(assertions.insert(guarded_expr).second)
@@ -1544,16 +1544,14 @@ 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);
 }
 
-void goto_checkt::check_rec_if(const exprt &expr, guardt &guard)
+void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
 {
-  const if_exprt &if_expr = to_if_expr(expr);
-
   INVARIANT(
     if_expr.cond().is_boolean(),
     "first argument of if must be boolean, but got " + if_expr.cond().pretty());
@@ -1575,9 +1573,8 @@ void goto_checkt::check_rec_if(const exprt &expr, guardt &guard)
   }
 }
 
-void goto_checkt::check_rec_member(const exprt &expr, guardt &guard)
+void goto_checkt::check_rec_member(const member_exprt &member, guardt &guard)
 {
-  const member_exprt &member = to_member_expr(expr);
   const dereference_exprt &deref = to_dereference_expr(member.struct_op());
 
   check_rec(deref.pointer(), guard);
@@ -1594,7 +1591,7 @@ void goto_checkt::check_rec_member(const exprt &expr, guardt &guard)
   if(member_offset_opt.has_value())
   {
     pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
-    new_pointer_type.subtype() = expr.type();
+    new_pointer_type.subtype() = member.type();
 
     const exprt char_pointer = typecast_exprt::conditional_cast(
       deref.pointer(), pointer_type(char_type()));
@@ -1613,21 +1610,18 @@ void goto_checkt::check_rec_member(const exprt &expr, guardt &guard)
 
     return;
   }
-
-  for(const auto &operand : expr.operands())
-    check_rec(operand, guard);
 }
 
-void goto_checkt::check_rec_div(const exprt &expr, guardt &guard)
+void goto_checkt::check_rec_div(const div_exprt &div_expr, guardt &guard)
 {
-  div_by_zero_check(to_div_expr(expr), guard);
+  div_by_zero_check(to_div_expr(div_expr), guard);
 
-  if(expr.type().id() == ID_signedbv)
-    integer_overflow_check(expr, guard);
-  else if(expr.type().id() == ID_floatbv)
+  if(div_expr.type().id() == ID_signedbv)
+    integer_overflow_check(div_expr, guard);
+  else if(div_expr.type().id() == ID_floatbv)
   {
-    nan_check(expr, guard);
-    float_overflow_check(expr, guard);
+    nan_check(div_expr, guard);
+    float_overflow_check(div_expr, guard);
   }
 }
 
@@ -1666,15 +1660,14 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   }
   else if(expr.id() == ID_if)
   {
-    check_rec_if(expr, 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)
   {
-    check_rec_member(expr, guard);
-    return;
+    check_rec_member(to_member_expr(expr), guard);
   }
 
   forall_operands(it, expr)
@@ -1686,7 +1679,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   }
   else if(expr.id()==ID_div)
   {
-    check_rec_div(expr, guard);
+    check_rec_div(to_div_expr(expr), guard);
   }
   else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
   {
@@ -1808,15 +1801,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);