CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
merged_type.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: A type that holds a combination of types
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_ANSI_C_MERGED_TYPE_H
10#define CPROVER_ANSI_C_MERGED_TYPE_H
11
12#include <util/type.h>
13
16{
17public:
21
23 {
24 return subtypes().back();
25 }
26};
27
29inline const merged_typet &to_merged_type(const typet &type)
30{
33 !static_cast<const type_with_subtypest &>(type).subtypes().empty(),
34 "merge_typet has at least one subtype");
35 return static_cast<const merged_typet &>(type);
36}
37
40{
43 !static_cast<const type_with_subtypest &>(type).subtypes().empty(),
44 "merge_typet has at least one subtype");
45 return static_cast<merged_typet &>(type);
46}
47
48#endif // CPROVER_ANSI_C_MERGED_TYPE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const irep_idt & id() const
Definition irep.h:388
holds a combination of types
Definition merged_type.h:16
typet & last_type()
Definition merged_type.h:22
Type with multiple subtypes.
Definition type.h:222
subtypest & subtypes()
Definition type.h:237
The type of an expression, extends irept.
Definition type.h:29
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
Definition merged_type.h:29
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Defines typet, type_with_subtypet and type_with_subtypest.