cprover
Loading...
Searching...
No Matches
cpp_typecheck_enum_type.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "cpp_typecheck.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/config.h>
17
18#include <ansi-c/c_qualifiers.h>
19
20#include "cpp_enum_type.h"
21
23{
24 c_enum_typet &c_enum_type=to_c_enum_type(enum_symbol.type);
25
26 exprt &body=static_cast<exprt &>(c_enum_type.add(ID_body));
27 irept::subt &components=body.get_sub();
28
29 c_enum_tag_typet enum_tag_type(enum_symbol.name);
30
31 mp_integer i=0;
32
33 for(auto &component : components)
34 {
35 const irep_idt &name = component.get(ID_name);
36
37 if(component.find(ID_value).is_not_nil())
38 {
39 exprt &value = static_cast<exprt &>(component.add(ID_value));
40 typecheck_expr(value);
41 implicit_typecast(value, c_enum_type.underlying_type());
42 make_constant(value);
43 if(to_integer(to_constant_expr(value), i))
44 {
46 error() << "failed to produce integer for enum constant" << eom;
47 throw 0;
48 }
49 }
50
51 exprt value_expr = from_integer(i, c_enum_type.underlying_type());
52 value_expr.type()=enum_tag_type; // override type
53
54 symbolt symbol;
55
56 symbol.name=id2string(enum_symbol.name)+"::"+id2string(name);
57 symbol.base_name=name;
58 symbol.value=value_expr;
59 symbol.location = static_cast<const source_locationt &>(
60 component.find(ID_C_source_location));
61 symbol.mode = enum_symbol.mode;
62 symbol.module=module;
63 symbol.type=enum_tag_type;
64 symbol.is_type=false;
65 symbol.is_macro=true;
66 symbol.is_file_local = true;
67 symbol.is_thread_local = true;
68
69 symbolt *new_symbol;
70 if(symbol_table.move(symbol, new_symbol))
71 {
73 error() << "cpp_typecheckt::typecheck_enum_body: "
74 << "symbol_table.move() failed" << eom;
75 throw 0;
76 }
77
78 cpp_idt &scope_identifier=
79 cpp_scopes.put_into_scope(*new_symbol);
80
81 scope_identifier.id_class=cpp_idt::id_classt::SYMBOL;
82
83 ++i;
84 }
85}
86
88{
89 // first save qualifiers
90 c_qualifierst qualifiers;
91 qualifiers.read(type);
92
93 cpp_enum_typet &enum_type=to_cpp_enum_type(type);
94 bool anonymous=!enum_type.has_tag();
95 irep_idt base_name;
96
97 cpp_save_scopet save_scope(cpp_scopes);
98
99 if(anonymous)
100 {
101 // we fabricate a tag based on the enum constants contained
102 base_name=enum_type.generate_anon_tag();
103 }
104 else
105 {
106 const cpp_namet &tag=enum_type.tag();
107
108 cpp_template_args_non_tct template_args;
109 template_args.make_nil();
110
111 cpp_typecheck_resolvet resolver(*this);
112 resolver.resolve_scope(tag, base_name, template_args);
113 }
114
115 bool has_body=enum_type.has_body();
116 bool tag_only_declaration=enum_type.get_tag_only_declaration();
117
118 cpp_scopet &dest_scope=
119 tag_scope(base_name, has_body, tag_only_declaration);
120
121 const irep_idt symbol_name=
122 dest_scope.prefix+"tag-"+id2string(base_name);
123
124 // check if we have it
125
126 symbol_tablet::symbolst::const_iterator previous_symbol=
127 symbol_table.symbols.find(symbol_name);
128
129 if(previous_symbol!=symbol_table.symbols.end())
130 {
131 // we do!
132
133 const symbolt &symbol=previous_symbol->second;
134
135 if(has_body)
136 {
138 error() << "error: enum symbol '" << base_name
139 << "' declared previously\n"
140 << "location of previous definition: " << symbol.location << eom;
141 throw 0;
142 }
143 }
144 else if(
145 has_body ||
147 {
148 std::string pretty_name=
150
151 // C++11 enumerations have an underlying type,
152 // which defaults to int.
153 // enums without underlying type may be 'packed'.
154 if(type.subtype().is_nil())
155 type.subtype()=signed_int_type();
156 else
157 {
158 typecheck_type(type.subtype());
159 if(
160 type.subtype().id() != ID_signedbv &&
161 type.subtype().id() != ID_unsignedbv &&
162 type.subtype().id() != ID_c_bool)
163 {
165 error() << "underlying type must be integral" << eom;
166 throw 0;
167 }
168 }
169
170 symbolt symbol;
171
172 symbol.name=symbol_name;
173 symbol.base_name=base_name;
174 symbol.value.make_nil();
175 symbol.location=type.source_location();
176 symbol.mode=ID_cpp;
177 symbol.module=module;
178 symbol.type.swap(type);
179 symbol.is_type=true;
180 symbol.is_macro=false;
181 symbol.pretty_name=pretty_name;
182
183 // move early, must be visible before doing body
184 symbolt *new_symbol;
185 if(symbol_table.move(symbol, new_symbol))
186 {
188 error() << "cpp_typecheckt::typecheck_enum_type: "
189 << "symbol_table.move() failed" << eom;
190 throw 0;
191 }
192
193 // put into scope
194 cpp_idt &scope_identifier=
195 cpp_scopes.put_into_scope(*new_symbol, dest_scope);
196
197 scope_identifier.id_class=cpp_idt::id_classt::CLASS;
198 scope_identifier.is_scope = true;
199
200 cpp_save_scopet save_scope_before_enum_typecheck(cpp_scopes);
201
202 if(new_symbol->type.get_bool(ID_C_class))
203 cpp_scopes.go_to(scope_identifier);
204
205 if(has_body)
206 typecheck_enum_body(*new_symbol);
207 }
208 else
209 {
211 error() << "use of enum '" << base_name << "' without previous declaration"
212 << eom;
213 throw 0;
214 }
215
216 // create enum tag expression, and add the qualifiers
217 type=c_enum_tag_typet(symbol_name);
218 qualifiers.write(type);
219}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
The type of C enums.
Definition: c_types.h:217
const typet & underlying_type() const
Definition: c_types.h:274
virtual void write(typet &src) const override
virtual void read(const typet &src) override
virtual void make_constant(exprt &expr)
symbol_tablet & symbol_table
const irep_idt module
struct configt::ansi_ct ansi_c
bool has_body() const
Definition: cpp_enum_type.h:49
const cpp_namet & tag() const
Definition: cpp_enum_type.h:24
bool has_tag() const
Definition: cpp_enum_type.h:29
irep_idt generate_anon_tag() const
bool get_tag_only_declaration() const
Definition: cpp_enum_type.h:54
Definition: cpp_id.h:23
std::string prefix
Definition: cpp_id.h:79
bool is_scope
Definition: cpp_id.h:43
id_classt id_class
Definition: cpp_id.h:45
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
void typecheck_type(typet &) override
void typecheck_enum_type(typet &type)
void implicit_typecast(exprt &expr, const typet &type) override
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
void typecheck_expr(exprt &) override
void typecheck_enum_body(symbolt &symbol)
cpp_scopest cpp_scopes
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
subt & get_sub()
Definition: irep.h:456
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_macro
Definition: symbol.h:61
bool is_file_local
Definition: symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_thread_local
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const source_locationt & source_location() const
Definition: type.h:74
configt config
Definition: config.cpp:25
C++ Language Type Checking.
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition: cpp_enum_type.h:62
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
BigInt mp_integer
Definition: smt_terms.h:12
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
flavourt mode
Definition: config.h:222