From ef1f40a0c15221e90ae76f81f2bee74189877306 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 13 Apr 2021 15:05:53 +0000
Subject: [PATCH] C front-end: support ID_integer-typed expressions in
 get_c_type

Mathematical integers were wrongly considered "OTHER," resulting in
missing type casts as demonstrated by the included regression test.
---
 .../integer-assignments1/integer-typecheck.desc    | 14 ++++++++++++++
 regression/validate-trace-xml-schema/check.py      |  1 +
 src/ansi-c/c_typecast.cpp                          |  2 ++
 3 files changed, 17 insertions(+)
 create mode 100644 regression/cbmc/integer-assignments1/integer-typecheck.desc

diff --git a/regression/cbmc/integer-assignments1/integer-typecheck.desc b/regression/cbmc/integer-assignments1/integer-typecheck.desc
new file mode 100644
index 00000000000..612dfad45eb
--- /dev/null
+++ b/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.
diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py
index 0b153f61854..91d373195b0 100644
--- a/regression/validate-trace-xml-schema/check.py
+++ b/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'],
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 21a5c21f9b6..54e5d0c8a28 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/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;
 }