cprover
cpp_typecheck_enum_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
14 #include <util/arith_tools.h>
15 
16 #include <ansi-c/c_qualifiers.h>
17 #include <util/c_types.h>
18 
19 #include "cpp_enum_type.h"
20 
22 {
23  c_enum_typet &c_enum_type=to_c_enum_type(enum_symbol.type);
24 
25  exprt &body=static_cast<exprt &>(c_enum_type.add(ID_body));
26  irept::subt &components=body.get_sub();
27 
28  c_enum_tag_typet enum_tag_type(enum_symbol.name);
29 
30  mp_integer i=0;
31 
32  Forall_irep(it, components)
33  {
34  const irep_idt &name=it->get(ID_name);
35 
36  if(it->find(ID_value).is_not_nil())
37  {
38  exprt &value=static_cast<exprt &>(it->add(ID_value));
39  typecheck_expr(value);
40  implicit_typecast(value, c_enum_type.subtype());
41  make_constant(value);
42  if(to_integer(value, i))
43  {
45  error() << "failed to produce integer for enum constant" << eom;
46  throw 0;
47  }
48  }
49 
50  exprt value_expr=from_integer(i, c_enum_type.subtype());
51  value_expr.type()=enum_tag_type; // override type
52 
53  symbolt symbol;
54 
55  symbol.name=id2string(enum_symbol.name)+"::"+id2string(name);
56  symbol.base_name=name;
57  symbol.value=value_expr;
58  symbol.location=
59  static_cast<const source_locationt &>(it->find(ID_C_source_location));
60  symbol.mode=ID_cpp;
61  symbol.module=module;
62  symbol.type=enum_tag_type;
63  symbol.is_type=false;
64  symbol.is_macro=true;
65 
66  symbolt *new_symbol;
67  if(symbol_table.move(symbol, new_symbol))
68  {
70  error() << "cpp_typecheckt::typecheck_enum_body: "
71  << "symbol_table.move() failed" << eom;
72  throw 0;
73  }
74 
75  cpp_idt &scope_identifier=
76  cpp_scopes.put_into_scope(*new_symbol);
77 
78  scope_identifier.id_class=cpp_idt::id_classt::SYMBOL;
79 
80  ++i;
81  }
82 }
83 
85 {
86  // first save qualifiers
87  c_qualifierst qualifiers;
88  qualifiers.read(type);
89 
90  cpp_enum_typet &enum_type=to_cpp_enum_type(type);
91  bool anonymous=!enum_type.has_tag();
92  irep_idt base_name;
93 
94  if(anonymous)
95  {
96  // we fabricate a tag based on the enum constants contained
97  base_name=enum_type.generate_anon_tag();
98  }
99  else
100  {
101  const cpp_namet &tag=enum_type.tag();
102 
103  if(tag.is_simple_name())
104  base_name=tag.get_base_name();
105  else
106  {
108  error() << "enum tag is expected to be a simple name" << eom;
109  throw 0;
110  }
111  }
112 
113  bool has_body=enum_type.has_body();
114  bool tag_only_declaration=enum_type.get_tag_only_declaration();
115 
116  cpp_scopet &dest_scope=
117  tag_scope(base_name, has_body, tag_only_declaration);
118 
119  const irep_idt symbol_name=
120  dest_scope.prefix+"tag-"+id2string(base_name);
121 
122  // check if we have it
123 
124  symbol_tablet::symbolst::iterator previous_symbol=
125  symbol_table.symbols.find(symbol_name);
126 
127  if(previous_symbol!=symbol_table.symbols.end())
128  {
129  // we do!
130 
131  symbolt &symbol=previous_symbol->second;
132 
133  if(has_body)
134  {
136  error() << "error: enum symbol `" << base_name
137  << "' declared previously\n"
138  << "location of previous definition: "
139  << symbol.location << eom;
140  throw 0;
141  }
142  }
143  else if(has_body)
144  {
145  std::string pretty_name=
147 
148  // C++11 enumerations have an underlying type,
149  // which defaults to int.
150  // enums without underlying type may be 'packed'.
151  if(type.subtype().is_nil())
152  type.subtype()=signed_int_type();
153  else
154  {
155  typecheck_type(type.subtype());
156  if(type.subtype().id()==ID_signedbv ||
157  type.subtype().id()==ID_unsignedbv)
158  {
159  }
160  else
161  {
163  error() << "underlying type must be integral" << eom;
164  throw 0;
165  }
166  }
167 
168  symbolt symbol;
169 
170  symbol.name=symbol_name;
171  symbol.base_name=base_name;
172  symbol.value.make_nil();
173  symbol.location=type.source_location();
174  symbol.mode=ID_cpp;
175  symbol.module=module;
176  symbol.type.swap(type);
177  symbol.is_type=true;
178  symbol.is_macro=false;
179  symbol.pretty_name=pretty_name;
180 
181  // move early, must be visible before doing body
182  symbolt *new_symbol;
183  if(symbol_table.move(symbol, new_symbol))
184  {
185  error().source_location=symbol.location;
186  error() << "cpp_typecheckt::typecheck_enum_type: "
187  << "symbol_table.move() failed" << eom;
188  throw 0;
189  }
190 
191  // put into scope
192  cpp_idt &scope_identifier=
193  cpp_scopes.put_into_scope(*new_symbol, dest_scope);
194 
195  scope_identifier.id_class=cpp_idt::id_classt::CLASS;
196 
197  typecheck_enum_body(*new_symbol);
198  }
199  else
200  {
202  error() << "use of enum `" << base_name
203  << "' without previous declaration" << eom;
204  throw 0;
205  }
206 
207  // create enum tag expression, and add the qualifiers
208  type=c_enum_tag_typet(symbol_name);
209  qualifiers.write(type);
210 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
BigInt mp_integer
Definition: mp_arith.h:19
void typecheck_type(typet &type)
irep_idt generate_anon_tag() const
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::vector< irept > subt
Definition: irep.h:91
virtual void make_constant(exprt &expr)
irep_idt mode
Language mode.
Definition: symbol.h:55
exprt value
Initial value of symbol.
Definition: symbol.h:40
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
bool has_body() const
Definition: cpp_enum_type.h:51
bool get_tag_only_declaration() const
Definition: cpp_enum_type.h:56
void typecheck_enum_body(symbolt &symbol)
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
bool is_simple_name() const
Definition: cpp_name.h:88
virtual void implicit_typecast(exprt &expr, const typet &type)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void typecheck_expr(exprt &expr)
subt & get_sub()
Definition: irep.h:245
const cpp_namet & tag() const
Definition: cpp_enum_type.h:26
symbol_tablet & symbol_table
void typecheck_enum_type(typet &type)
void read(const typet &src)
std::string prefix
Definition: cpp_id.h:80
const irep_idt & id() const
Definition: irep.h:189
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:680
symbolst symbols
Definition: symbol_table.h:57
bool has_tag() const
Definition: cpp_enum_type.h:31
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
void write(typet &src) const
id_classt id_class
Definition: cpp_id.h:51
C++ Language Type Checking.
C++ Language Type Checking.
#define Forall_irep(it, irep)
Definition: irep.h:66
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition: cpp_enum_type.h:64
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
const source_locationt & source_location() const
Definition: type.h:95
irep_idt get_base_name() const
Definition: cpp_name.cpp:17
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
Base class for all expressions.
Definition: expr.h:46
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const irep_idt module
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
Definition: cpp_id.h:28
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
bool is_type
Definition: symbol.h:66
const typet & subtype() const
Definition: type.h:31
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
The type of C enums.
Definition: std_types.h:637
An enum tag type.
Definition: std_types.h:698
bool is_macro
Definition: symbol.h:66
cpp_scopest cpp_scopes