cprover
Loading...
Searching...
No Matches
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
16 const irep_idt &base_name,
17 irep_idt &identifier, // output
18 bool tag,
19 bool label)
20{
21 // labels and tags have a separate name space
22 const irep_idt scope_name=
23 tag?"tag-"+id2string(base_name):
24 label?"label-"+id2string(base_name):
25 base_name;
26
27 for(scopest::const_reverse_iterator it=scopes.rbegin();
28 it!=scopes.rend();
29 it++)
30 {
31 scopet::name_mapt::const_iterator n_it=
32 it->name_map.find(scope_name);
33
34 if(n_it!=it->name_map.end())
35 {
36 identifier=n_it->second.prefixed_name;
37 return n_it->second.id_class;
38 }
39 }
40
41 // Not found.
42 // If it's a tag, we will add to current scope.
43 if(tag)
44 {
49 i.base_name=base_name;
50 identifier=i.prefixed_name;
52 }
53
54 identifier=base_name;
56}
57
59{
60 const std::string scope_name=
61 "tag-"+tag.get_string(ID_C_base_name);
62
64
65 if(prefixed_name!=tag.get(ID_identifier))
66 {
67 // re-defined in a deeper scope
68 ansi_c_identifiert &identifier=
71 identifier.prefixed_name=prefixed_name;
72 tag.set(ID_identifier, prefixed_name);
73 }
74}
75
76extern char *yyansi_ctext;
77
78int yyansi_cerror(const std::string &error)
79{
81 return 0;
82}
83
85 exprt &declaration,
86 irept &declarator)
87{
88 PRECONDITION(declarator.is_not_nil());
90 to_ansi_c_declaration(declaration);
91
93 new_declarator.build(declarator);
94
95 irep_idt base_name=new_declarator.get_base_name();
96
97 bool is_member=ansi_c_declaration.get_is_member();
98 bool is_parameter=ansi_c_declaration.get_is_parameter();
99
100 if(is_member)
101 {
102 // we don't put them into a struct scope (unlike C++)
103 new_declarator.set_name(base_name);
104 ansi_c_declaration.declarators().push_back(new_declarator);
105 return; // done
106 }
107
108 // global?
109 if(current_scope().prefix.empty())
110 ansi_c_declaration.set_is_global(true);
111
112 // abstract?
113 if(!base_name.empty())
114 {
115 c_storage_spect c_storage_spec(ansi_c_declaration.type());
116 bool is_typedef=c_storage_spec.is_typedef;
117 bool is_extern=c_storage_spec.is_extern;
118
119 bool force_root_scope=false;
120
121 // Functions always go into global scope, unless
122 // declared as a parameter or are typedefs.
123 if(new_declarator.type().id()==ID_code &&
124 !is_parameter &&
125 !is_typedef)
126 force_root_scope=true;
127
128 // variables marked as 'extern' always go into global scope
129 if(is_extern)
130 force_root_scope=true;
131
132 ansi_c_id_classt id_class=is_typedef?
135
136 scopet &scope=
138
139 // set the final name
140 irep_idt prefixed_name=force_root_scope?
141 base_name:
142 current_scope().prefix+id2string(base_name);
143 new_declarator.set_name(prefixed_name);
144
145 // add to scope
146 ansi_c_identifiert &identifier=scope.name_map[base_name];
147 identifier.id_class=id_class;
148 identifier.prefixed_name=prefixed_name;
149
151 current_scope().name_map[base_name] = identifier;
152 }
153
154 ansi_c_declaration.declarators().push_back(new_declarator);
155}
156
158{
159 if(type.id()==ID_typedef)
161 else if(type.id()==ID_struct ||
162 type.id()==ID_union ||
163 type.id()==ID_c_enum)
165 else if(type.id()==ID_merged_type)
166 {
167 for(const typet &subtype : to_type_with_subtypes(type).subtypes())
168 {
171 }
172 }
173 else if(type.has_subtype())
174 return get_class(to_type_with_subtype(type).subtype());
175
177}
178
183
188
193
195 const irep_idt &name,
196 bool enabled)
197{
198 if(pragma_cprover_stack.empty())
200
201 pragma_cprover_stack.back()[name] = enabled;
202}
203
205{
206 auto top = pragma_cprover_stack.back();
207 auto found = top.find(name);
208 return found != top.end() && found->second != enabled;
209}
210
212{
213 // handle enable/disable shadowing
214 // by bottom-to-top flattening
215 std::map<irep_idt, bool> flattened;
216
217 for(const auto &pragma_set : pragma_cprover_stack)
218 for(const auto &pragma : pragma_set)
219 flattened[pragma.first] = pragma.second;
220
222
223 for(const auto &pragma : flattened)
224 {
225 std::string check_name = id2string(pragma.first);
226 std::string full_name =
227 (pragma.second ? "enable:" : "disable:") + check_name;
228 source_location.add_pragma(full_name);
229 }
230}
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
char * yyansi_ctext
int yyansi_cerror(const std::string &error)
ansi_c_parsert ansi_c_parser
ansi_c_id_classt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:39
bool empty() const
Definition dstring.h:90
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:372
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:95
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
const std::string & get_string(const irep_idt &name) const
Definition irep.h:409
source_locationt source_location
Definition parser.h:139
void parse_error(const std::string &message, const std::string &before)
Definition parser.cpp:30
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:47
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:219
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175