cprover
ansi_c_parser.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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  {
46  current_scope().name_map[scope_name];
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 
63  irep_idt prefixed_name=current_scope().prefix+scope_name;
64 
65  if(prefixed_name!=tag.get(ID_identifier))
66  {
67  // re-defined in a deeper scope
68  ansi_c_identifiert &identifier=
69  current_scope().name_map[scope_name];
71  identifier.prefixed_name=prefixed_name;
72  tag.set(ID_identifier, prefixed_name);
73  }
74 }
75 
76 extern char *yyansi_ctext;
77 
78 int yyansi_cerror(const std::string &error)
79 {
81  return 0;
82 }
83 
85  exprt &declaration,
86  irept &declarator)
87 {
88  assert(declarator.is_not_nil());
89  ansi_c_declarationt &ansi_c_declaration=
90  to_ansi_c_declaration(declaration);
91 
92  ansi_c_declaratort new_declarator;
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=
137  force_root_scope?root_scope():current_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 
150  if(force_root_scope)
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 
180 {
181  return pragma_cprover_stack.empty();
182 }
183 
185 {
186  pragma_cprover_stack.emplace_back();
187 }
188 
190 {
191  pragma_cprover_stack.pop_back();
192 }
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 
204 bool ansi_c_parsert::pragma_cprover_clash(const irep_idt &name, bool enabled)
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 
221  source_location.remove(ID_pragma);
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
Definition: ansi_c_scope.h:18
bool get_is_parameter() const
void set_is_global(bool is_global)
const declaratorst & declarators() const
void set_name(const irep_idt &name)
void build(irept &src)
irep_idt get_base_name() const
ansi_c_id_classt id_class
Definition: ansi_c_scope.h:31
irep_idt prefixed_name
Definition: ansi_c_scope.h:32
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)
scopet & root_scope()
Definition: ansi_c_parser.h:88
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
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.
scopet & current_scope()
void pragma_cprover_add_check(const irep_idt &name, bool enabled)
Adds a check to the CPROVER pragma stack.
std::string prefix
Definition: ansi_c_scope.h:47
name_mapt name_map
Definition: ansi_c_scope.h:45
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
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:45
void remove(const irep_idt &name)
Definition: irep.cpp:96
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:135
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:66
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:221
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177