Merge pull request #8265 from diffblue/complex_initialization1

initialisation of `_Complex` with an initializer list

Author: tautschnig

regression/cbmc/complex/complex_initialization1.c

@@ -0,0 +1,12 @@
+_Complex float var1 = 1 + 2i;
+_Complex float var2 = {1, 2};
+_Complex float var3 = {1 + 2i};
+_Complex float var4 = {1 + 3i, 2};
+
+int main(void)
+{
+  __CPROVER_assert(var1 == var2, "var1 vs var2");
+  __CPROVER_assert(var1 == var3, "var1 vs var3");
+  __CPROVER_assert(var1 == var4, "var1 vs var4");
+  return 0;
+}

regression/cbmc/complex/complex_initialization1.desc

@@ -0,0 +1,8 @@
+CORE
+complex_initialization1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_initializer.cpp

@@ -969,6 +969,32 @@ exprt c_typecheck_baset::do_initializer_list(
       result = *zero;
     }
   }
+  else if(type.id() == ID_complex)
+  {
+    // These may be initialized with an expression, an initializer list
+    // of size two, or an initializer list of size one.
+    if(value.operands().size() == 1)
+    {
+      return do_initializer_rec(
+        to_unary_expr(value).op(), type, force_constant);
+    }
+    else if(value.operands().size() == 2)
+    {
+      auto &complex_type = to_complex_type(type);
+      auto &subtype = complex_type.subtype();
+      auto real = do_initializer_rec(
+        to_binary_expr(value).op0(), subtype, force_constant);
+      auto imag = do_initializer_rec(
+        to_binary_expr(value).op1(), subtype, force_constant);
+      return complex_exprt(real, imag, complex_type)
+        .with_source_location(value.source_location());
+    }
+    else
+    {
+      throw errort().with_location(value.source_location())
+        << "too many initializers for '" << to_string(type) << "'";
+    }
+  }
   else
   {
     // The initializer for a scalar shall be a single expression,