cprover
format_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "format_type.h"
10 #include "c_types.h"
11 #include "format_expr.h"
12 #include "pointer_expr.h"
13 
14 #include <ostream>
15 
17 static std::ostream &format_rec(std::ostream &os, const struct_typet &src)
18 {
19  os << "struct"
20  << " {";
21  bool first = true;
22 
23  for(const auto &c : src.components())
24  {
25  if(first)
26  first = false;
27  else
28  os << ',';
29 
30  os << ' ' << format(c.type()) << ' ' << c.get_name();
31  }
32 
33  return os << " }";
34 }
35 
37 static std::ostream &format_rec(std::ostream &os, const union_typet &src)
38 {
39  os << "union"
40  << " {";
41  bool first = true;
42 
43  for(const auto &c : src.components())
44  {
45  if(first)
46  first = false;
47  else
48  os << ',';
49 
50  os << ' ' << format(c.type()) << ' ' << c.get_name();
51  }
52 
53  return os << " }";
54 }
55 
56 // The below generates a string in a generic syntax
57 // that is inspired by C/C++/Java, and is meant for debugging
58 // purposes.
59 std::ostream &format_rec(std::ostream &os, const typet &type)
60 {
61  const auto &id = type.id();
62 
63  if(id == ID_pointer)
64  return os << format(to_pointer_type(type).subtype()) << '*';
65  else if(id == ID_array)
66  {
67  const auto &t = to_array_type(type);
68  if(t.is_complete())
69  return os << format(t.subtype()) << '[' << format(t.size()) << ']';
70  else
71  return os << format(t.subtype()) << "[]";
72  }
73  else if(id == ID_struct)
74  return format_rec(os, to_struct_type(type));
75  else if(id == ID_union)
76  return format_rec(os, to_union_type(type));
77  else if(id == ID_union_tag)
78  return os << "union " << to_union_tag_type(type).get_identifier();
79  else if(id == ID_struct_tag)
80  return os << "struct " << to_struct_tag_type(type).get_identifier();
81  else if(id == ID_c_enum_tag)
82  return os << "c_enum " << to_c_enum_tag_type(type).get_identifier();
83  else if(id == ID_signedbv)
84  return os << "signedbv[" << to_signedbv_type(type).get_width() << ']';
85  else if(id == ID_unsignedbv)
86  return os << "unsignedbv[" << to_unsignedbv_type(type).get_width() << ']';
87  else if(id == ID_bv)
88  return os << "bv[" << to_bitvector_type(type).get_width() << ']';
89  else if(id == ID_floatbv)
90  return os << "floatbv[" << to_floatbv_type(type).get_width() << ']';
91  else if(id == ID_c_bool)
92  return os << "c_bool[" << to_c_bool_type(type).get_width() << ']';
93  else if(id == ID_bool)
94  return os << "\xf0\x9d\x94\xb9"; // u+1D539, 'B'
95  else if(id == ID_integer)
96  return os << "\xe2\x84\xa4"; // u+2124, 'Z'
97  else if(id == ID_natural)
98  return os << "\xe2\x84\x95"; // u+2115, 'N'
99  else if(id == ID_rational)
100  return os << "\xe2\x84\x9a"; // u+211A, 'Q'
101  else
102  return os << id;
103 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:404
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
format
static format_containert< T > format(const T &o)
Definition: format.h:37
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:93
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
typet
The type of an expression, extends irept.
Definition: type.h:28
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
format_rec
static std::ostream & format_rec(std::ostream &os, const struct_typet &src)
format a struct_typet
Definition: format_type.cpp:17
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
pointer_expr.h
API to expression classes for Pointers.
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
union_typet
The union type.
Definition: c_types.h:112
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
format_expr.h
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
c_types.h
format_type.h