From a54746f365fafbbc7c015a2528494f97d315021c Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 21 Aug 2018 12:13:20 +0100 Subject: [PATCH 1/3] Add documentation to typet --- src/util/type.cpp | 18 ++++++++++++++--- src/util/type.h | 51 +++++++++++------------------------------------ 2 files changed, 27 insertions(+), 42 deletions(-) diff --git a/src/util/type.cpp b/src/util/type.cpp index 2a235c2d652..735f8ed2129 100644 --- a/src/util/type.cpp +++ b/src/util/type.cpp @@ -1,20 +1,29 @@ /*******************************************************************\ -Module: +Module: Implementations of some functions of typet Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com \*******************************************************************/ +/// \file +/// Implementations of some functions of typet + #include "type.h" #include "std_types.h" #include "namespace.h" +/// Copy the provided type to the subtypes of this type. +/// \param type The type to add to subtypes void typet::copy_to_subtypes(const typet &type) { subtypes().push_back(type); } +/// Move the provided type to the subtypes of this type. Destroys the +/// provided type. +/// \param type The type to add to subtypes void typet::move_to_subtypes(typet &type) { subtypest &sub=subtypes(); @@ -22,6 +31,8 @@ void typet::move_to_subtypes(typet &type) sub.back().swap(type); } +/// Returns true if the type is a rational, real, integer, natural, complex, +/// unsignedbv, signedbv, floatbv or fixedbv. bool is_number(const typet &type) { const irep_idt &id=type.id(); @@ -36,8 +47,9 @@ bool is_number(const typet &type) id==ID_fixedbv; } -/// Identify if a given type is constant itself or -/// contains constant components. Examples include: +/// Identify whether a given type is constant itself or contains constant +/// components. +/// Examples include: /// - const int a; /// - struct contains_constant_pointer { int x; int * const p; }; /// - const int b[3]; diff --git a/src/util/type.h b/src/util/type.h index ddfcc77f1db..d2ea25f2d95 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -1,11 +1,14 @@ /*******************************************************************\ -Module: +Module: Defines typet, type_with_subtypet and type_with_subtypest Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com \*******************************************************************/ +/// \file +/// Defines typet, type_with_subtypet and type_with_subtypest #ifndef CPROVER_UTIL_TYPE_H #define CPROVER_UTIL_TYPE_H @@ -17,8 +20,11 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; -/*! \brief The type of an expression -*/ +/// The type of an expression, extends irept. Types may have subtypes. This is +/// modeled with two subs named “subtype” (a single type) and “subtypes” +/// (a vector of types). The class typet only adds specialized methods +/// for accessing the subtype information to the interface of irept. +/// For pre-defined types see `std_types.h`. class typet:public irept { public: @@ -90,7 +96,7 @@ class typet:public irept { remove(ID_subtype); } #endif - void move_to_subtypes(typet &type); // destroys expr + void move_to_subtypes(typet &type); void copy_to_subtypes(const typet &type); @@ -115,6 +121,7 @@ class typet:public irept } }; +/// Type with a single subtype. class type_with_subtypet:public typet { public: @@ -136,6 +143,7 @@ class type_with_subtypet:public typet #endif }; +/// Type with multiple subtypes. class type_with_subtypest:public typet { public: @@ -169,43 +177,8 @@ class type_with_subtypest:public typet for(typet::subtypest::iterator it=(type).subtypes().begin(); \ it!=(type).subtypes().end(); ++it) -/* - -pre-defined types: - universe // super type - type // another type - predicate // predicate expression (subtype and predicate) - uninterpreted // uninterpreted type with identifier - empty // void - bool // true or false - abstract // abstract super type - struct // with components: each component has name and type - // the ordering matters - rational - real - integer - complex - string - enum // with elements - // the ordering does not matter - tuple // with components: each component has type - // the ordering matters - mapping // domain -> range - bv // no interpretation - unsignedbv - signedbv // two's complement - floatbv // IEEE floating point format - code - pointer // for ANSI-C (subtype) - symbol // look in symbol table (identifier) - number // generic number super type - -*/ - bool is_number(const typet &type); -// rational, real, integer, complex, unsignedbv, signedbv, floatbv -// Is the passed in type const qualified? bool is_constant_or_has_constant_components( const typet &type, const namespacet &ns); From 7ad664c04ef38a72be41bb55d9d7a14854f1486e Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 21 Aug 2018 12:13:38 +0100 Subject: [PATCH 2/3] Add documentation to type_eq --- src/util/base_type.cpp | 13 +++++++++++++ src/util/type_eq.cpp | 16 ++++++++++++++-- src/util/type_eq.h | 5 ++++- 3 files changed, 31 insertions(+), 3 deletions(-) diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index e26a4225cf1..93324e6d700 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -320,6 +320,15 @@ bool base_type_eqt::base_type_eq_rec( return true; } +/// Check types for equality across all levels of hierarchy. For equality +/// in the top level of the hierarchy only use \ref type_eq. +/// Example: +/// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal, +/// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a") +/// .type}` will also compare equal. +/// \param type1 The first type to compare. +/// \param type2 The second type to compare. +/// \param ns The namespace, needed for resolution of symbols. bool base_type_eq( const typet &type1, const typet &type2, @@ -329,6 +338,10 @@ bool base_type_eq( return base_type_eq.base_type_eq(type1, type2); } +/// Check expressions for equality across all levels of hierarchy. +/// \param expr1 The first expression to compare. +/// \param expr2 The second expression to compare. +/// \param ns The namespace, needed for resolution of symbols. bool base_type_eq( const exprt &expr1, const exprt &expr2, diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp index 5a4e4585d94..aefd710be0a 100644 --- a/src/util/type_eq.cpp +++ b/src/util/type_eq.cpp @@ -1,13 +1,14 @@ /*******************************************************************\ -Module: Type Checking +Module: Type equality Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com \*******************************************************************/ /// \file -/// Type Checking +/// Type equality #include "type_eq.h" @@ -15,6 +16,17 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_types.h" #include "symbol.h" +/// Check types for equality at the top level. If either of the types is a +/// symbol type, i.e., a reference into the symbol table, retrieve it from +/// the namespace and compare but don't do this recursively. For equality +/// across all level in the hierarchy use \ref base_type_eq. +/// Example: +/// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal, +/// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a") +/// .type}` will not compare equal. +/// \param type1 The first type to compare. +/// \param type2 The second type to compare. +/// \param ns The namespace, needed for resolution of symbols. bool type_eq(const typet &type1, const typet &type2, const namespacet &ns) { if(type1==type2) diff --git a/src/util/type_eq.h b/src/util/type_eq.h index d871536eca8..87928026111 100644 --- a/src/util/type_eq.h +++ b/src/util/type_eq.h @@ -1,11 +1,14 @@ /*******************************************************************\ -Module: +Module: Type equality Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com \*******************************************************************/ +/// \file +/// Type equality #ifndef CPROVER_UTIL_TYPE_EQ_H #define CPROVER_UTIL_TYPE_EQ_H From 592b11429e3af89e471265d0a3de8da415e043ed Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 21 Aug 2018 12:14:01 +0100 Subject: [PATCH 3/3] Add documentation to std_types --- src/util/std_types.cpp | 14 +- src/util/std_types.h | 837 ++++++++++++++++++----------------------- 2 files changed, 372 insertions(+), 479 deletions(-) diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 1bc39932014..0712ad7cbe1 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -1,11 +1,15 @@ /*******************************************************************\ -Module: +Module: Pre-defined types Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com \*******************************************************************/ +/// \file +/// Pre-defined types + #include "std_types.h" #include "string2int.h" @@ -26,6 +30,7 @@ std::size_t floatbv_typet::get_f() const return unsafe_string2unsigned(id2string(f)); } +/// Return the sequence number of the component with given name. std::size_t struct_union_typet::component_number( const irep_idt &component_name) const { @@ -48,6 +53,7 @@ std::size_t struct_union_typet::component_number( return 0; } +/// Get the reference to a component with given name. const struct_union_typet::componentt &struct_union_typet::get_component( const irep_idt &component_name) const { @@ -73,6 +79,10 @@ typet struct_union_typet::component_type( return c.type(); } +/// Returns true if the struct is a prefix of \a other, i.e., if this struct +/// has n components then the component types and names of this struct must +/// match the first n components of \a other struct. +/// \param other Struct type to compare with. bool struct_typet::is_prefix_of(const struct_typet &other) const { const componentst &ot_components=other.components(); @@ -102,12 +112,14 @@ bool struct_typet::is_prefix_of(const struct_typet &other) const return true; // ok, *this is a prefix of ot } +/// Returns true if the type is a reference. bool is_reference(const typet &type) { return type.id()==ID_pointer && type.get_bool(ID_C_reference); } +/// Returns if the type is an R value reference. bool is_rvalue_reference(const typet &type) { return type.id()==ID_pointer && diff --git a/src/util/std_types.h b/src/util/std_types.h index 9e84cffb3f2..3cf53f56db1 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1,21 +1,18 @@ /*******************************************************************\ -Module: +Module: Pre-defined types Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com \*******************************************************************/ +/// \file +/// Pre-defined types + #ifndef CPROVER_UTIL_STD_TYPES_H #define CPROVER_UTIL_STD_TYPES_H -/*! \file util/std_types.h - * \brief API to type classes - * - * \author Daniel Kroening - * \date Sun Jul 31 21:54:44 BST 2011 -*/ - #include "expr.h" #include "mp_arith.h" #include "invariant.h" @@ -25,12 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com class constant_exprt; -/*! - * Conversion to subclasses of @ref typet -*/ - -/*! \brief The proper Booleans -*/ +/// The Boolean type class bool_typet:public typet { public: @@ -39,8 +31,8 @@ class bool_typet:public typet } }; -/*! \brief The NIL type -*/ +/// The NIL type, i.e., an invalid type, no value. Use `optional` +/// instead where possible. class nil_typet:public typet { public: @@ -49,8 +41,7 @@ class nil_typet:public typet } }; -/*! \brief The empty type -*/ +/// The empty type class empty_typet:public typet { public: @@ -59,14 +50,12 @@ class empty_typet:public typet } }; -/*! \brief The void type -*/ +/// The void type, the same as \ref empty_typet. class void_typet:public empty_typet { }; -/*! \brief Unbounded, signed integers -*/ +/// Unbounded, signed integers (mathematical integers, not bitvectors) class integer_typet:public typet { public: @@ -75,8 +64,7 @@ class integer_typet:public typet } }; -/*! \brief Natural numbers (which include zero) -*/ +/// Natural numbers including zero (mathematical integers, not bitvectors) class natural_typet:public typet { public: @@ -85,8 +73,7 @@ class natural_typet:public typet } }; -/*! \brief Unbounded, signed rational numbers -*/ +/// Unbounded, signed rational numbers class rational_typet:public typet { public: @@ -95,8 +82,7 @@ class rational_typet:public typet } }; -/*! \brief Unbounded, signed real numbers -*/ +/// Unbounded, signed real numbers class real_typet:public typet { public: @@ -105,8 +91,7 @@ class real_typet:public typet } }; -/*! \brief A reference into the symbol table -*/ +/// A reference into the symbol table class symbol_typet:public typet { public: @@ -126,39 +111,39 @@ class symbol_typet:public typet } }; -/*! \brief Cast a generic typet to a \ref symbol_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * symbol_typet. - * - * \param type Source type - * \return Object of type \ref symbol_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref symbol_typet. +/// +/// This is an unchecked conversion. \a type must be known to be +/// \ref symbol_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref symbol_typet. inline const symbol_typet &to_symbol_type(const typet &type) { PRECONDITION(type.id() == ID_symbol_type); return static_cast(type); } -/*! \copydoc to_symbol_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_symbol_type(const typet &) inline symbol_typet &to_symbol_type(typet &type) { PRECONDITION(type.id() == ID_symbol_type); return static_cast(type); } +/// Check whether a reference to a typet is a \ref symbol_typet. +/// \param type Source type. +/// \return True if \param type is a \ref symbol_typet. template <> inline bool can_cast_type(const typet &type) { return type.id() == ID_symbol_type; } -/*! \brief Base type of C structs and unions, and C++ classes -*/ +/// Base type for structs and unions +/// +/// For example C structs, C unions, C++ classes, Java classes. class struct_union_typet:public typet { public: @@ -267,33 +252,28 @@ class struct_union_typet:public typet void set_tag(const irep_idt &tag) { set(ID_tag, tag); } }; -/*! \brief Cast a generic typet to a \ref struct_union_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * struct_union_typet. - * - * \param type Source type - * \return Object of type \ref struct_union_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref struct_union_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// struct_union_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type +/// \return Object of type \ref struct_union_typet inline const struct_union_typet &to_struct_union_type(const typet &type) { PRECONDITION(type.id()==ID_struct || type.id()==ID_union); return static_cast(type); } -/*! \copydoc to_struct_union_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_struct_union_type(const typet &) inline struct_union_typet &to_struct_union_type(typet &type) { PRECONDITION(type.id()==ID_struct || type.id()==ID_union); return static_cast(type); } -/*! \brief Structure type -*/ +/// Structure type, corresponds to C style structs class struct_typet:public struct_union_typet { public: @@ -301,43 +281,42 @@ class struct_typet:public struct_union_typet { } - // returns true if the object is a prefix of \a other bool is_prefix_of(const struct_typet &other) const; }; -/*! \brief Cast a generic typet to a \ref struct_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * struct_typet. - * - * \param type Source type - * \return Object of type \ref struct_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref struct_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// struct_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref struct_typet. inline const struct_typet &to_struct_type(const typet &type) { PRECONDITION(type.id()==ID_struct); return static_cast(type); } -/*! \copydoc to_struct_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_struct_type(const typet &) inline struct_typet &to_struct_type(typet &type) { PRECONDITION(type.id()==ID_struct); return static_cast(type); } +/// Check whether a reference to a typet is a \ref struct_typet. +/// \param type Source type. +/// \return True if \param type is a \ref struct_typet. template <> inline bool can_cast_type(const typet &type) { return type.id() == ID_struct; } -/*! \brief C++ class type -*/ +/// Class type +/// +/// For example, C++ and Java classes. class class_typet:public struct_typet { public: @@ -422,39 +401,39 @@ class class_typet:public struct_typet } }; -/*! \brief Cast a generic typet to a \ref class_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * class_typet. - * - * \param type Source type - * \return Object of type \ref class_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref class_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// class_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref class_typet. inline const class_typet &to_class_type(const typet &type) { PRECONDITION(type.id()==ID_struct); return static_cast(type); } -/*! \copydoc to_class_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_class_type(const typet &) inline class_typet &to_class_type(typet &type) { PRECONDITION(type.id()==ID_struct); return static_cast(type); } +/// Check whether a reference to a typet is a \ref class_typet. +/// \param type Source type. +/// \return True if \param type is a \ref class_typet. template <> inline bool can_cast_type(const typet &type) { return can_cast_type(type) && type.get_bool(ID_C_class); } -/*! \brief The union type -*/ +/// The union type +/// +/// For example, C union. class union_typet:public struct_union_typet { public: @@ -463,34 +442,28 @@ class union_typet:public struct_union_typet } }; -/*! \brief Cast a generic typet to a \ref union_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * union_typet. - * - * \param type Source type - * \return Object of type \ref union_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref union_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// union_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref union_typet inline const union_typet &to_union_type(const typet &type) { PRECONDITION(type.id()==ID_union); return static_cast(type); } -/*! \copydoc to_union_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_union_type(const typet &) inline union_typet &to_union_type(typet &type) { PRECONDITION(type.id()==ID_union); return static_cast(type); } -/*! \brief A generic tag-based type -*/ - +/// A tag-based type, i.e., \ref typet with an identifier class tag_typet:public typet { public: @@ -512,16 +485,14 @@ class tag_typet:public typet } }; -/*! \brief Cast a generic typet to a \ref tag_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * tag_typet. - * - * \param type Source type - * \return Object of type \ref tag_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref tag_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// tag_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref tag_typet. inline const tag_typet &to_tag_type(const typet &type) { PRECONDITION(type.id()==ID_c_enum_tag || @@ -530,9 +501,7 @@ inline const tag_typet &to_tag_type(const typet &type) return static_cast(type); } -/*! \copydoc to_tag_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_tag_type(const typet &) inline tag_typet &to_tag_type(typet &type) { PRECONDITION(type.id()==ID_c_enum_tag || @@ -541,9 +510,7 @@ inline tag_typet &to_tag_type(typet &type) return static_cast(type); } -/*! \brief A struct tag type -*/ - +/// A struct tag type, i.e., \ref struct_typet with an identifier class struct_tag_typet:public tag_typet { public: @@ -553,34 +520,28 @@ class struct_tag_typet:public tag_typet } }; -/*! \brief Cast a generic typet to a \ref struct_tag_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * struct_tag_typet. - * - * \param type Source type - * \return Object of type \ref struct_tag_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref struct_tag_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// struct_tag_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref struct_tag_typet inline const struct_tag_typet &to_struct_tag_type(const typet &type) { PRECONDITION(type.id()==ID_struct_tag); return static_cast(type); } -/*! \copydoc to_struct_tag_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_struct_tag_type(const typet &) inline struct_tag_typet &to_struct_tag_type(typet &type) { PRECONDITION(type.id()==ID_struct_tag); return static_cast(type); } -/*! \brief A union tag type -*/ - +/// A union tag type, i.e., \ref union_typet with an identifier class union_tag_typet:public tag_typet { public: @@ -590,34 +551,29 @@ class union_tag_typet:public tag_typet } }; -/*! \brief Cast a generic typet to a \ref union_tag_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * union_tag_typet. - * - * \param type Source type - * \return Object of type \ref union_tag_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref union_tag_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// union_tag_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref union_tag_typet. inline const union_tag_typet &to_union_tag_type(const typet &type) { PRECONDITION(type.id()==ID_union_tag); return static_cast(type); } -/*! \copydoc to_union_tag_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_union_tag_type(const typet &) inline union_tag_typet &to_union_tag_type(typet &type) { PRECONDITION(type.id()==ID_union_tag); return static_cast(type); } -/*! \brief A generic enumeration type (not to be confused with C enums) -*/ - +/// An enumeration type, i.e., a type with elements (not to be confused with C +/// enums) class enumeration_typet:public typet { public: @@ -636,34 +592,28 @@ class enumeration_typet:public typet } }; -/*! \brief Cast a generic typet to a \ref enumeration_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * enumeration_typet. - * - * \param type Source type - * \return Object of type \ref enumeration_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref enumeration_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// enumeration_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref enumeration_typet. inline const enumeration_typet &to_enumeration_type(const typet &type) { PRECONDITION(type.id()==ID_enumeration); return static_cast(type); } -/*! \copydoc to_enumeration_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_enumeration_type(const typet &) inline enumeration_typet &to_enumeration_type(typet &type) { PRECONDITION(type.id()==ID_enumeration); return static_cast(type); } -/*! \brief The type of C enums -*/ - +/// The type of C enums class c_enum_typet:public type_with_subtypet { public: @@ -697,34 +647,28 @@ class c_enum_typet:public type_with_subtypet } }; -/*! \brief Cast a generic typet to a \ref c_enum_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * c_enum_typet. - * - * \param type Source type - * \return Object of type \ref c_enum_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref c_enum_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_enum_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref c_enum_typet. inline const c_enum_typet &to_c_enum_type(const typet &type) { PRECONDITION(type.id()==ID_c_enum); return static_cast(type); } -/*! \copydoc to_c_enum_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_c_enum_type(const typet &) inline c_enum_typet &to_c_enum_type(typet &type) { PRECONDITION(type.id()==ID_c_enum); return static_cast(type); } -/*! \brief An enum tag type -*/ - +/// C enum tag type, i.e., \ref c_enum_typet with an identifier class c_enum_tag_typet:public tag_typet { public: @@ -734,51 +678,46 @@ class c_enum_tag_typet:public tag_typet } }; -/*! \brief Cast a generic typet to a \ref c_enum_tag_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * c_enum_tag_typet. - * - * \param type Source type - * \return Object of type \ref c_enum_tag_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref c_enum_tag_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_enum_tag_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref c_enum_tag_typet. inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type) { PRECONDITION(type.id()==ID_c_enum_tag); return static_cast(type); } -/*! \copydoc to_enum_tag_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_c_enum_tag_type(const typet &) inline c_enum_tag_typet &to_c_enum_tag_type(typet &type) { PRECONDITION(type.id()==ID_c_enum_tag); return static_cast(type); } -/*! \brief Base type of functions -*/ +/// Base type of functions class code_typet:public typet { public: class parametert; typedef std::vector parameterst; - /// Constructs a new code type, i.e. function type - /// \param _parameters: the vector of function parameters - /// \param _return_type: the return type + /// Constructs a new code type, i.e., function type. + /// \param _parameters The vector of function parameters. + /// \param _return_type The return type. code_typet(parameterst &&_parameters, typet &&_return_type) : typet(ID_code) { parameters().swap(_parameters); return_type().swap(_return_type); } - /// Constructs a new code type, i.e. function type - /// \param _parameters: the vector of function parameters - /// \param _return_type: the return type + /// Constructs a new code type, i.e., function type. + /// \param _parameters The vector of function parameters. + /// \param _return_type The return type. code_typet(parameterst &&_parameters, const typet &_return_type) : typet(ID_code) { @@ -942,7 +881,7 @@ class code_typet:public typet set(ID_constructor, true); } - // this produces the list of parameter identifiers + /// Produces the list of parameter identifiers. std::vector parameter_identifiers() const { std::vector result; @@ -956,7 +895,7 @@ class code_typet:public typet typedef std::unordered_map parameter_indicest; - /// Get a map from parameter name to its index + /// Get a map from parameter name to its index. parameter_indicest parameter_indices() const { parameter_indicest parameter_indices; @@ -974,22 +913,23 @@ class code_typet:public typet } }; +/// Check whether a reference to a typet is a \ref code_typet. +/// \param type Source type. +/// \return True if \param type is a \ref code_typet. template <> inline bool can_cast_type(const typet &type) { return type.id() == ID_code; } -/*! \brief Cast a generic typet to a \ref code_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * code_typet. - * - * \param type Source type - * \return Object of type \ref code_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref code_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// code_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref code_typet. inline const code_typet &to_code_type(const typet &type) { PRECONDITION(can_cast_type(type)); @@ -997,9 +937,7 @@ inline const code_typet &to_code_type(const typet &type) return static_cast(type); } -/*! \copydoc to_code_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_code_type(const typet &) inline code_typet &to_code_type(typet &type) { PRECONDITION(can_cast_type(type)); @@ -1007,9 +945,9 @@ inline code_typet &to_code_type(typet &type) return static_cast(type); } - -/*! \brief arrays with given size -*/ +/// Arrays with given size +/// +/// Used for ordinary source-language arrays. class array_typet:public type_with_subtypet { public: @@ -1041,39 +979,37 @@ class array_typet:public type_with_subtypet } }; +/// Check whether a reference to a typet is a \ref array_typet. +/// \param type Source type. +/// \return True if \param type is a \ref array_typet. template <> inline bool can_cast_type(const typet &type) { return type.id() == ID_array; } -/*! \brief Cast a generic typet to an \ref array_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * array_typet. - * - * \param type Source type - * \return Object of type \ref array_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to an \ref array_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// array_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref array_typet. inline const array_typet &to_array_type(const typet &type) { PRECONDITION(can_cast_type(type)); return static_cast(type); } -/*! \copydoc to_array_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_array_type(const typet &) inline array_typet &to_array_type(typet &type) { PRECONDITION(can_cast_type(type)); return static_cast(type); } -/*! \brief arrays without size -*/ +/// Arrays without size class incomplete_array_typet:public type_with_subtypet { public: @@ -1087,33 +1023,32 @@ class incomplete_array_typet:public type_with_subtypet } }; -/*! \brief Cast a generic typet to an \ref incomplete_array_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * incomplete_array_typet. - * - * \param type Source type - * \return Object of type \ref incomplete_array_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to an \ref incomplete_array_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// incomplete_array_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref incomplete_array_typet. inline const incomplete_array_typet &to_incomplete_array_type(const typet &type) { PRECONDITION(type.id()==ID_array); return static_cast(type); } -/*! \copydoc to_incomplete_array_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_incomplete_array_type(const typet &) inline incomplete_array_typet &to_incomplete_array_type(typet &type) { PRECONDITION(type.id()==ID_array); return static_cast(type); } -/*! \brief Base class of bitvector types -*/ +/// Base class of fixed-width bit-vector types +/// +/// Superclass of anything represented by bits, for example integers (in 32 +/// or 64-bit representation), floating point numbers etc. In contrast, \ref +/// integer_typet is a direct integer representation. class bitvector_typet:public type_with_subtypet { public: @@ -1152,16 +1087,14 @@ class bitvector_typet:public type_with_subtypet } }; -/*! \brief Cast a generic typet to a \ref bitvector_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * bitvector_typet. - * - * \param type Source type - * \return Object of type \ref bitvector_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref bitvector_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// bitvector_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref bitvector_typet. inline const bitvector_typet &to_bitvector_type(const typet &type) { PRECONDITION(type.id()==ID_signedbv || @@ -1178,6 +1111,7 @@ inline const bitvector_typet &to_bitvector_type(const typet &type) return static_cast(type); } +/// \copydoc to_bitvector_type(const typet &type) inline bitvector_typet &to_bitvector_type(typet &type) { PRECONDITION(type.id()==ID_signedbv || @@ -1194,8 +1128,7 @@ inline bitvector_typet &to_bitvector_type(typet &type) return static_cast(type); } -/*! \brief fixed-width bit-vector without numerical interpretation -*/ +/// Fixed-width bit-vector without numerical interpretation class bv_typet:public bitvector_typet { public: @@ -1205,33 +1138,28 @@ class bv_typet:public bitvector_typet } }; -/*! \brief Cast a generic typet to a \ref bv_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * bv_typet. - * - * \param type Source type - * \return Object of type \ref bv_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref bv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// bv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref bv_typet. inline const bv_typet &to_bv_type(const typet &type) { PRECONDITION(type.id()==ID_bv); return static_cast(type); } -/*! \copydoc to_bv_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_bv_type(const typet &) inline bv_typet &to_bv_type(typet &type) { PRECONDITION(type.id()==ID_bv); return static_cast(type); } -/*! \brief Fixed-width bit-vector with unsigned binary interpretation -*/ +/// Fixed-width bit-vector with unsigned binary interpretation class unsignedbv_typet:public bitvector_typet { public: @@ -1247,33 +1175,28 @@ class unsignedbv_typet:public bitvector_typet constant_exprt largest_expr() const; }; -/*! \brief Cast a generic typet to an \ref unsignedbv_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * unsignedbv_typet. - * - * \param type Source type - * \return Object of type \ref unsignedbv_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to an \ref unsignedbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// unsignedbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref unsignedbv_typet. inline const unsignedbv_typet &to_unsignedbv_type(const typet &type) { PRECONDITION(type.id()==ID_unsignedbv); return static_cast(type); } -/*! \copydoc to_unsignedbv_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_unsignedbv_type(const typet &) inline unsignedbv_typet &to_unsignedbv_type(typet &type) { PRECONDITION(type.id()==ID_unsignedbv); return static_cast(type); } -/*! \brief Fixed-width bit-vector with two's complement interpretation -*/ +/// Fixed-width bit-vector with two's complement interpretation class signedbv_typet:public bitvector_typet { public: @@ -1289,33 +1212,31 @@ class signedbv_typet:public bitvector_typet constant_exprt largest_expr() const; }; -/*! \brief Cast a generic typet to a \ref signedbv_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * signedbv_typet. - * - * \param type Source type - * \return Object of type \ref signedbv_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref signedbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// signedbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref signedbv_typet. inline const signedbv_typet &to_signedbv_type(const typet &type) { PRECONDITION(type.id()==ID_signedbv); return static_cast(type); } -/*! \copydoc to_signedbv_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_signedbv_type(const typet &) inline signedbv_typet &to_signedbv_type(typet &type) { PRECONDITION(type.id()==ID_signedbv); return static_cast(type); } -/*! \brief Fixed-width bit-vector with signed fixed-point interpretation -*/ +/// Fixed-width bit-vector with signed fixed-point interpretation +/// +/// Integer and fraction bits refer to the number of bits before and after +/// the decimal point, respectively. The width is the sum of the two. class fixedbv_typet:public bitvector_typet { public: @@ -1336,24 +1257,21 @@ class fixedbv_typet:public bitvector_typet } }; -/*! \brief Cast a generic typet to a \ref fixedbv_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * fixedbv_typet. - * - * \param type Source type - * \return Object of type \ref fixedbv_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref fixedbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// fixedbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref fixedbv_typet. inline const fixedbv_typet &to_fixedbv_type(const typet &type) { PRECONDITION(type.id()==ID_fixedbv); return static_cast(type); } -/*! \brief Fixed-width bit-vector with IEEE floating-point interpretation -*/ +/// Fixed-width bit-vector with IEEE floating-point interpretation class floatbv_typet:public bitvector_typet { public: @@ -1375,24 +1293,21 @@ class floatbv_typet:public bitvector_typet } }; -/*! \brief Cast a generic typet to a \ref floatbv_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * floatbv_typet. - * - * \param type Source type - * \return Object of type \ref floatbv_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref floatbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// floatbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref floatbv_typet. inline const floatbv_typet &to_floatbv_type(const typet &type) { PRECONDITION(type.id()==ID_floatbv); return static_cast(type); } -/*! \brief Type for c bit fields -*/ +/// Type for C bit fields class c_bit_field_typet:public bitvector_typet { public: @@ -1404,40 +1319,28 @@ class c_bit_field_typet:public bitvector_typet // These have a sub-type }; -/*! \brief Cast a generic typet to a \ref c_bit_field_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * c_bit_field_typet. - * - * \param type Source type - * \return Object of type \ref c_bit_field_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref c_bit_field_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_bit_field_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref c_bit_field_typet. inline const c_bit_field_typet &to_c_bit_field_type(const typet &type) { PRECONDITION(type.id()==ID_c_bit_field); return static_cast(type); } -/*! \brief Cast a generic typet to a \ref c_bit_field_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * c_bit_field_typet. - * - * \param type Source type - * \return Object of type \ref c_bit_field_typet - * - * \ingroup gr_std_types -*/ +/// \copydoc to_c_bit_field_type(const typet &type) inline c_bit_field_typet &to_c_bit_field_type(typet &type) { PRECONDITION(type.id()==ID_c_bit_field); return static_cast(type); } -/*! \brief The pointer type -*/ +/// The pointer type class pointer_typet:public bitvector_typet { public: @@ -1452,16 +1355,14 @@ class pointer_typet:public bitvector_typet } }; -/*! \brief Cast a generic typet to a \ref pointer_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * pointer_typet. - * - * \param type Source type - * \return Object of type \ref pointer_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref pointer_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// pointer_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref pointer_typet. inline const pointer_typet &to_pointer_type(const typet &type) { PRECONDITION(type.id()==ID_pointer); @@ -1470,9 +1371,7 @@ inline const pointer_typet &to_pointer_type(const typet &type) return ret; } -/*! \copydoc to_pointer_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_pointer_type(const typet &) inline pointer_typet &to_pointer_type(typet &type) { PRECONDITION(type.id()==ID_pointer); @@ -1481,6 +1380,9 @@ inline pointer_typet &to_pointer_type(typet &type) return ret; } +/// Check whether a reference to a typet is a \ref pointer_typet. +/// \param type Source type. +/// \return True if \param type is a \ref pointer_typet. template <> inline bool can_cast_type(const typet &type) { @@ -1493,8 +1395,10 @@ inline void validate_type(const pointer_typet &type) DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width"); } -/*! \brief The reference type -*/ +/// The reference type +/// +/// Intends to model C++ reference. Comparing to \ref pointer_typet should +/// never be null. class reference_typet:public pointer_typet { public: @@ -1505,16 +1409,14 @@ class reference_typet:public pointer_typet } }; -/*! \brief Cast a generic typet to a \ref reference_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * reference_typet. - * - * \param type Source type - * \return Object of type \ref reference_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref reference_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// reference_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref reference_typet. inline const reference_typet &to_reference_type(const typet &type) { PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference)); @@ -1522,9 +1424,7 @@ inline const reference_typet &to_reference_type(const typet &type) return static_cast(type); } -/*! \copydoc to_reference_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_reference_type(const typet &) inline reference_typet &to_reference_type(typet &type) { PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference)); @@ -1532,15 +1432,11 @@ inline reference_typet &to_reference_type(typet &type) return static_cast(type); } -/*! \brief TO_BE_DOCUMENTED -*/ bool is_reference(const typet &type); -/*! \brief TO_BE_DOCUMENTED -*/ + bool is_rvalue_reference(const typet &type); -/*! \brief The C/C++ Booleans -*/ +/// The C/C++ Booleans class c_bool_typet:public bitvector_typet { public: @@ -1554,33 +1450,30 @@ class c_bool_typet:public bitvector_typet } }; -/*! \brief Cast a generic typet to a \ref c_bool_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * c_bool_typet. - * - * \param type Source type - * \return Object of type \ref c_bool_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref c_bool_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// c_bool_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref c_bool_typet. inline const c_bool_typet &to_c_bool_type(const typet &type) { PRECONDITION(type.id()==ID_c_bool); return static_cast(type); } -/*! \copydoc to_c_bool_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_c_bool_type(const typet &) inline c_bool_typet &to_c_bool_type(typet &type) { PRECONDITION(type.id()==ID_c_bool); return static_cast(type); } -/*! \brief TO_BE_DOCUMENTED -*/ +/// String type +/// +/// Represents string constants, such as `@class_identifier`. class string_typet:public typet { public: @@ -1589,24 +1482,21 @@ class string_typet:public typet } }; -/*! \brief Cast a generic typet to a \ref string_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * string_typet. - * - * \param type Source type - * \return Object of type \ref string_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref string_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// string_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref string_typet. inline const string_typet &to_string_type(const typet &type) { PRECONDITION(type.id()==ID_string); return static_cast(type); } -/*! \brief A type for subranges of integers -*/ +/// A type for subranges of integers class range_typet:public typet { public: @@ -1623,24 +1513,28 @@ class range_typet:public typet void set_to(const mp_integer &to); }; -/*! \brief Cast a generic typet to a \ref range_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * range_typet. - * - * \param type Source type - * \return Object of type \ref range_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref range_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// range_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref range_typet. inline const range_typet &to_range_type(const typet &type) { PRECONDITION(type.id()==ID_range); return static_cast(type); } -/*! \brief A constant-size array type -*/ +/// The vector type +/// +/// Used to represent the short vectors used by CPU instruction sets such as +/// MMX, SSE and AVX. They all provide registers that are something like +/// 8 x int32, for example, and corresponding operations that operate +/// element-wise on their operand vectors. Compared to \ref array_typet +/// that has no element-wise operators. Note that `remove_vector.h` removes +/// this data type by compilation into arrays. class vector_typet:public type_with_subtypet { public: @@ -1662,33 +1556,28 @@ class vector_typet:public type_with_subtypet } }; -/*! \brief Cast a generic typet to a \ref vector_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * vector_typet. - * - * \param type Source type - * \return Object of type \ref vector_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref vector_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// vector_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref vector_typet. inline const vector_typet &to_vector_type(const typet &type) { PRECONDITION(type.id()==ID_vector); return static_cast(type); } -/*! \copydoc to_vector_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_vector_type(const typet &) inline vector_typet &to_vector_type(typet &type) { PRECONDITION(type.id()==ID_vector); return static_cast(type); } -/*! \brief Complex numbers made of pair of given subtype -*/ +/// Complex numbers made of pair of given subtype class complex_typet:public type_with_subtypet { public: @@ -1702,34 +1591,29 @@ class complex_typet:public type_with_subtypet } }; -/*! \brief Cast a generic typet to a \ref complex_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * complex_typet. - * - * \param type Source type - * \return Object of type \ref complex_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref complex_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// complex_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref complex_typet. inline const complex_typet &to_complex_type(const typet &type) { PRECONDITION(type.id()==ID_complex); return static_cast(type); } -/*! \copydoc to_complex_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_complex_type(const typet &) inline complex_typet &to_complex_type(typet &type) { PRECONDITION(type.id()==ID_complex); return static_cast(type); } -/*! \brief A type for mathematical functions (do not - confuse with functions/methods in code) -*/ +/// A type for mathematical functions (do not confuse with functions/methods +/// in code) class mathematical_function_typet:public typet { public: @@ -1787,29 +1671,28 @@ class mathematical_function_typet:public typet return d.back(); } - // The codomain is the set of values that the - // function maps to (the "target") + /// Return the codomain, i.e., the set of values that the function maps to + /// (the "target"). typet &codomain() { return subtypes()[1]; } + /// \copydoc codomain() const typet &codomain() const { return subtypes()[1]; } }; -/*! \brief Cast a generic typet to a \ref mathematical_function_typet - * - * This is an unchecked conversion. \a type must be known to be \ref - * mathematical_function_typet. - * - * \param type Source type - * \return Object of type \ref mathematical_function_typet - * - * \ingroup gr_std_types -*/ +/// \brief Cast a typet to a \ref mathematical_function_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// mathematical_function_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref mathematical_function_typet. inline const mathematical_function_typet & to_mathematical_function_type(const typet &type) { @@ -1817,9 +1700,7 @@ inline const mathematical_function_typet & return static_cast(type); } -/*! \copydoc to_mathematical_function_type(const typet &) - * \ingroup gr_std_types -*/ +/// \copydoc to_mathematical_function_type(const typet &) inline mathematical_function_typet & to_mathematical_function_type(typet &type) {