Merge pull request #1751 from tautschnig/fix-1748

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

Author: kroening

regression/cbmc/Pointer_byte_extract5/main.c

@@ -1,4 +1,4 @@
-#include <stdlib.h>
+void *malloc(__CPROVER_size_t);
 
 typedef union
 {

regression/cbmc/Pointer_byte_extract8/main.c

@@ -1,4 +1,4 @@
-#include <stdlib.h>
+void *malloc(__CPROVER_size_t);
 
 typedef union
 {

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

regression/cbmc/address_space_size_limit2/test.c

@@ -1,6 +1,7 @@
-#include <stdlib.h>
 #include <assert.h>
 
+void *malloc(__CPROVER_size_t);
+
 int main(int argc, char** argv)
 {
   char* c=(char*)malloc(10);

src/ansi-c/c_preprocess.cpp

@@ -437,13 +437,20 @@ bool c_preprocess_visual_studio(
       // yes, both _WIN32 and _WIN64 get defined
       command_file << "/D_WIN64" << "\n";
     }
+    else if(config.ansi_c.int_width == 16 && config.ansi_c.pointer_width == 32)
+    {
+      // 16-bit LP32 is an artificial architecture we simulate when using --16
+      DATA_INVARIANT(
+        pointer_diff_type() == signed_long_int_type(),
+        "Pointer difference expected to be long int typed");
+      command_file << "/D__PTRDIFF_TYPE__=long" << '\n';
+    }
     else
     {
       DATA_INVARIANT(
         pointer_diff_type()==signed_int_type(),
         "Pointer difference expected to be int typed");
       command_file << "/D__PTRDIFF_TYPE__=int" << "\n";
-      command_file << "/U_WIN64" << "\n";
     }
 
     if(config.ansi_c.char_is_unsigned)

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 &&