C++: __CPROVER_integer and __CPROVER_rational

This extends the C++ front-end to recognize __CPROVER_integer and
__CPROVER_rational, in the same way as done in the C frontend.

Author: kroening

src/cpp/cpp_typecheck_conversions.cpp

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

src/cpp/cpp_typecheck_type.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 /// 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 ||