Merge pull request #6434 from NlightNFotis/implication_statement_checks

Refinement of guard based on antecedent of implication statement

Author: NlightNFotis

regression/cbmc-primitives/implication_statement_checks_1/test.c

@@ -0,0 +1,10 @@
+// clang-format off
+int main(int argc, char **argv)
+{
+    int y;
+
+    __CPROVER_assert(
+        y != 0 ==> 10 / y <= 10,
+        "10 / y is expected to succeed");
+}
+// clang-format on

regression/cbmc-primitives/implication_statement_checks_1/test.desc

@@ -0,0 +1,16 @@
+CORE
+--div-by-zero-check
+test.c
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d 10 / y is expected to succeed: SUCCESS
+\[main\.division-by-zero\.1\] line \d division by zero in 10 / y: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+\[main\.division-by-zero\.1\] line \d division by zero in 10 / y: FAILURE
+--
+Without the change that drives the refinement of the guard for a `ID_implies`
+statement in `goto-check`, this will fail with a counterexample of `y = 0`.
+With the bug fix, the `--div-by-zero-check` will succeed because the
+antecedent of the conditional is becoming the guard for the consequent,
+guarding any checks performed there.

src/analyses/goto_check.cpp

@@ -1606,6 +1606,8 @@ void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
 
 void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
 {
+  PRECONDITION(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
   INVARIANT(
     expr.is_boolean(),
     "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
@@ -1736,7 +1738,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
     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 || expr.id() == ID_implies)
   {
     check_rec_logical_op(expr, guard);
     return;