Merge pull request #3720 from diffblue/fix-compound-assignment-promotion

Fix compound assignment promotion

Author: Daniel Kroening

regression/cbmc/Fixedbv1/main.c

@@ -5,13 +5,13 @@ int main() {
   int y;
 
   x=2;
-  x-=0.6;
+  x -= (__CPROVER_fixedbv[64][32])0.6;
   y=x; // this yields 1.4, which is cut off
 
   assert(y==1);
 
   x=2;
-  x-=0.4;
+  x -= (__CPROVER_fixedbv[64][32])0.4;
   y=x; // this yields 1.6, which is cut off, too!
 
   assert(y==1);

regression/cbmc/compound-assignment/compound_promotion.desc

@@ -1,5 +1,5 @@
-KNOWNBUG
-compound_promition.c
+CORE
+compound_promotion.c
 
 ^EXIT=0$
 ^SIGNAL=0$

src/ansi-c/c_typecheck_expr.cpp

@@ -3458,7 +3458,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
     }
     else
     {
-      implicit_typecast(op1, o_type0);
+      implicit_typecast_arithmetic(op0, op1);
 
       if(is_number(op1.type()) ||
          op1.type().id()==ID_bool ||