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 "format_expr.h"
11 #include "std_types.h"
12 
13 #include <ostream>
14 
16 static std::ostream &format_rec(std::ostream &os, const struct_typet &src)
17 {
18  os << "struct"
19  << " {";
20  bool first = true;
21 
22  for(const auto &c : src.components())
23  {
24  if(first)
25  first = false;
26  else
27  os << ',';
28 
29  os << ' ' << format(c.type()) << ' ' << c.get_name();
30  }
31 
32  return os << " }";
33 }
34 
36 static std::ostream &format_rec(std::ostream &os, const union_typet &src)
37 {
38  os << "union"
39  << " {";
40  bool first = true;
41 
42  for(const auto &c : src.components())
43  {
44  if(first)
45  first = false;
46  else
47  os << ',';
48 
49  os << ' ' << format(c.type()) << ' ' << c.get_name();
50  }
51 
52  return os << " }";
53 }
54 
55 // The below generates a string in a generic syntax
56 // that is inspired by C/C++/Java, and is meant for debugging
57 // purposes.
58 std::ostream &format_rec(std::ostream &os, const typet &type)
59 {
60  const auto &id = type.id();
61 
62  if(id == ID_pointer)
63  return os << format(to_pointer_type(type).subtype()) << '*';
64  else if(id == ID_array)
65  {
66  const auto &t = to_array_type(type);
67  if(t.is_complete())
68  return os << format(t.subtype()) << '[' << format(t.size()) << ']';
69  else
70  return os << format(t.subtype()) << "[]";
71  }
72  else if(id == ID_struct)
73  return format_rec(os, to_struct_type(type));
74  else if(id == ID_union)
75  return format_rec(os, to_union_type(type));
76  else if(id == ID_union_tag)
77  return os << "union " << to_union_tag_type(type).get_identifier();
78  else if(id == ID_struct_tag)
79  return os << "struct " << to_struct_tag_type(type).get_identifier();
80  else if(id == ID_c_enum_tag)
81  return os << "c_enum " << to_c_enum_tag_type(type).get_identifier();
82  else if(id == ID_signedbv)
83  return os << "signedbv[" << to_signedbv_type(type).get_width() << ']';
84  else if(id == ID_unsignedbv)
85  return os << "unsignedbv[" << to_unsignedbv_type(type).get_width() << ']';
86  else if(id == ID_floatbv)
87  return os << "floatbv[" << to_floatbv_type(type).get_width() << ']';
88  else if(id == ID_c_bool)
89  return os << "c_bool[" << to_c_bool_type(type).get_width() << ']';
90  else if(id == ID_bool)
91  return os << "\xf0\x9d\x94\xb9"; // u+1D539, 'B'
92  else if(id == ID_integer)
93  return os << "\xe2\x84\xa4"; // u+2124, 'Z'
94  else if(id == ID_natural)
95  return os << "\xe2\x84\x95"; // u+2115, 'N'
96  else if(id == ID_rational)
97  return os << "\xe2\x84\x9a"; // u+211A, 'Q'
98  else
99  return os << id;
100 }
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: std_types.h:1636
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:555
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: std_types.h:721
format
static format_containert< T > format(const T &o)
Definition: format.h:35
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:29
format_rec
static std::ostream & format_rec(std::ostream &os, const struct_typet &src)
format a struct_typet
Definition: format_type.cpp:16
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
std_types.h
Pre-defined types.
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:515
union_typet
The union type.
Definition: std_types.h:393
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
format_expr.h
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
format_type.h