CBMC
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/invariant.h>
18 #include <util/std_types.h>
19 #include <util/symbol.h>
20 
21 #include "merged_type.h"
22 
24 {
25  typet *p=static_cast<typet *>(&src);
26 
27  // walk down subtype until we hit typedef_type, symbol or "abstract"
28  while(true)
29  {
30  typet &t=*p;
31 
32  if(t.id() == ID_typedef_type || t.id() == ID_symbol)
33  {
34  set_base_name(t.get(ID_C_base_name));
36  t.make_nil();
37  break;
38  }
39  else if(t.id().empty() ||
40  t.is_nil())
41  {
43  }
44  else if(t.id()==ID_abstract)
45  {
46  t.make_nil();
47  break;
48  }
49  else if(t.id()==ID_merged_type)
50  {
51  // we always walk down the _last_ member of a merged type
52  auto &merged_type = to_merged_type(t);
53  p = &merged_type.last_type();
54  }
55  else
56  p = &t.add_subtype();
57  }
58 
59  type()=static_cast<const typet &>(src);
60  value().make_nil();
61 }
62 
63 void ansi_c_declarationt::output(std::ostream &out) const
64 {
65  out << "Flags:";
66  if(get_is_typedef())
67  out << " is_typedef";
69  out << " is_enum_constant";
70  if(get_is_static())
71  out << " is_static";
72  if(get_is_parameter())
73  out << " is_parameter";
74  if(get_is_global())
75  out << " is_global";
76  if(get_is_register())
77  out << " is_register";
79  out << " is_thread_local";
80  if(get_is_inline())
81  out << " is_inline";
82  if(get_is_extern())
83  out << " is_extern";
85  out << " is_static_assert";
86  out << "\n";
87 
88  out << "Type: " << type().pretty() << "\n";
89 
90  for(const auto &declarator : declarators())
91  out << "Declarator: " << declarator.pretty() << "\n";
92 }
93 
95  const ansi_c_declaratort &declarator) const
96 {
97  typet result=declarator.type();
98  typet *p=&result;
99 
100  // this gets types that are still raw parse trees
101  while(p->is_not_nil())
102  {
103  if(p->id()==ID_frontend_pointer || p->id()==ID_array ||
104  p->id()==ID_vector || p->id()==ID_c_bit_field ||
105  p->id()==ID_block_pointer || p->id()==ID_code)
106  {
107  p = &p->add_subtype();
108  }
109  else if(p->id()==ID_merged_type)
110  {
111  // we always go down on the right-most subtype
112  auto &merged_type = to_merged_type(*p);
113  p = &merged_type.last_type();
114  }
115  else
116  UNREACHABLE;
117  }
118 
119  *p=type();
120 
121  // retain typedef for dump-c
122  if(get_is_typedef())
123  result.set(ID_C_typedef, declarator.get_name());
124 
125  return result;
126 }
127 
128 symbolt
130 {
131  symbolt symbol{declarator.get_name(), full_type(declarator), ID_C};
132  symbol.value=declarator.value();
133  symbol.pretty_name=symbol.name;
134  symbol.base_name=declarator.get_base_name();
135  symbol.is_type=get_is_typedef();
136  symbol.location=declarator.source_location();
137  symbol.is_extern=get_is_extern();
138  symbol.is_macro=get_is_typedef() || get_is_enum_constant();
139  symbol.is_parameter=get_is_parameter();
140  symbol.is_weak=get_is_weak();
141 
142  // is it a function?
143  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())
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  }
175  else // non-function
176  {
177  symbol.is_static_lifetime=
178  !symbol.is_macro &&
179  !symbol.is_type &&
180  (get_is_global() || get_is_static());
181 
182  symbol.is_thread_local=
183  (!symbol.is_static_lifetime && !get_is_extern()) ||
185 
186  symbol.is_file_local =
187  symbol.is_macro || (!get_is_global() && !get_is_extern()) ||
188  (get_is_global() && get_is_static()) || symbol.is_parameter;
189  }
190 
191  return symbol;
192 }
ANSI-CC Language Type Checking.
configt config
Definition: config.cpp:25
symbolt to_symbol(const ansi_c_declaratort &) const
bool get_is_parameter() const
typet full_type(const ansi_c_declaratort &) const
bool get_is_enum_constant() const
bool get_is_static() const
const ansi_c_declaratort & declarator() const
const declaratorst & declarators() const
bool get_is_register() const
bool get_is_thread_local() const
bool get_is_typedef() const
bool get_is_static_assert() const
void output(std::ostream &) const
void set_base_name(const irep_idt &base_name)
void build(irept &src)
irep_idt get_base_name() const
irep_idt get_name() const
void set_inlined(bool value)
Definition: std_types.h:714
struct configt::ansi_ct ansi_c
bool empty() const
Definition: dstring.h:89
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
bool is_not_nil() const
Definition: irep.h:368
const irep_idt & id() const
Definition: irep.h:384
void make_nil()
Definition: irep.h:442
bool is_nil() const
Definition: irep.h:364
typet & last_type()
Definition: merged_type.h:22
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
typet & add_subtype()
Definition: type.h:53
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
Definition: merged_type.h:29
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
flavourt mode
Definition: config.h:252
Symbol table entry.