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 #include <cassert>
16 
17 #include <util/config.h>
18 #include <util/std_types.h>
19 #include <util/invariant.h>
20 
22 {
23  typet *p=static_cast<typet *>(&src);
24 
25  // walk down subtype until we hit typedef_type, symbol or "abstract"
26  while(true)
27  {
28  typet &t=*p;
29 
30  if(t.id() == ID_typedef_type || t.id() == ID_symbol)
31  {
32  set_base_name(t.get(ID_C_base_name));
34  t.make_nil();
35  break;
36  }
37  else if(t.id().empty() ||
38  t.is_nil())
39  {
41  }
42  else if(t.id()==ID_abstract)
43  {
44  t.make_nil();
45  break;
46  }
47  else if(t.id()==ID_merged_type)
48  {
49  // we always walk down the _last_ member of a merged type
50  assert(!t.subtypes().empty());
51  p=&(t.subtypes().back());
52  }
53  else
54  p=&t.subtype();
55  }
56 
57  type()=static_cast<const typet &>(src);
58  value().make_nil();
59 }
60 
61 void ansi_c_declarationt::output(std::ostream &out) const
62 {
63  out << "Flags:";
64  if(get_is_typedef())
65  out << " is_typedef";
67  out << " is_enum_constant";
68  if(get_is_static())
69  out << " is_static";
70  if(get_is_parameter())
71  out << " is_parameter";
72  if(get_is_global())
73  out << " is_global";
74  if(get_is_register())
75  out << " is_register";
77  out << " is_thread_local";
78  if(get_is_inline())
79  out << " is_inline";
80  if(get_is_extern())
81  out << " is_extern";
83  out << " is_static_assert";
84  out << "\n";
85 
86  out << "Type: " << type().pretty() << "\n";
87 
88  for(const auto &declarator : declarators())
89  out << "Declarator: " << declarator.pretty() << "\n";
90 }
91 
93  const ansi_c_declaratort &declarator) const
94 {
95  typet result=declarator.type();
96  typet *p=&result;
97 
98  // this gets types that are still raw parse trees
99  while(p->is_not_nil())
100  {
101  if(p->id()==ID_frontend_pointer || p->id()==ID_array ||
102  p->id()==ID_vector || p->id()==ID_c_bit_field ||
103  p->id()==ID_block_pointer || p->id()==ID_code)
104  p=&p->subtype();
105  else if(p->id()==ID_merged_type)
106  {
107  // we always go down on the right-most subtype
108  assert(!p->subtypes().empty());
109  p=&(p->subtypes().back());
110  }
111  else
112  UNREACHABLE;
113  }
114 
115  *p=type();
116 
117  // retain typedef for dump-c
118  if(get_is_typedef())
119  result.set(ID_C_typedef, declarator.get_name());
120 
121  return result;
122 }
123 
125  const ansi_c_declaratort &declarator,
126  symbolt &symbol) const
127 {
128  symbol.clear();
129  symbol.value=declarator.value();
130  symbol.type=full_type(declarator);
131  symbol.name=declarator.get_name();
132  symbol.pretty_name=symbol.name;
134  symbol.is_type=get_is_typedef();
136  symbol.is_extern=get_is_extern();
139  symbol.is_weak=get_is_weak();
140 
141  // is it a function?
142 
143  if(symbol.type.id()==ID_code && !symbol.is_type)
144  {
145  symbol.is_static_lifetime=false;
146  symbol.is_thread_local=false;
147 
148  symbol.is_file_local=get_is_static();
149 
150  if(get_is_inline())
151  symbol.type.set(ID_C_inlined, true);
152 
153  if(
157  {
158  // GCC extern inline cleanup, to enable remove_internal_symbols
159  // do its full job
160  // https://gcc.gnu.org/ml/gcc/2006-11/msg00006.html
161  // __attribute__((__gnu_inline__))
162  if(get_is_inline())
163  {
164  if(get_is_static()) // C99 and above
165  symbol.is_extern=false;
166  else if(get_is_extern()) // traditional GCC
167  symbol.is_file_local=true;
168  }
169 
170  // GCC __attribute__((__used__)) - do not treat those as file-local
171  if(get_is_used())
172  symbol.is_file_local = false;
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 ||
188  (!get_is_global() && !get_is_extern()) ||
189  (get_is_global() && get_is_static() && !get_is_used()) ||
190  symbol.is_parameter;
191  }
192 }
bool get_is_static_assert() const
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
bool get_is_static() const
struct configt::ansi_ct ansi_c
bool get_is_register() const
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
bool is_thread_local
Definition: symbol.h:67
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool get_is_typedef() const
void clear()
Definition: symbol.h:76
void build(irept &src)
subtypest & subtypes()
Definition: type.h:58
exprt value
Initial value of symbol.
Definition: symbol.h:37
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
configt config
Definition: config.cpp:23
typet full_type(const ansi_c_declaratort &) const
bool is_static_lifetime
Definition: symbol.h:67
const irep_idt & id() const
Definition: irep.h:259
const declaratorst & declarators() const
irep_idt get_base_name() const
void set_base_name(const irep_idt &base_name)
flavourt mode
Definition: config.h:114
bool is_parameter
Definition: symbol.h:68
bool get_is_enum_constant() const
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
irep_idt get_name() const
Base class for tree-like data structures with sharing.
Definition: irep.h:156
const source_locationt & source_location() const
Definition: type.h:97
void output(std::ostream &) const
bool is_extern
Definition: symbol.h:68
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
API to type classes.
bool get_is_parameter() const
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:271
bool is_file_local
Definition: symbol.h:68
ANSI-CC Language Type Checking.
void make_nil()
Definition: irep.h:315
bool is_weak
Definition: symbol.h:68
source_locationt & add_source_location()
Definition: expr.h:130
bool is_type
Definition: symbol.h:63
const typet & subtype() const
Definition: type.h:33
bool empty() const
Definition: dstring.h:73
bool is_macro
Definition: symbol.h:63
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
bool get_is_thread_local() const
const ansi_c_declaratort & declarator() const