c_types.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_C_TYPES_H
#define CPROVER_UTIL_C_TYPES_H
 
#include "deprecate.h"
#include "pointer_expr.h"
 
class c_bit_field_typet : public bitvector_typet
{
public:
  explicit c_bit_field_typet(typet _subtype, std::size_t width)
    : bitvector_typet(ID_c_bit_field, width)
  {
    add_subtype() = std::move(_subtype);
  }
 
  // These have a sub-type. The preferred way to access it
  // are the underlying_type methods.
  const typet &underlying_type() const
  {
    return subtype();
  }
 
  typet &underlying_type()
  {
    return subtype();
  }
 
  // Use .underlying_type() instead -- this method will be removed
  const typet &subtype() const
  {
    // The existence of get_sub() front is enforced by check(...)
    return static_cast<const typet &>(get_sub().front());
  }
 
  // Use .underlying_type() instead -- this method will be removed
  typet &subtype()
  {
    // The existence of get_sub() front is enforced by check(...)
    return static_cast<typet &>(get_sub().front());
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    bitvector_typet::check(type, vm);
    type_with_subtypet::check(type, vm);
  }
};
 
template <>
inline bool can_cast_type<c_bit_field_typet>(const typet &type)
{
  return type.id() == ID_c_bit_field;
}
 
inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
{
  PRECONDITION(can_cast_type<c_bit_field_typet>(type));
  c_bit_field_typet::check(type);
  return static_cast<const c_bit_field_typet &>(type);
}
 
inline c_bit_field_typet &to_c_bit_field_type(typet &type)
{
  PRECONDITION(can_cast_type<c_bit_field_typet>(type));
  type_with_subtypet::check(type);
  return static_cast<c_bit_field_typet &>(type);
}
 
class c_bool_typet : public bitvector_typet
{
public:
  explicit c_bool_typet(std::size_t width) : bitvector_typet(ID_c_bool, width)
  {
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width");
  }
};
 
template <>
inline bool can_cast_type<c_bool_typet>(const typet &type)
{
  return type.id() == ID_c_bool;
}
 
inline const c_bool_typet &to_c_bool_type(const typet &type)
{
  PRECONDITION(can_cast_type<c_bool_typet>(type));
  c_bool_typet::check(type);
  return static_cast<const c_bool_typet &>(type);
}
 
inline c_bool_typet &to_c_bool_type(typet &type)
{
  PRECONDITION(can_cast_type<c_bool_typet>(type));
  c_bool_typet::check(type);
  return static_cast<c_bool_typet &>(type);
}
 
class union_typet : public struct_union_typet
{
public:
  union_typet() : struct_union_typet(ID_union)
  {
  }
 
  explicit union_typet(componentst _components)
    : struct_union_typet(ID_union, std::move(_components))
  {
  }
 
  std::optional<std::pair<struct_union_typet::componentt, mp_integer>>
  find_widest_union_component(const namespacet &ns) const;
};
 
template <>
inline bool can_cast_type<union_typet>(const typet &type)
{
  return type.id() == ID_union;
}
 
inline const union_typet &to_union_type(const typet &type)
{
  PRECONDITION(can_cast_type<union_typet>(type));
  return static_cast<const union_typet &>(type);
}
 
inline union_typet &to_union_type(typet &type)
{
  PRECONDITION(can_cast_type<union_typet>(type));
  return static_cast<union_typet &>(type);
}
 
class union_tag_typet : public struct_or_union_tag_typet
{
public:
  explicit union_tag_typet(const irep_idt &identifier)
    : struct_or_union_tag_typet(ID_union_tag, identifier)
  {
  }
};
 
template <>
inline bool can_cast_type<union_tag_typet>(const typet &type)
{
  return type.id() == ID_union_tag;
}
 
inline const union_tag_typet &to_union_tag_type(const typet &type)
{
  PRECONDITION(can_cast_type<union_tag_typet>(type));
  return static_cast<const union_tag_typet &>(type);
}
 
inline union_tag_typet &to_union_tag_type(typet &type)
{
  PRECONDITION(can_cast_type<union_tag_typet>(type));
  return static_cast<union_tag_typet &>(type);
}
 
class c_enum_typet : public type_with_subtypet
{
public:
  explicit c_enum_typet(typet _subtype)
    : type_with_subtypet(ID_c_enum, std::move(_subtype))
  {
  }
 
  class c_enum_membert : public irept
  {
  public:
    irep_idt get_value() const
    {
      return get(ID_value);
    }
    void set_value(const irep_idt &value)
    {
      set(ID_value, value);
    }
    irep_idt get_identifier() const
    {
      return get(ID_identifier);
    }
    void set_identifier(const irep_idt &identifier)
    {
      set(ID_identifier, identifier);
    }
    irep_idt get_base_name() const
    {
      return get(ID_base_name);
    }
    void set_base_name(const irep_idt &base_name)
    {
      set(ID_base_name, base_name);
    }
  };
 
  typedef std::vector<c_enum_membert> memberst;
 
  c_enum_typet(typet _subtype, memberst enum_members)
    : c_enum_typet(std::move(_subtype))
  {
    members() = std::move(enum_members);
  }
 
  memberst &members()
  {
    return reinterpret_cast<memberst &>(add(ID_body).get_sub());
  }
 
  const memberst &members() const
  {
    return (const memberst &)(find(ID_body).get_sub());
  }
 
  bool is_incomplete() const
  {
    return get_bool(ID_incomplete);
  }
 
  void make_incomplete()
  {
    set(ID_incomplete, true);
  }
 
  // The preferred way to access the subtype
  // are the underlying_type methods.
  const typet &underlying_type() const
  {
    return subtype();
  }
 
  typet &underlying_type()
  {
    return subtype();
  }
};
 
template <>
inline bool can_cast_type<c_enum_typet>(const typet &type)
{
  return type.id() == ID_c_enum;
}
 
inline const c_enum_typet &to_c_enum_type(const typet &type)
{
  PRECONDITION(can_cast_type<c_enum_typet>(type));
  type_with_subtypet::check(type);
  return static_cast<const c_enum_typet &>(type);
}
 
inline c_enum_typet &to_c_enum_type(typet &type)
{
  PRECONDITION(can_cast_type<c_enum_typet>(type));
  type_with_subtypet::check(type);
  return static_cast<c_enum_typet &>(type);
}
 
class c_enum_tag_typet : public tag_typet
{
public:
  explicit c_enum_tag_typet(const irep_idt &identifier)
    : tag_typet(ID_c_enum_tag, identifier)
  {
  }
};
 
template <>
inline bool can_cast_type<c_enum_tag_typet>(const typet &type)
{
  return type.id() == ID_c_enum_tag;
}
 
inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
{
  PRECONDITION(can_cast_type<c_enum_tag_typet>(type));
  return static_cast<const c_enum_tag_typet &>(type);
}
 
inline c_enum_tag_typet &to_c_enum_tag_type(typet &type)
{
  PRECONDITION(can_cast_type<c_enum_tag_typet>(type));
  return static_cast<c_enum_tag_typet &>(type);
}
 
class code_with_contract_typet : public code_typet
{
public:
  code_with_contract_typet(parameterst _parameters, typet _return_type)
    : code_typet(std::move(_parameters), std::move(_return_type))
  {
  }
 
  bool has_contract() const
  {
    return !c_ensures().empty() || !c_requires().empty() ||
           !c_assigns().empty() || !c_frees().empty();
  }
 
  const exprt::operandst &c_assigns() const
  {
    return static_cast<const exprt &>(find(ID_C_spec_assigns)).operands();
  }
 
  exprt::operandst &c_assigns()
  {
    return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
  }
 
  const exprt::operandst &c_frees() const
  {
    return static_cast<const exprt &>(find(ID_C_spec_frees)).operands();
  }
 
  exprt::operandst &c_frees()
  {
    return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
  }
 
  const exprt::operandst &c_requires() const
  {
    return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
  }
 
  exprt::operandst &c_requires()
  {
    return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
  }
 
  const exprt::operandst &c_ensures() const
  {
    return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
  }
 
  exprt::operandst &c_ensures()
  {
    return static_cast<exprt &>(add(ID_C_spec_ensures)).operands();
  }
};
 
template <>
inline bool can_cast_type<code_with_contract_typet>(const typet &type)
{
  return type.id() == ID_code;
}
 
inline const code_with_contract_typet &
to_code_with_contract_type(const typet &type)
{
  PRECONDITION(can_cast_type<code_with_contract_typet>(type));
  code_with_contract_typet::check(type);
  return static_cast<const code_with_contract_typet &>(type);
}
 
inline code_with_contract_typet &to_code_with_contract_type(typet &type)
{
  PRECONDITION(can_cast_type<code_with_contract_typet>(type));
  code_with_contract_typet::check(type);
  return static_cast<code_with_contract_typet &>(type);
}
 
bitvector_typet c_index_type();
signedbv_typet signed_int_type();
unsignedbv_typet unsigned_int_type();
signedbv_typet signed_long_int_type();
signedbv_typet signed_short_int_type();
unsignedbv_typet unsigned_short_int_type();
signedbv_typet signed_long_long_int_type();
unsignedbv_typet unsigned_long_int_type();
unsignedbv_typet unsigned_long_long_int_type();
typet c_bool_type();
bitvector_typet char_type();
unsignedbv_typet unsigned_char_type();
signedbv_typet signed_char_type();
bitvector_typet wchar_t_type();
unsignedbv_typet char16_t_type();
unsignedbv_typet char32_t_type();
floatbv_typet float_type();
floatbv_typet double_type();
floatbv_typet long_double_type();
unsignedbv_typet size_type();
signedbv_typet signed_size_type();
signedbv_typet pointer_diff_type();
pointer_typet pointer_type(const typet &);
empty_typet void_type();
 
// This is for Java and C++
reference_typet reference_type(const typet &);
 
// Turns an ID_C_c_type into a string, e.g.,
// ID_signed_int gets "signed int".
std::string c_type_as_string(const irep_idt &);
 
#endif // CPROVER_UTIL_C_TYPES_H