cprover
ansi_c_declaration.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "ansi_c_declaration.h"
13 
14 #include <ostream>
15 
16 #include <util/config.h>
17 #include <util/std_types.h>
18 #include <util/invariant.h>
19 
20 #include "merged_type.h"
21 
23 {
24  typet *p=static_cast<typet *>(&src);
25 
26  // walk down subtype until we hit typedef_type, symbol or "abstract"
27  while(true)
28  {
29  typet &t=*p;
30 
31  if(t.id() == ID_typedef_type || t.id() == ID_symbol)
32  {
33  set_base_name(t.get(ID_C_base_name));
35  t.make_nil();
36  break;
37  }
38  else if(t.id().empty() ||
39  t.is_nil())
40  {
42  }
43  else if(t.id()==ID_abstract)
44  {
45  t.make_nil();
46  break;
47  }
48  else if(t.id()==ID_merged_type)
49  {
50  // we always walk down the _last_ member of a merged type
51  auto &merged_type = to_merged_type(t);
52  p = &merged_type.last_type();
53  }
54  else
55  p=&t.subtype();
56  }
57 
58  type()=static_cast<const typet &>(src);
59  value().make_nil();
60 }
61 
62 void ansi_c_declarationt::output(std::ostream &out) const
63 {
64  out << "Flags:";
65  if(get_is_typedef())
66  out << " is_typedef";
68  out << " is_enum_constant";
69  if(get_is_static())
70  out << " is_static";
71  if(get_is_parameter())
72  out << " is_parameter";
73  if(get_is_global())
74  out << " is_global";
75  if(get_is_register())
76  out << " is_register";
78  out << " is_thread_local";
79  if(get_is_inline())
80  out << " is_inline";
81  if(get_is_extern())
82  out << " is_extern";
84  out << " is_static_assert";
85  out << "\n";
86 
87  out << "Type: " << type().pretty() << "\n";
88 
89  for(const auto &declarator : declarators())
90  out << "Declarator: " << declarator.pretty() << "\n";
91 }
92 
94  const ansi_c_declaratort &declarator) const
95 {
96  typet result=declarator.type();
97  typet *p=&result;
98 
99  // this gets types that are still raw parse trees
100  while(p->is_not_nil())
101  {
102  if(p->id()==ID_frontend_pointer || p->id()==ID_array ||
103  p->id()==ID_vector || p->id()==ID_c_bit_field ||
104  p->id()==ID_block_pointer || p->id()==ID_code)
105  p=&p->subtype();
106  else if(p->id()==ID_merged_type)
107  {
108  // we always go down on the right-most subtype
109  auto &merged_type = to_merged_type(*p);
110  p = &merged_type.last_type();
111  }
112  else
113  UNREACHABLE;
114  }
115 
116  *p=type();
117 
118  // retain typedef for dump-c
119  if(get_is_typedef())
120  result.set(ID_C_typedef, declarator.get_name());
121 
122  return result;
123 }
124 
126  const ansi_c_declaratort &declarator,
127  symbolt &symbol) const
128 {
129  symbol.clear();
130  symbol.value=declarator.value();
131  symbol.type=full_type(declarator);
132  symbol.name=declarator.get_name();
133  symbol.pretty_name=symbol.name;
135  symbol.is_type=get_is_typedef();
137  symbol.is_extern=get_is_extern();
140  symbol.is_weak=get_is_weak();
141 
142  // is it a function?
143  const typet &type = symbol.type.id() == ID_merged_type
144  ? to_merged_type(symbol.type).last_type()
145  : symbol.type;
146 
147  if(type.id() == ID_code && !symbol.is_type)
148  {
149  symbol.is_static_lifetime=false;
150  symbol.is_thread_local=false;
151 
152  symbol.is_file_local=get_is_static();
153 
154  if(get_is_inline())
155  to_code_type(symbol.type).set_inlined(true);
156 
157  if(
161  {
162  // GCC extern inline cleanup, to enable remove_internal_symbols
163  // do its full job
164  // https://gcc.gnu.org/ml/gcc/2006-11/msg00006.html
165  // __attribute__((__gnu_inline__))
166  if(get_is_inline())
167  {
168  if(get_is_static()) // C99 and above
169  symbol.is_extern=false;
170  else if(get_is_extern()) // traditional GCC
171  symbol.is_file_local=true;
172  }
173 
174  // GCC __attribute__((__used__)) - do not treat those as file-local
175  if(get_is_used())
176  symbol.is_file_local = false;
177  }
178  }
179  else // non-function
180  {
181  symbol.is_static_lifetime=
182  !symbol.is_macro &&
183  !symbol.is_type &&
184  (get_is_global() || get_is_static());
185 
186  symbol.is_thread_local=
187  (!symbol.is_static_lifetime && !get_is_extern()) ||
189 
190  symbol.is_file_local=
191  symbol.is_macro ||
192  (!get_is_global() && !get_is_extern()) ||
193  (get_is_global() && get_is_static() && !get_is_used()) ||
194  symbol.is_parameter;
195  }
196 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
typet::subtype
const typet & subtype() const
Definition: type.h:47
ansi_c_declarationt::get_is_thread_local
bool get_is_thread_local() const
Definition: ansi_c_declaration.h:147
ansi_c_declaration.h
ANSI-CC Language Type Checking.
ansi_c_declarationt::declarators
const declaratorst & declarators() const
Definition: ansi_c_declaration.h:215
ansi_c_declarationt::get_is_typedef
bool get_is_typedef() const
Definition: ansi_c_declaration.h:77
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
ansi_c_declarationt::get_is_used
bool get_is_used() const
Definition: ansi_c_declaration.h:197
ansi_c_declaratort::value
exprt & value()
Definition: ansi_c_declaration.h:25
irept::make_nil
void make_nil()
Definition: irep.h:465
typet
The type of an expression, extends irept.
Definition: type.h:28
ansi_c_declarationt::get_is_static
bool get_is_static() const
Definition: ansi_c_declaration.h:97
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
ansi_c_declarationt::get_is_weak
bool get_is_weak() const
Definition: ansi_c_declaration.h:187
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
merged_type.h
invariant.h
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
configt::ansi_c
struct configt::ansi_ct ansi_c
ansi_c_declarationt::declarator
const ansi_c_declaratort & declarator() const
Definition: ansi_c_declaration.h:226
configt::ansi_ct::flavourt::ARM
@ ARM
ansi_c_declarationt::get_is_static_assert
bool get_is_static_assert() const
Definition: ansi_c_declaration.h:177
configt::ansi_ct::flavourt::CLANG
@ CLANG
ansi_c_declaratort::set_base_name
void set_base_name(const irep_idt &base_name)
Definition: ansi_c_declaration.h:50
ansi_c_declaratort::get_name
irep_idt get_name() const
Definition: ansi_c_declaration.h:40
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
ansi_c_declaratort::build
void build(irept &src)
Definition: ansi_c_declaration.cpp:22
to_merged_type
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
Definition: merged_type.h:29
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
ansi_c_declarationt::get_is_parameter
bool get_is_parameter() const
Definition: ansi_c_declaration.h:107
ansi_c_declaratort
Definition: ansi_c_declaration.h:19
ansi_c_declaratort::get_base_name
irep_idt get_base_name() const
Definition: ansi_c_declaration.h:45
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
std_types.h
Pre-defined types.
code_typet::set_inlined
void set_inlined(bool value)
Definition: std_types.h:664
ansi_c_declarationt::to_symbol
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
Definition: ansi_c_declaration.cpp:125
ansi_c_declarationt::get_is_register
bool get_is_register() const
Definition: ansi_c_declaration.h:137
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
ansi_c_declarationt::get_is_enum_constant
bool get_is_enum_constant() const
Definition: ansi_c_declaration.h:87
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
dstringt::empty
bool empty() const
Definition: dstring.h:88
config
configt config
Definition: config.cpp:24
symbolt::clear
void clear()
Zero initialise a symbol object.
Definition: symbol.h:75
configt::ansi_ct::mode
flavourt mode
Definition: config.h:196
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
ansi_c_declarationt::get_is_global
bool get_is_global() const
Definition: ansi_c_declaration.h:127
ansi_c_declarationt::get_is_extern
bool get_is_extern() const
Definition: ansi_c_declaration.h:167
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:431
symbolt::is_type
bool is_type
Definition: symbol.h:61
ansi_c_declarationt::output
void output(std::ostream &) const
Definition: ansi_c_declaration.cpp:62
ansi_c_declarationt::full_type
typet full_type(const ansi_c_declaratort &) const
Definition: ansi_c_declaration.cpp:93
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
config.h
configt::ansi_ct::flavourt::GCC
@ GCC
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
symbolt::is_weak
bool is_weak
Definition: symbol.h:67
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
ansi_c_declarationt::get_is_inline
bool get_is_inline() const
Definition: ansi_c_declaration.h:157
merged_typet::last_type
typet & last_type()
Definition: merged_type.h:22