C front-end: fix promotion order for types ranking lower than int

The ranks specified in the enum are only correct if sizeof(int) > sizeof(short)
and sizeof(int) > sizeof(char). The code was supposed to fix this up, but none
of the branches was feasible as max_type would always be at least INT.

Fixes: diffblue#1748

Author: tautschnig

regression/cbmc/Promotion4/main.c

@@ -0,0 +1,12 @@
+int main(int argc, char *argv[])
+{
+  __CPROVER_assert(sizeof(unsigned int) == 2, "[--16] size of int is 16 bit");
+  __CPROVER_assert(
+    sizeof(unsigned long) == 4, "[--LP32] size of long is 32 bit");
+
+  unsigned int k = non_det_unsigned();
+  __CPROVER_assume(k < 1);
+  __CPROVER_assert(k != 0xffff, "false counter example 16Bit?");
+
+  return 0;
+}

regression/cbmc/Promotion4/test.desc

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

src/ansi-c/c_typecast.cpp

@@ -418,16 +418,15 @@ c_typecastt::c_typet c_typecastt::minimum_promotion(
   c_typet max_type=std::max(c_type, INT); // minimum promotion
 
   // The second case can arise if we promote any unsigned type
-  // that is as large as unsigned int.
-
-  if(config.ansi_c.short_int_width==config.ansi_c.int_width &&
-     max_type==USHORT)
+  // that is as large as unsigned int. In this case the promotion configuration
+  // via the enum is actually wrong, and we need to fix this up.
+  if(
+    config.ansi_c.short_int_width == config.ansi_c.int_width &&
+    c_type == USHORT)
     max_type=UINT;
-  else if(config.ansi_c.char_width==config.ansi_c.int_width &&
-          max_type==UCHAR)
+  else if(
+    config.ansi_c.char_width == config.ansi_c.int_width && c_type == UCHAR)
     max_type=UINT;
-  else
-    max_type=std::max(max_type, INT);
 
   if(max_type==UINT &&
      type.id()==ID_c_bit_field &&