CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
ansi_c_parser.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "ansi_c_parser.h"
10
11#include "c_storage_spec.h"
12
14 const irep_idt &base_name,
15 irep_idt &identifier, // output
16 bool tag,
17 bool label)
18{
19 // labels and tags have a separate name space
20 const irep_idt scope_name=
21 tag?"tag-"+id2string(base_name):
22 label?"label-"+id2string(base_name):
23 base_name;
24
25 for(scopest::const_reverse_iterator it=scopes.rbegin();
26 it!=scopes.rend();
27 it++)
28 {
29 scopet::name_mapt::const_iterator n_it=
30 it->name_map.find(scope_name);
31
32 if(n_it!=it->name_map.end())
33 {
34 identifier=n_it->second.prefixed_name;
35 return n_it->second.id_class;
36 }
37 }
38
39 // Not found.
40 // If it's a tag, we will add to current scope.
41 if(tag)
42 {
47 i.base_name=base_name;
48 identifier=i.prefixed_name;
50 }
51
52 identifier=base_name;
54}
55
57{
58 const std::string scope_name=
59 "tag-"+tag.get_string(ID_C_base_name);
60
62
63 if(prefixed_name!=tag.get(ID_identifier))
64 {
65 // re-defined in a deeper scope
66 ansi_c_identifiert &identifier=
69 identifier.prefixed_name=prefixed_name;
70 tag.set(ID_identifier, prefixed_name);
71 }
72}
73
75 exprt &declaration,
76 irept &declarator)
77{
78 PRECONDITION(declarator.is_not_nil());
80 to_ansi_c_declaration(declaration);
81
83 new_declarator.build(declarator);
84
85 irep_idt base_name=new_declarator.get_base_name();
86
87 bool is_member=ansi_c_declaration.get_is_member();
88 bool is_parameter=ansi_c_declaration.get_is_parameter();
89
90 if(is_member)
91 {
92 // we don't put them into a struct scope (unlike C++)
93 new_declarator.set_name(base_name);
94 ansi_c_declaration.declarators().push_back(new_declarator);
95 return; // done
96 }
97
98 // global?
99 if(current_scope().prefix.empty())
100 ansi_c_declaration.set_is_global(true);
101
102 // abstract?
103 if(!base_name.empty())
104 {
105 c_storage_spect c_storage_spec(ansi_c_declaration.type());
106 bool is_typedef=c_storage_spec.is_typedef;
107 bool is_extern=c_storage_spec.is_extern;
108
109 bool force_root_scope=false;
110
111 // Functions always go into global scope, unless
112 // declared as a parameter or are typedefs.
113 if(new_declarator.type().id()==ID_code &&
114 !is_parameter &&
115 !is_typedef)
116 force_root_scope=true;
117
118 // variables marked as 'extern' always go into global scope
119 if(is_extern)
120 force_root_scope=true;
121
122 ansi_c_id_classt id_class=is_typedef?
125
126 scopet &scope=
128
129 // set the final name
130 irep_idt prefixed_name=force_root_scope?
131 base_name:
132 current_scope().prefix+id2string(base_name);
133 new_declarator.set_name(prefixed_name);
134
135 // add to scope
136 ansi_c_identifiert &identifier=scope.name_map[base_name];
137 identifier.id_class=id_class;
138 identifier.prefixed_name=prefixed_name;
139
141 current_scope().name_map[base_name] = identifier;
142 }
143
144 ansi_c_declaration.declarators().push_back(new_declarator);
145}
146
148{
149 if(type.id()==ID_typedef)
151 else if(type.id()==ID_struct ||
152 type.id()==ID_union ||
153 type.id()==ID_c_enum)
155 else if(type.id()==ID_merged_type)
156 {
157 for(const typet &subtype : to_type_with_subtypes(type).subtypes())
158 {
161 }
162 }
163 else if(type.has_subtype())
164 return get_class(to_type_with_subtype(type).subtype());
165
167}
168
173
178
183
185 const irep_idt &name,
186 bool enabled)
187{
188 if(pragma_cprover_stack.empty())
190
191 pragma_cprover_stack.back()[name] = enabled;
192}
193
195{
196 auto top = pragma_cprover_stack.back();
197 auto found = top.find(name);
198 return found != top.end() && found->second != enabled;
199}
200
202{
203 // handle enable/disable shadowing
204 // by bottom-to-top flattening
205 std::map<irep_idt, bool> flattened;
206
207 for(const auto &pragma_set : pragma_cprover_stack)
208 for(const auto &pragma : pragma_set)
209 flattened[pragma.first] = pragma.second;
210
212
213 for(const auto &pragma : flattened)
214 {
215 std::string check_name = id2string(pragma.first);
216 std::string full_name =
217 (pragma.second ? "enable:" : "disable:") + check_name;
218 _source_location.add_pragma(full_name);
219 }
220}
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
ansi_c_id_classt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ansi_c_id_classt id_class
void pragma_cprover_pop()
Pops a level in the CPROVER pragma stack.
void set_pragma_cprover()
Tags source_location with the current CPROVER pragma stack.
bool pragma_cprover_empty()
True iff the CPROVER pragma stack is empty.
void add_declarator(exprt &declaration, irept &declarator)
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
scopet & root_scope()
scopet & current_scope()
void add_tag_with_body(irept &tag)
bool pragma_cprover_clash(const irep_idt &name, bool enabled)
Returns true iff the same check with polarity is already present at top of the stack.
static ansi_c_id_classt get_class(const typet &type)
ansi_c_id_classt lookup(const irep_idt &base_name, irep_idt &identifier, bool tag, bool label)
void pragma_cprover_push()
Pushes an empty level in the CPROVER pragma stack.
void pragma_cprover_add_check(const irep_idt &name, bool enabled)
Adds a check to the CPROVER pragma stack.
std::string prefix
name_mapt name_map
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
bool is_not_nil() const
Definition irep.h:372
const irep_idt & id() const
Definition irep.h:388
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
source_locationt _source_location
Definition parser.h:145
void add_pragma(const irep_idt &pragma)
The type of an expression, extends irept.
Definition type.h:29
bool has_subtype() const
Definition type.h:64
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:252
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208