cprover
Loading...
Searching...
No Matches
ansi_c_declaration.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Type Checking
4
5Author: 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.subtype();
57 }
58
59 type()=static_cast<const typet &>(src);
60 value().make_nil();
61}
62
63void 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";
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 p=&p->subtype();
107 else if(p->id()==ID_merged_type)
108 {
109 // we always go down on the right-most subtype
110 auto &merged_type = to_merged_type(*p);
111 p = &merged_type.last_type();
112 }
113 else
115 }
116
117 *p=type();
118
119 // retain typedef for dump-c
120 if(get_is_typedef())
121 result.set(ID_C_typedef, declarator.get_name());
122
123 return result;
124}
125
127 const ansi_c_declaratort &declarator,
128 symbolt &symbol) const
129{
130 symbol.clear();
131 symbol.value=declarator.value();
132 symbol.type=full_type(declarator);
133 symbol.name=declarator.get_name();
134 symbol.pretty_name=symbol.name;
136 symbol.is_type=get_is_typedef();
138 symbol.is_extern=get_is_extern();
141 symbol.is_weak=get_is_weak();
142
143 // is it a function?
144 const typet &type = symbol.type.id() == ID_merged_type
145 ? to_merged_type(symbol.type).last_type()
146 : symbol.type;
147
148 if(type.id() == ID_code && !symbol.is_type)
149 {
150 symbol.is_static_lifetime=false;
151 symbol.is_thread_local=false;
152
154
155 if(get_is_inline())
156 to_code_type(symbol.type).set_inlined(true);
157
158 if(
162 {
163 // GCC extern inline cleanup, to enable remove_internal_symbols
164 // do its full job
165 // https://gcc.gnu.org/ml/gcc/2006-11/msg00006.html
166 // __attribute__((__gnu_inline__))
167 if(get_is_inline())
168 {
169 if(get_is_static()) // C99 and above
170 symbol.is_extern=false;
171 else if(get_is_extern()) // traditional GCC
172 symbol.is_file_local=true;
173 }
174
175 // GCC __attribute__((__used__)) - do not treat those as file-local
176 if(get_is_used())
177 symbol.is_file_local = false;
178 }
179 }
180 else // non-function
181 {
182 symbol.is_static_lifetime=
183 !symbol.is_macro &&
184 !symbol.is_type &&
186
187 symbol.is_thread_local=
188 (!symbol.is_static_lifetime && !get_is_extern()) ||
190
191 symbol.is_file_local=
192 symbol.is_macro ||
193 (!get_is_global() && !get_is_extern()) ||
194 (get_is_global() && get_is_static() && !get_is_used()) ||
195 symbol.is_parameter;
196 }
197}
ANSI-CC Language Type Checking.
const ansi_c_declaratort & declarator() const
const declaratorst & declarators() const
typet full_type(const ansi_c_declaratort &) const
bool get_is_enum_constant() const
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
bool get_is_thread_local() const
bool get_is_static_assert() const
void output(std::ostream &) const
void set_base_name(const irep_idt &base_name)
irep_idt get_base_name() const
irep_idt get_name() const
void set_inlined(bool value)
Definition std_types.h:670
struct configt::ansi_ct ansi_c
bool empty() const
Definition dstring.h:88
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
typet & last_type()
Definition merged_type.h:22
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
void clear()
Zero initialise a symbol object.
Definition symbol.h:75
bool is_extern
Definition symbol.h:66
bool is_macro
Definition symbol.h:61
bool is_file_local
Definition symbol.h:66
bool is_static_lifetime
Definition symbol.h:65
bool is_parameter
Definition symbol.h:67
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
bool is_weak
Definition symbol.h:67
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
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
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:503
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
flavourt mode
Definition config.h:222
Symbol table entry.