c_types_util.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: API to expression classes
 
Author: Malte Mues <mail.mues@gmail.com>
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_C_TYPES_UTIL_H
#define CPROVER_UTIL_C_TYPES_UTIL_H
 
 
#include "arith_tools.h"
#include "invariant.h"
#include "std_types.h"
#include "type.h"
 
#include <algorithm>
#include <string>
 
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) &&
         (c_type == ID_char || c_type == ID_unsigned_char ||
          c_type == ID_signed_char);
}
 
inline bool is_c_bool_type(const typet &type)
{
  return type.id() == ID_c_bool;
}
 
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) &&
         (c_type == ID_signed_int || c_type == ID_unsigned_int ||
          c_type == ID_signed_short_int || c_type == ID_unsigned_int ||
          c_type == ID_unsigned_short_int || c_type == ID_signed_long_int ||
          c_type == ID_signed_long_long_int || c_type == ID_unsigned_long_int ||
          c_type == ID_unsigned_long_long_int);
}
 
inline bool is_c_char_pointer_type(const typet &type)
{
  return type.id() == ID_pointer &&
         is_c_char_type(to_pointer_type(type).base_type());
}
 
inline bool is_c_integral_pointer_type(const typet &type)
{
  return type.id() == ID_pointer &&
         is_c_integral_type(to_pointer_type(type).base_type());
}
 
inline bool is_c_enum_type(const typet &type)
{
  return type.id() == ID_c_enum;
}
 
inline constant_exprt convert_member_name_to_enum_value(
  const irep_idt &member_name,
  const c_enum_typet &c_enum)
{
  for(const auto &enum_value : c_enum.members())
  {
    if(enum_value.get_identifier() == member_name)
    {
      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.");
}
 
inline bool id2boolean(const std::string &bool_value)
{
  std::string string_value = 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;
}
 
inline constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
{
  return bool_value ? from_integer(mp_integer(1), type)
                    : from_integer(mp_integer(0), type);
}
#endif // CPROVER_UTIL_C_TYPES_UTIL_H