cprover
cpp_typecheck_declaration.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \********************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
15 
17 {
18  // see if the declaration is empty
19  if(declaration.is_empty())
20  return;
21 
22  // The function bodies must not be checked here,
23  // but only at the very end when all declarations have been
24  // processed (or considering forward declarations at least)
25 
26  // templates are done in a dedicated function
27  if(declaration.is_template())
28  convert_template_declaration(declaration);
29  else
31 }
32 
34 {
35  codet new_code(ID_decl_block);
36  new_code.reserve_operands(declaration.declarators().size());
37 
38  // unnamed object
39  std::string identifier="#anon_union"+std::to_string(anon_counter++);
40 
41  const cpp_namet cpp_name(identifier, declaration.source_location());
42  cpp_declaratort declarator;
43  declarator.name()=cpp_name;
44 
45  cpp_declarator_convertert cpp_declarator_converter(*this);
46 
47  const symbolt &symbol=
48  cpp_declarator_converter.convert(declaration, declarator);
49 
50  if(!cpp_is_pod(declaration.type()))
51  {
52  error().source_location=follow(declaration.type()).source_location();
53  error() << "anonymous union is not POD" << eom;
54  throw 0;
55  }
56 
57  new_code.add_to_operands(code_declt(cpp_symbol_expr(symbol)));
58 
59  // do scoping
60  symbolt union_symbol =
61  symbol_table.get_writeable_ref(follow(symbol.type).get(ID_name));
62 
63  for(const auto &c : to_union_type(union_symbol.type).components())
64  {
65  if(c.type().id() == ID_code)
66  {
67  error().source_location=union_symbol.type.source_location();
68  error() << "anonymous union '" << union_symbol.base_name
69  << "' shall not have function members" << eom;
70  throw 0;
71  }
72 
73  const irep_idt &base_name = c.get_base_name();
74 
75  if(cpp_scopes.current_scope().contains(base_name))
76  {
77  error().source_location=union_symbol.type.source_location();
78  error() << "identifier '" << base_name << "' already in scope" << eom;
79  throw 0;
80  }
81 
82  cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
84  id.identifier = c.get_name();
85  id.class_identifier=union_symbol.name;
86  id.is_member=true;
87  }
88 
89  symbol_table.get_writeable_ref(union_symbol.name)
90  .type.set(ID_C_unnamed_object, symbol.base_name);
91 
92  return new_code;
93 }
94 
96  cpp_declarationt &declaration)
97 {
98  assert(!declaration.is_template());
99 
100  // we first check if this is a typedef
101  typet &declaration_type=declaration.type();
102  bool is_typedef=declaration.is_typedef();
103 
104  // the name anonymous tag types
105  declaration.name_anon_struct_union();
106 
107  // do the type of the declaration
108  if(declaration.declarators().empty() || !has_auto(declaration_type))
109  typecheck_type(declaration_type);
110 
111  // Elaborate any class template instance _unless_ we do a typedef.
112  // These are only elaborated on usage!
113  if(!is_typedef)
114  elaborate_class_template(declaration_type);
115 
116  // mark as 'already typechecked'
117  if(!declaration.declarators().empty())
119 
120  // Special treatment for anonymous unions
121  if(declaration.declarators().empty() &&
122  follow(declaration.type()).get_bool(ID_C_is_anonymous))
123  {
124  typet final_type=follow(declaration.type());
125 
126  if(final_type.id()!=ID_union)
127  {
128  error().source_location=final_type.source_location();
129  error() << "top-level declaration does not declare anything"
130  << eom;
131  throw 0;
132  }
133 
134  convert_anonymous_union(declaration);
135  }
136 
137  // do the declarators (optional)
138  for(auto &d : declaration.declarators())
139  {
140  // copy the declarator (we destroy the original)
141  cpp_declaratort declarator=d;
142 
143  cpp_declarator_convertert cpp_declarator_converter(*this);
144 
145  cpp_declarator_converter.is_typedef=is_typedef;
146 
147  symbolt &symbol=cpp_declarator_converter.convert(
148  declaration_type, declaration.storage_spec(),
149  declaration.member_spec(), declarator);
150 
151  // any template instance to remember?
152  if(declaration.find(ID_C_template).is_not_nil())
153  {
154  symbol.type.set(ID_C_template, declaration.find(ID_C_template));
155  symbol.type.set(
156  ID_C_template_arguments,
157  declaration.find(ID_C_template_arguments));
158  }
159 
160  // replace declarator by symbol expression
161  exprt tmp=cpp_symbol_expr(symbol);
162  d.swap(tmp);
163 
164  // is there a constructor to be called for the declarator?
165  if(symbol.is_lvalue &&
166  declarator.init_args().has_operands())
167  {
168  auto constructor = cpp_constructor(
169  symbol.location,
170  cpp_symbol_expr(symbol),
171  declarator.init_args().operands());
172 
173  if(constructor.has_value())
174  symbol.value = constructor.value();
175  else
176  symbol.value = nil_exprt();
177  }
178  }
179 }
cpp_typecheckt::convert
void convert(cpp_linkage_spect &)
Definition: cpp_typecheck_linkage_spec.cpp:14
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cpp_typecheckt::convert_non_template_declaration
void convert_non_template_declaration(cpp_declarationt &declaration)
Definition: cpp_typecheck_declaration.cpp:95
cpp_declarationt::storage_spec
const cpp_storage_spect & storage_spec() const
Definition: cpp_declaration.h:74
cpp_declarationt::is_typedef
bool is_typedef() const
Definition: cpp_declaration.h:135
cpp_typecheckt::elaborate_class_template
void elaborate_class_template(const typet &type)
elaborate class template instances
Definition: cpp_instantiate_template.cpp:224
cpp_typecheckt::anon_counter
unsigned anon_counter
Definition: cpp_typecheck.h:226
cpp_declarationt::is_empty
bool is_empty() const
Definition: cpp_declaration.h:32
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
cpp_declaratort::name
cpp_namet & name()
Definition: cpp_declarator.h:36
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
cpp_declarator_convertert::convert
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
Definition: cpp_declarator_converter.cpp:34
exprt
Base class for all expressions.
Definition: expr.h:53
cpp_typecheckt::cpp_constructor
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
Definition: cpp_constructor.cpp:25
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
cpp_declarationt::name_anon_struct_union
void name_anon_struct_union()
Definition: cpp_declaration.h:144
cpp_scopet::contains
bool contains(const irep_idt &base_name_to_lookup)
Definition: cpp_scope.cpp:203
cpp_idt
Definition: cpp_id.h:29
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:64
cpp_declarationt::member_spec
const cpp_member_spect & member_spec() const
Definition: cpp_declaration.h:86
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
messaget::error
mstreamt & error() const
Definition: message.h:399
cpp_idt::id_classt::SYMBOL
@ SYMBOL
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
cpp_declarator_convertert
Definition: cpp_declarator_converter.h:26
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
cpp_declarator_convertert::is_typedef
bool is_typedef
Definition: cpp_declarator_converter.h:31
cpp_symbol_expr
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:67
cpp_declarationt
Definition: cpp_declaration.h:24
irept::id
const irep_idt & id() const
Definition: irep.h:418
cpp_declarationt::is_template
bool is_template() const
Definition: cpp_declaration.h:52
cpp_typecheckt::convert_template_declaration
void convert_template_declaration(cpp_declarationt &declaration)
Definition: cpp_typecheck_template.cpp:967
cpp_typecheck.h
C++ Language Type Checking.
cpp_declaratort::init_args
exprt & init_args()
Definition: cpp_declarator.h:59
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
cpp_typecheckt::has_auto
static bool has_auto(const typet &type)
Definition: cpp_typecheck_compound_type.cpp:64
cpp_idt::id_class
id_classt id_class
Definition: cpp_id.h:51
cpp_typecheckt::convert_anonymous_union
codet convert_anonymous_union(cpp_declarationt &declaration)
Definition: cpp_typecheck_declaration.cpp:33
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:157
already_typechecked_typet::make_already_typechecked
static void make_already_typechecked(typet &type)
Definition: c_typecheck_base.h:309
exprt::operands
operandst & operands()
Definition: expr.h:95
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:127
cpp_namet
Definition: cpp_name.h:17
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cpp_declaratort
Definition: cpp_declarator.h:20
cpp_scopet::insert
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
cpp_declarator_converter.h
C++ Language Type Checking.
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35