Annotate flexible array members

Make sure we can distinguish flexible array members from other arrays,
for example when wanting to distinguish their compile-time from their
runtime size.

Author: tautschnig

src/analyses/goto_check_c.cpp

@@ -1628,15 +1628,17 @@ void goto_check_ct::bounds_check_index(
                         ? to_array_type(array_type).size()
                         : to_vector_type(array_type).size();
 
-  if(size.is_nil())
+  if(size.is_nil() && !array_type.get_bool(ID_C_flexible_array_member))
   {
     // Linking didn't complete, we don't have a size.
     // Not clear what to do.
   }
   else if(size.id() == ID_infinity)
   {
   }
-  else if(size.is_zero() && expr.array().id() == ID_member)
+  else if(
+    expr.array().id() == ID_member &&
+    (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))
   {
     // a variable sized struct member
     //

src/ansi-c/c_typecheck_type.cpp

@@ -1010,8 +1010,8 @@ void c_typecheck_baset::typecheck_compound_body(
         }
 
         // make it zero-length
-        c_type.id(ID_array);
-        c_type.set(ID_size, from_integer(0, c_index_type()));
+        to_array_type(c_type).size() = from_integer(0, c_index_type());
+        c_type.set(ID_C_flexible_array_member, true);
       }
     }
   }

src/util/irep_ids.def

@@ -867,6 +867,7 @@ IREP_ID_ONE(empty_union)
 IREP_ID_ONE(bitreverse)
 IREP_ID_ONE(saturating_minus)
 IREP_ID_ONE(saturating_plus)
+IREP_ID_TWO(C_flexible_array_member, #flexible_array_member)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/pointer_offset_size.cpp

@@ -368,6 +368,11 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
         if(bytes > 0)
           result = plus_exprt(result, from_integer(bytes, result.type()));
       }
+      else if(c.type().get_bool(ID_C_flexible_array_member))
+      {
+        // flexible array members do not change the sizeof result
+        continue;
+      }
       else
       {
         DATA_INVARIANT(
@@ -569,7 +574,10 @@ build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
   if(type.is_nil())
     return {};
 
-  const auto type_size = pointer_offset_size(type, ns);
+  const auto type_size_expr = size_of_expr(type, ns);
+  optionalt<mp_integer> type_size;
+  if(type_size_expr.has_value())
+    type_size = numeric_cast<mp_integer>(*type_size_expr);
   auto val = numeric_cast<mp_integer>(expr);
 
   if(

src/util/simplify_expr.cpp

@@ -1746,6 +1746,9 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       if(comps.empty() || comps.back().type().id() != ID_array)
         return false;
 
+      if(comps.back().type().get_bool(ID_C_flexible_array_member))
+        return true;
+
       const auto size =
         numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
       return !size.has_value() || *size <= 1;