Merge pull request #6030 from tautschnig/integer-promotion

C front-end: support ID_integer-typed expressions in get_c_type

Author: kroening

regression/cbmc/integer-assignments1/integer-typecheck.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* cast\(100, ℤ\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* 100$
+--
+implicit_typecast_arithmetic previously failed to insert a typecast for the
+(mathematical) integer-typed expression. This resulted in a multiplication over
+mixed types, which sometimes (!) resulted in an invariant failure during
+simplification. This was first observed when compiling with GCC 10, cf.
+discussion in #6028.

regression/validate-trace-xml-schema/check.py

@@ -22,6 +22,7 @@
     ['xml-interface1', 'test.desc'],
     ['xml-interface1', 'test_wrong_flag.desc'],
     # these want --show-goto-functions instead of producing a trace
+    ['integer-assignments1', 'integer-typecheck.desc'],
     ['destructors', 'compound_literal.desc'],
     ['destructors', 'enter_lexical_block.desc'],
     ['reachability-slice-interproc2', 'test.desc'],

src/ansi-c/c_typecast.cpp

@@ -382,6 +382,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
 
     return get_c_type(new_type);
   }
+  else if(type.id() == ID_integer)
+    return INTEGER;
 
   return OTHER;
 }