cprover
cpp_type2name.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Module
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_type2name.h"
13 
14 #include <string>
15 
16 #include <util/cprover_prefix.h>
17 #include <util/std_types.h>
18 #include <util/type.h>
19 
20 static std::string do_prefix(const std::string &s)
21 {
22  if(s.find(',')!=std::string::npos ||
23  (s!="" && isdigit(s[0])))
24  return std::to_string(s.size())+"_"+s;
25 
26  return s;
27 }
28 
29 static void irep2name(const irept &irep, std::string &result)
30 {
31  result="";
32 
33  if(is_reference(static_cast<const typet&>(irep)))
34  result+="reference";
35 
36  if(irep.id()!="")
37  result+=do_prefix(irep.id_string());
38 
39  if(irep.get_named_sub().empty() &&
40  irep.get_sub().empty() &&
41  irep.get_comments().empty())
42  return;
43 
44  result+='(';
45  bool first=true;
46 
48  {
49  if(first)
50  first=false;
51  else
52  result+=',';
53 
54  result+=do_prefix(name2string(it->first));
55 
56  result+='=';
57  std::string tmp;
58  irep2name(it->second, tmp);
59  result+=tmp;
60  }
61 
63  if(it->first==ID_C_constant ||
64  it->first==ID_C_volatile ||
65  it->first==ID_C_restricted)
66  {
67  if(first)
68  first=false;
69  else
70  result+=',';
71  result+=do_prefix(name2string(it->first));
72  result+='=';
73  std::string tmp;
74  irep2name(it->second, tmp);
75  result+=tmp;
76  }
77 
78  forall_irep(it, irep.get_sub())
79  {
80  if(first)
81  first=false;
82  else
83  result+=',';
84  std::string tmp;
85  irep2name(*it, tmp);
86  result+=tmp;
87  }
88 
89  result+=')';
90 }
91 
92 std::string cpp_type2name(const typet &type)
93 {
94  std::string result;
95 
96  if(type.get_bool(ID_C_constant))
97  result+="const_";
98 
99  if(type.get_bool(ID_C_restricted))
100  result+="restricted_";
101 
102  if(type.get_bool(ID_C_volatile))
103  result+="volatile_";
104 
105  if(type.id()==ID_empty || type.id()==ID_void)
106  result+="void";
107  else if(type.id() == ID_c_bool)
108  result+="bool";
109  else if(type.id() == ID_bool)
110  result += CPROVER_PREFIX "bool";
111  else if(type.id()==ID_pointer)
112  {
113  if(is_reference(type))
114  result+="ref_"+cpp_type2name(type.subtype());
115  else if(is_rvalue_reference(type))
116  result+="rref_"+cpp_type2name(type.subtype());
117  else
118  result+="ptr_"+cpp_type2name(type.subtype());
119  }
120  else if(type.id()==ID_signedbv || type.id()==ID_unsignedbv)
121  {
122  // we try to use #c_type
123  const irep_idt c_type=type.get(ID_C_c_type);
124 
125  if(!c_type.empty())
126  result+=id2string(c_type);
127  else if(type.id()==ID_unsignedbv)
128  result+="unsigned_int";
129  else
130  result+="signed_int";
131  }
132  else if(type.id()==ID_fixedbv || type.id()==ID_floatbv)
133  {
134  // we try to use #c_type
135  const irep_idt c_type=type.get(ID_C_c_type);
136 
137  if(!c_type.empty())
138  result+=id2string(c_type);
139  else
140  result+="double";
141  }
142  else if(type.id()==ID_code)
143  {
144  // we do (args)->(return_type)
145  const code_typet::parameterst &parameters=to_code_type(type).parameters();
146  const typet &return_type=to_code_type(type).return_type();
147 
148  result+='(';
149 
150  for(code_typet::parameterst::const_iterator
151  arg_it=parameters.begin();
152  arg_it!=parameters.end();
153  arg_it++)
154  {
155  if(arg_it!=parameters.begin())
156  result+=',';
157  result+=cpp_type2name(arg_it->type());
158  }
159 
160  result+=')';
161  result+="->(";
162  result+=cpp_type2name(return_type);
163  result+=')';
164  }
165  else
166  {
167  // give up
168  std::string tmp;
169  irep2name(type, tmp);
170  return tmp;
171  }
172 
173  return result;
174 }
175 
176 std::string cpp_expr2name(const exprt &expr)
177 {
178  std::string tmp;
179  irep2name(expr, tmp);
180  return tmp;
181 }
The type of an expression, extends irept.
Definition: type.h:27
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define CPROVER_PREFIX
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
std::vector< parametert > parameterst
Definition: std_types.h:754
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
#define forall_named_irep(it, irep)
Definition: irep.h:70
subt & get_sub()
Definition: irep.h:317
const irep_idt & id() const
Definition: irep.h:259
const std::string & name2string(const irep_namet &n)
Definition: irep.h:53
C++ Language Module.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
named_subt & get_comments()
Definition: irep.h:321
std::string cpp_type2name(const typet &type)
Base class for tree-like data structures with sharing.
Definition: irep.h:156
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
named_subt & get_named_sub()
Definition: irep.h:319
Pre-defined types.
Base class for all expressions.
Definition: expr.h:54
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:139
const parameterst & parameters() const
Definition: std_types.h:893
static void irep2name(const irept &irep, std::string &result)
const std::string & id_string() const
Definition: irep.h:262
static std::string do_prefix(const std::string &s)
std::string cpp_expr2name(const exprt &expr)
const typet & subtype() const
Definition: type.h:38
bool empty() const
Definition: dstring.h:75
const typet & return_type() const
Definition: std_types.h:883
Defines typet, type_with_subtypet and type_with_subtypest.
#define forall_irep(it, irep)
Definition: irep.h:62