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