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.

Author: marek-trtik

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);

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

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();