diff --git a/regression/cbmc/complex/complex_initialization1.c b/regression/cbmc/complex/complex_initialization1.c new file mode 100644 index 00000000000..1d52dcbf6aa --- /dev/null +++ b/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; +} diff --git a/regression/cbmc/complex/complex_initialization1.desc b/regression/cbmc/complex/complex_initialization1.desc new file mode 100644 index 00000000000..068833d4819 --- /dev/null +++ b/regression/cbmc/complex/complex_initialization1.desc @@ -0,0 +1,8 @@ +CORE +complex_initialization1.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index eebba08236b..e17d59966c7 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/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,