Sizeof should fail on incomplete types

regression/cbmc/incomplete-sizeof/array.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int arr[];
+
+int main(int argc, char **argv)
+{
+  size_t s = sizeof(arr);
+  assert(s == 4);
+}

regression/cbmc/incomplete-sizeof/array.desc

@@ -0,0 +1,9 @@
+CORE
+array.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file array.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
+^CONVERSION ERROR$
+--
+^warning: ignoring

regression/cbmc/incomplete-sizeof/enum.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+enum foo;
+
+int main(int argc, char **argv)
+{
+  size_t s = sizeof(enum foo);
+  assert(s == 0);
+}

regression/cbmc/incomplete-sizeof/enum.desc

@@ -0,0 +1,9 @@
+CORE
+enum.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file enum.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
+^CONVERSION ERROR$
+--
+^warning: ignoring

regression/cbmc/incomplete-sizeof/struct.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct foo;
+
+int main(int argc, char **argv)
+{
+  struct foo *thefoo = malloc(sizeof(struct foo));
+  size_t s = sizeof(struct foo);
+  assert(s == 0);
+}

regression/cbmc/incomplete-sizeof/struct.desc

@@ -0,0 +1,9 @@
+CORE
+struct.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file struct.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
+^CONVERSION ERROR$
+--
+^warning: ignoring

regression/cbmc/incomplete-sizeof/union.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+union foo;
+
+int main(int argc, char **argv)
+{
+  size_t s = sizeof(union foo);
+  assert(s == 0);
+}

regression/cbmc/incomplete-sizeof/union.desc

@@ -0,0 +1,9 @@
+CORE
+union.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file union.c line \d+ function main: invalid application of \'sizeof\' to an incomplete type$
+^CONVERSION ERROR$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -951,6 +951,21 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
   }
   else
   {
+    if(
+      (type.id() == ID_struct_tag &&
+       follow_tag(to_struct_tag_type(type)).is_incomplete()) ||
+      (type.id() == ID_union_tag &&
+       follow_tag(to_union_tag_type(type)).is_incomplete()) ||
+      (type.id() == ID_c_enum_tag &&
+       follow_tag(to_c_enum_tag_type(type)).is_incomplete()) ||
+      (type.id() == ID_array && to_array_type(type).is_incomplete()))
+    {
+      error().source_location = expr.source_location();
+      error() << "invalid application of \'sizeof\' to an incomplete type\n\t\'"
+              << to_string(type) << "\'" << eom;
+      throw 0;
+    }
+
     auto size_of_opt = size_of_expr(type, *this);
 
     if(!size_of_opt.has_value())