direct support for ID_c_bool in exprt (#438)

The `is_true()` / `is_false()` functions in `exprt` currently support
only the `ID_bool` type. In Java, Boolean values are represented as
`ID_c_bool` due to the internal JVM usage of integers. Adding this
support here seems easier than having special treatment in
`java_bytecode`.

Author: mgudemann

src/util/expr.cpp

@@ -245,9 +245,18 @@ Function: exprt::is_true
 
 bool exprt::is_true() const
 {
-  return is_constant() &&
-         type().id()==ID_bool &&
-         get(ID_value)!=ID_false;
+  if(is_constant())
+  {
+    if(type().id()==ID_bool)
+      return get(ID_value)!=ID_false;
+    else if(type().id()==ID_c_bool)
+    {
+      mp_integer i;
+      to_integer(*this, i);
+      return i!=mp_integer(0);
+    }
+  }
+  return false;
 }
 
 /*******************************************************************\
@@ -264,9 +273,14 @@ Function: exprt::is_false
 
 bool exprt::is_false() const
 {
-  return is_constant() &&
-         type().id()==ID_bool &&
-         get(ID_value)==ID_false;
+  if(is_constant())
+  {
+    if(type().id()==ID_bool)
+      return get(ID_value)==ID_false;
+    else if(type().id()==ID_c_bool)
+      return !is_true();
+  }
+  return false;
 }
 
 /*******************************************************************\