Support decrement operators over complex numbers

We already did so for increment, decrement just requires the same special case.

Author: tautschnig

regression/cbmc/complex1/main.c

@@ -2,7 +2,7 @@
 
 int main()
 {
-  #ifdef __GNUC__
+#ifdef __GNUC__
   _Complex c; // this is usually '_Complex double'
   c=1.0i+2;
 
@@ -21,10 +21,10 @@ int main()
 
   // The real part is stored first in memory on i386.
   // Need to find out about other architectures.
-  #if defined(__i386__) || defined(__amd64__)
+#if defined(__i386__) || defined(__amd64__)
   assert(((signed char *)&char_complex)[0]==-2);
   assert(((signed char *)&char_complex)[1]==3);
-  #endif
+#endif
 
   assert(__real__ char_complex == -2);
   assert(__imag__ char_complex == 3);
@@ -44,18 +44,35 @@ int main()
   char_complex++;
   assert(__real__ char_complex == 101);
   assert(__imag__ char_complex == 3);
+  ++char_complex;
+  assert(__real__ char_complex == 102);
+  assert(__imag__ char_complex == 3);
+  char_complex += 1;
+  assert(__real__ char_complex == 103);
+  assert(__imag__ char_complex == 3);
 
   // also separately
   (__real__ char_complex)++;
-  assert(__real__ char_complex == 102);
+  assert(__real__ char_complex == 104);
   assert(__imag__ char_complex == 3);
 
   // casts to reals produce the real part
-  assert((int) char_complex == 102);
+  assert((int)char_complex == 104);
+
+  // can be decremented
+  char_complex--;
+  assert(__real__ char_complex == 103);
+  assert(__imag__ char_complex == 3);
+  --char_complex;
+  assert(__real__ char_complex == 102);
+  assert(__imag__ char_complex == 3);
+  char_complex -= 1;
+  assert(__real__ char_complex == 101);
+  assert(__imag__ char_complex == 3);
 
-  #else
+#else
 
   // Visual studio doesn't have it
 
-  #endif
+#endif
 }

src/goto-programs/goto_convert_side_effect.cpp

@@ -167,30 +167,20 @@ void goto_convertt::remove_pre(
   {
     UNREACHABLE;
   }
-  else if(op_type.id()==ID_c_enum ||
-          op_type.id()==ID_c_enum_tag)
+
+  exprt constant;
+
+  if(constant_type.id() == ID_complex)
   {
-    rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
-    rhs.op0().make_typecast(signed_int_type());
-    rhs.type()=signed_int_type();
-    rhs.make_typecast(op_type);
+    exprt real = from_integer(1, constant_type.subtype());
+    exprt imag = from_integer(0, constant_type.subtype());
+    constant = complex_exprt(real, imag, to_complex_type(constant_type));
   }
   else
-  {
-    typet constant_type;
-
-    if(op_type.id()==ID_pointer)
-      constant_type=index_type();
-    else if(is_number(op_type) || op_type.id()==ID_c_bool)
-      constant_type=op_type;
-    else
-    {
-      UNREACHABLE;
-    }
+    constant = from_integer(1, constant_type);
 
-    rhs.add_to_operands(expr.op0(), from_integer(1, constant_type));
-    rhs.type()=expr.op0().type();
-  }
+  rhs.add_to_operands(expr.op0(), std::move(constant));
+  rhs.type() = expr.op0().type();
 
   code_assignt assignment(expr.op0(), rhs);
   assignment.add_source_location()=expr.find_source_location();