Fix pointer validity instrumentation for incomplete array types

regression/cbmc/pointer-check-incomplete-array/main.c

@@ -0,0 +1,31 @@
+// This test checks that dereferencing a pointer to an incomplete array type
+// does not trigger an invariant violation.
+// Related to issues #5293 and #4930
+
+int (*a)[];
+
+void b()
+{
+  *a; // This should not cause an invariant violation
+}
+
+void c()
+{
+  int(*p)[];
+  *p; // Another case with a local variable
+}
+
+void test_pointer_arithmetic()
+{
+  int(*p)[] = a;
+  int(*q)[] = p + 1; // Pointer arithmetic on incomplete array type
+  int(*r)[] = q - 1; // Subtraction
+}
+
+int main()
+{
+  b();
+  c();
+  test_pointer_arithmetic();
+  return 0;
+}

regression/cbmc/pointer-check-incomplete-array/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+Test that dereferencing pointers to incomplete array types does not cause
+invariant violations.

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -1407,24 +1407,31 @@ void goto_check_ct::pointer_overflow_check(
   if(object_type.id() != ID_empty)
   {
     auto size_of_expr_opt = size_of_expr(object_type, ns);
-    CHECK_RETURN(size_of_expr_opt.has_value());
-    exprt object_size = size_of_expr_opt.value();
-
-    const binary_exprt &binary_expr = to_binary_expr(expr);
-    exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer
-                             ? binary_expr.rhs()
-                             : binary_expr.lhs();
-    mult_exprt mul{
-      offset_operand,
-      typecast_exprt::conditional_cast(object_size, offset_operand.type())};
-    mul.add_source_location() = offset_operand.source_location();
-
-    flag_overridet override_overflow(offset_operand.source_location());
-    override_overflow.set_flag(
-      enable_signed_overflow_check, true, "signed_overflow_check");
-    override_overflow.set_flag(
-      enable_unsigned_overflow_check, true, "unsigned_overflow_check");
-    integer_overflow_check(mul, guard);
+
+    // For incomplete types (e.g., incomplete arrays), we cannot perform
+    // overflow checking since the size is unknown. We skip the overflow check
+    // for such types.
+    if(size_of_expr_opt.has_value())
+    {
+      exprt object_size = size_of_expr_opt.value();
+
+      const binary_exprt &binary_expr = to_binary_expr(expr);
+      exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer
+                               ? binary_expr.rhs()
+                               : binary_expr.lhs();
+      mult_exprt mul{
+        offset_operand,
+        typecast_exprt::conditional_cast(object_size, offset_operand.type())};
+      mul.add_source_location() = offset_operand.source_location();
+
+      flag_overridet override_overflow(offset_operand.source_location());
+      override_overflow.set_flag(
+        enable_signed_overflow_check, true, "signed_overflow_check");
+      override_overflow.set_flag(
+        enable_unsigned_overflow_check, true, "unsigned_overflow_check");
+      integer_overflow_check(mul, guard);
+    }
+    // else: incomplete type - cannot check overflow
   }
 
   // the result must be within object bounds or one past the end
@@ -1467,8 +1474,19 @@ void goto_check_ct::pointer_validity_check(
   else
   {
     auto size_of_expr_opt = size_of_expr(expr.type(), ns);
-    CHECK_RETURN(size_of_expr_opt.has_value());
-    size = size_of_expr_opt.value();
+
+    // For incomplete array types (e.g., when dereferencing int (*p)[]),
+    // size_of_expr returns an empty optional since the size is not known.
+    // In this case, we perform a minimal validity check similar to void pointers.
+    if(!size_of_expr_opt.has_value())
+    {
+      // Cannot determine size for incomplete types; use minimal check
+      size = from_integer(1, size_type());
+    }
+    else
+    {
+      size = size_of_expr_opt.value();
+    }
   }
 
   auto conditions = get_pointer_dereferenceable_conditions(pointer, size);

src/goto-instrument/contracts/utils.cpp

@@ -179,9 +179,20 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
   if(auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
   {
     const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
-    CHECK_RETURN(size_of_expr_opt.has_value());
 
-    validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
+    // For incomplete types (e.g., incomplete arrays), size_of_expr returns
+    // an empty optional. In such cases, we use a minimal size check.
+    if(size_of_expr_opt.has_value())
+    {
+      validity_checks.push_back(
+        r_ok_exprt{deref->pointer(), *size_of_expr_opt});
+    }
+    else
+    {
+      // Cannot determine size for incomplete types; use minimal size
+      validity_checks.push_back(
+        r_ok_exprt{deref->pointer(), from_integer(1, size_type())});
+    }
   }
 
   for(const auto &op : expr.operands())