Improve type utility functions

Better names and small code refactoring.

Author: petr-bauch

src/ansi-c/c_typecast.cpp

@@ -213,11 +213,15 @@ bool check_c_implicit_typecast(
       const irept &src_subtype =src_type.subtype();
 
       if(src_subtype == dest_subtype)
+      {
         return false;
+      }
       else if(
         has_a_void_pointer(src_type) || // from void to anything
         has_a_void_pointer(dest_type))  // to void from anything
+      {
         return false;
+      }
     }
 
     if(dest_type.id()==ID_array &&

src/util/c_types_util.h

@@ -1,11 +1,18 @@
-// Copyright 2018 Author: Malte Mues <[email protected]>
+/*******************************************************************\
+
+Module: API to expression classes
+
+Author: Malte Mues <[email protected]>
+
+\*******************************************************************/
 
-/// \file
-/// This file contains functions, that should support test for underlying
-/// c types, in cases where this is required for anlysis purpose.
 #ifndef CPROVER_UTIL_C_TYPES_UTIL_H
 #define CPROVER_UTIL_C_TYPES_UTIL_H
 
+/// \file
+/// This file contains functions, that should support test for underlying
+/// c types, in cases where this is required for analysis purpose.
+
 #include "arith_tools.h"
 #include "invariant.h"
 #include "std_types.h"
@@ -15,7 +22,7 @@
 #include <string>
 
 /// This function checks, whether this has been a char type in the c program.
-inline bool is_c_char(const typet &type)
+inline bool is_c_char_type(const typet &type)
 {
   const irep_idt &c_type = type.get(ID_C_c_type);
   return is_signed_or_unsigned_bitvector(type) &&
@@ -25,16 +32,16 @@ inline bool is_c_char(const typet &type)
 
 /// This function checks, whether the type
 /// has been a bool type in the c program.
-inline bool is_c_bool(const typet &type)
+inline bool is_c_bool_type(const typet &type)
 {
   return type.id() == ID_c_bool;
 }
 
-/// This function checks, whether the type is has been some kind of integer
+/// This function checks, whether the type has been some kind of integer
 /// type in the c program.
 /// It considers the signed and unsigned verison of
 /// int, short, long and long long as integer types in c.
-inline bool is_c_int_derivate(const typet &type)
+inline bool is_c_integral_type(const typet &type)
 {
   const irep_idt &c_type = type.get(ID_C_c_type);
   return is_signed_or_unsigned_bitvector(type) &&
@@ -47,63 +54,72 @@ inline bool is_c_int_derivate(const typet &type)
 
 /// This function checks, whether type is a pointer and the target type
 /// of the pointer has been a char type in the c program.
-inline bool is_c_char_pointer(const typet &type)
+inline bool is_c_char_pointer_type(const typet &type)
 {
-  return type.id() == ID_pointer && is_c_char(type.subtype());
+  return type.id() == ID_pointer && is_c_char_type(type.subtype());
 }
 
 /// This function checks, whether type is a pointer and the target type
 /// has been some kind of int type in the c program.
 /// is_c_int_derivate answers is used for checking the int type.
-inline bool is_c_int_derivate_pointer(const typet &type)
+inline bool is_c_integral_pointer_type(const typet &type)
 {
-  return type.id() == ID_pointer && is_c_int_derivate(type.subtype());
+  return type.id() == ID_pointer && is_c_integral_type(type.subtype());
 }
 
 /// This function checks, whether the type
 /// has been an enum type in the c program.
-inline bool is_c_enum(const typet &type)
+inline bool is_c_enum_type(const typet &type)
 {
   return type.id() == ID_c_enum;
 }
 
 /// This function creates a constant representing the
 /// bitvector encoded integer value of a string in the enum.
 /// \param member_name is a string that should be in the enum.
-/// \param c_enum the enum type memeber_name is supposed to be part of.
-/// \return value a constant, that could be assigned as value for an expression
-/// with type c_enum.
+/// \param c_enum the enum type \p member_name is supposed to be part of.
+/// \return constant, that could be assigned as the value of an expression with
+///   type c_enum.
 constant_exprt convert_member_name_to_enum_value(
-  const std::string &member_name,
+  const irep_idt &member_name,
   const c_enum_typet &c_enum)
 {
   for(const auto &enum_value : c_enum.members())
   {
-    if(id2string(enum_value.get_identifier()) == member_name)
+    if(enum_value.get_identifier() == member_name)
     {
-      mp_integer int_value = string2integer(id2string(enum_value.get_value()));
-      return from_integer(int_value, c_enum);
+      auto maybe_int_value = numeric_cast<mp_integer>(
+        constant_exprt{enum_value.get_value(), typet{ID_bv}});
+      CHECK_RETURN(maybe_int_value.has_value());
+      return from_integer(*maybe_int_value, c_enum);
     }
   }
   INVARIANT(false, "member_name must be a valid value in the c_enum.");
 }
 
+/// Convert id to a Boolean value
+/// \param bool_value: A string that is compared to "true" ignoring case.
+/// \return a constant of type Boolean
+bool id2boolean(const irep_idt &bool_value)
+{
+  std::string string_value = id2string(bool_value);
+  std::transform(
+    string_value.begin(), string_value.end(), string_value.begin(), ::tolower);
+  if(string_value == "true")
+    return true;
+  if(string_value == "false")
+    return false;
+  UNREACHABLE;
+}
+
 /// This function creates a constant representing either 0 or 1 as value of
 /// type type.
-/// \param bool_value: A string that is compared to "true" ignoring case.
+/// \param bool_value: A Boolean value.
 /// \param type: The type, the resulting constant is supposed to have.
 /// \return a constant of type \param type with either 0 or 1 as value.
-constant_exprt from_c_boolean_value(std::string bool_value, const typet &type)
+constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
 {
-  std::transform(
-    bool_value.begin(), bool_value.end(), bool_value.begin(), ::tolower);
-  if(bool_value == "true")
-  {
-    return from_integer(mp_integer(1), type);
-  }
-  else
-  {
-    return from_integer(mp_integer(0), type);
-  }
+  return bool_value ? from_integer(mp_integer(1), type)
+                    : from_integer(mp_integer(0), type);
 }
 #endif // CPROVER_UTIL_C_TYPES_UTIL_H

src/util/std_types.h

@@ -29,7 +29,7 @@ class namespacet;
 /// if the given typet is a constant
 inline bool is_constant(const typet &type)
 {
-  return type.id() == ID_constant;
+  return type.get_bool(ID_C_constant);
 }
 
 /// The Boolean type