Merge pull request #7215 from diffblue/architecture_integer

change type of numerical architecture symbols to integer

Author: kroening

regression/ansi-c/arch_flags_mcpu_bad/object.intel

@@ -113,7 +113,8 @@ static std::string architecture_string(const std::string &value, const char *s)
 template <typename T>
 static std::string architecture_string(T value, const char *s)
 {
-  return std::string("const int " CPROVER_PREFIX "architecture_") +
+  return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX
+                     "architecture_") +
          std::string(s) + "=" + std::to_string(value) + ";\n";
 }
 

regression/ansi-c/arch_flags_mcpu_good/object.arm

@@ -1451,12 +1451,36 @@ bool cpp_typecheckt::implicit_conversion_sequence(
   {
     rank=backup_rank;
     if(!user_defined_conversion_sequence(e, type, new_expr, rank))
+    {
+      if(
+        type.id() == ID_integer &&
+        (expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv))
+      {
+        // This is a nonstandard implicit conversion, from
+        // bit-vectors to unbounded integers.
+        rank = 0;
+        new_expr = typecast_exprt(expr, type);
+        return true;
+      }
+      else if(
+        (type.id() == ID_signedbv || type.id() == ID_unsignedbv) &&
+        expr.type().id() == ID_integer)
+      {
+        // This is a nonstandard implicit conversion, from
+        // unbounded integers to bit-vectors.
+        rank = 0;
+        new_expr = typecast_exprt(expr, type);
+        return true;
+      }
+
+      // no conversion
       return false;
+    }
 
-    #if 0
+#if 0
     simplify_exprt simplify(*this);
     simplify.simplify(new_expr);
-    #endif
+#endif
   }
 
   return true;

regression/ansi-c/arch_flags_mthumb_bad/object.intel

@@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 /// C++ Language Type Checking
 
 #include <util/c_types.h>
+#include <util/cprover_prefix.h>
+#include <util/mathematical_types.h>
 #include <util/simplify_expr.h>
 #include <util/source_location.h>
 
@@ -69,6 +71,19 @@ void cpp_typecheckt::typecheck_type(typet &type)
     if(type.get_bool(ID_C_constant))
       qualifiers.is_constant = true;
 
+    // CPROVER extensions
+    irep_idt typedef_identifier = type.get(ID_C_typedef);
+    if(typedef_identifier == CPROVER_PREFIX "rational")
+    {
+      type = rational_typet();
+      type.add_source_location() = symbol_expr.source_location();
+    }
+    else if(typedef_identifier == CPROVER_PREFIX "integer")
+    {
+      type = integer_typet();
+      type.add_source_location() = symbol_expr.source_location();
+    }
+
     qualifiers.write(type);
   }
   else if(type.id()==ID_struct ||

regression/ansi-c/arch_flags_mthumb_good/object.arm

@@ -1094,7 +1094,7 @@ bool constant_interval_exprt::is_numeric(
 
 bool constant_interval_exprt::is_int(const typet &type)
 {
-  return (is_signed(type) || is_unsigned(type));
+  return is_signed(type) || is_unsigned(type) || type.id() == ID_integer;
 }
 
 bool constant_interval_exprt::is_float(const typet &src)