From 8f8cda4ac3ba827453524026cd4fbcdf658c7897 Mon Sep 17 00:00:00 2001
From: Marek Trtik <marek.trtik@diffblue.com>
Date: Sun, 26 Nov 2017 12:23:56 +0000
Subject: [PATCH] Fixing issue 'implicit conversion not permitted' for alias
 variables.

There are several SV-COMP benchmarks where is used and alias
variable with a global array variable. The alias varialbe is not
array ariable and it wants to alias with the array, i.e. with the
first element in the array. This commit prevents the type mismatch.
---
 src/ansi-c/c_typecast.cpp           | 19 ++++++++++++++++++-
 src/ansi-c/c_typecast.h             |  8 +++++++-
 src/ansi-c/c_typecheck_typecast.cpp |  1 +
 3 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 9d51bca80e8..6a3f6daf9fa 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -456,6 +456,23 @@ void c_typecastt::implicit_typecast(
   implicit_typecast_followed(expr, src_type, type_qual, dest_type);
 }
 
+static bool is_array_element_alias(const namespacet& ns, const symbolt* const orig_symbol, const typet &src_type, const typet &dest_type)
+{
+  if(orig_symbol==nullptr)
+    return false;
+  const symbolt* aliased_symbol;
+  if(ns.lookup(orig_symbol->name, aliased_symbol))
+    return false;
+  if(!aliased_symbol->is_macro)
+    return false;
+  if(src_type.id()!=ID_array)
+    return false;
+  const typet &src_subtype=ns.follow(src_type.subtype());
+  if(src_subtype!=dest_type)
+    return false;
+  return true;
+}
+
 void c_typecastt::implicit_typecast_followed(
   exprt &expr,
   const typet &src_type,
@@ -569,7 +586,7 @@ void c_typecastt::implicit_typecast_followed(
     }
   }
 
-  if(check_c_implicit_typecast(src_type, dest_type))
+  if(check_c_implicit_typecast(src_type, dest_type) && !is_array_element_alias(ns, get_current_symbol(), src_type, dest_type))
     errors.push_back("implicit conversion not permitted");
   else if(src_type!=dest_type)
     do_typecast(expr, orig_dest_type);
diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h
index 11e379f3935..75db13ece88 100644
--- a/src/ansi-c/c_typecast.h
+++ b/src/ansi-c/c_typecast.h
@@ -41,7 +41,7 @@ bool c_implicit_typecast_arithmetic(
 class c_typecastt
 {
 public:
-  explicit c_typecastt(const namespacet &_ns):ns(_ns)
+  explicit c_typecastt(const namespacet &_ns):ns(_ns), current_symbol(nullptr)
   {
   }
 
@@ -63,6 +63,9 @@ class c_typecastt
   std::list<std::string> errors;
   std::list<std::string> warnings;
 
+  void set_current_symbol(const symbolt * const symbol) { current_symbol=symbol; }
+  const symbolt *get_current_symbol() const { return current_symbol; }
+
 protected:
   const namespacet &ns;
 
@@ -100,6 +103,9 @@ class c_typecastt
   void do_typecast(exprt &dest, const typet &type);
 
   c_typet minimum_promotion(const typet &type) const;
+
+private:
+  const symbolt *current_symbol;
 };
 
 #endif // CPROVER_ANSI_C_C_TYPECAST_H
diff --git a/src/ansi-c/c_typecheck_typecast.cpp b/src/ansi-c/c_typecheck_typecast.cpp
index 2ce03d83f18..0672d1019d2 100644
--- a/src/ansi-c/c_typecheck_typecast.cpp
+++ b/src/ansi-c/c_typecheck_typecast.cpp
@@ -15,6 +15,7 @@ void c_typecheck_baset::implicit_typecast(
   const typet &dest_type)
 {
   c_typecastt c_typecast(*this);
+  c_typecast.set_current_symbol(&current_symbol);
 
   typet src_type=expr.type();