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

@@ -44,14 +44,31 @@ 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
 

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();