Address review comments

Will be squashed.

Author: petr-bauch

src/analyses/goto_check.cpp

@@ -111,26 +111,26 @@ class goto_checkt
   /// 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 expr: the expression to be checked
+  /// \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 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
   ///   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 expr: the expression to be checked
+  /// \param member: 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 div_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.
@@ -1487,7 +1487,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)
@@ -1545,16 +1545,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());
@@ -1576,9 +1574,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);
@@ -1595,7 +1592,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()));
@@ -1615,20 +1612,20 @@ void goto_checkt::check_rec_member(const exprt &expr, guardt &guard)
     return;
   }
 
-  for(const auto &operand : expr.operands())
+  for(const auto &operand : member.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);
   }
 }
 
@@ -1667,14 +1664,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);
+    check_rec_member(to_member_expr(expr), guard);
     return;
   }
 
@@ -1687,7 +1684,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)
   {
@@ -1867,15 +1864,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);