cprover
ansi_c_parser.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_ANSI_C_ANSI_C_PARSER_H
11 #define CPROVER_ANSI_C_ANSI_C_PARSER_H
12 
13 #include <set>
14 
15 #include <util/parser.h>
16 #include <util/config.h>
17 
18 #include "ansi_c_parse_tree.h"
19 #include "ansi_c_scope.h"
20 
22 
23 class ansi_c_parsert:public parsert
24 {
25 public:
27 
29  : tag_following(false),
30  asm_block_following(false),
32  mode(modet::NONE),
33  cpp98(false),
34  cpp11(false),
35  for_has_scope(false),
37  {
38  }
39 
40  virtual bool parse() override
41  {
42  return yyansi_cparse()!=0;
43  }
44 
45  virtual void clear() override
46  {
48  parse_tree.clear();
49 
50  // scanner state
51  tag_following=false;
52  asm_block_following=false;
54  string_literal.clear();
55  pragma_pack.clear();
56  pragma_cprover.clear();
57 
58  // set up global scope
59  scopes.clear();
60  scopes.push_back(scopet());
61  }
62 
63  // internal state of the scanner
67  std::string string_literal;
68  std::list<exprt> pragma_pack;
69  std::list<std::set<irep_idt>> pragma_cprover;
70 
73 
74  // recognize C++98 and C++11 keywords
75  bool cpp98, cpp11;
76 
77  // in C99 and upwards, for(;;) has a scope
79 
80  // ISO/IEC TS 18661-3:2015
82 
85 
86  typedef std::list<scopet> scopest;
88 
90  {
91  return scopes.front();
92  }
93 
94  const scopet &root_scope() const
95  {
96  return scopes.front();
97  }
98 
99  void pop_scope()
100  {
101  scopes.pop_back();
102  }
103 
105  {
106  assert(!scopes.empty());
107  return scopes.back();
108  }
109 
110  enum class decl_typet { TAG, MEMBER, PARAMETER, OTHER };
111 
112  // convert a declarator and then add it to existing an declaration
113  void add_declarator(exprt &declaration, irept &declarator);
114 
115  // adds a tag to the current scope
116  void add_tag_with_body(irept &tag);
117 
118  void copy_item(const ansi_c_declarationt &declaration)
119  {
120  assert(declaration.id()==ID_declaration);
121  parse_tree.items.push_back(declaration);
122  }
123 
124  void new_scope(const std::string &prefix)
125  {
126  const scopet &current=current_scope();
127  scopes.push_back(scopet());
128  scopes.back().prefix=current.prefix+prefix;
129  }
130 
132  const irep_idt &base_name, // in
133  irep_idt &identifier, // out
134  bool tag,
135  bool label);
136 
137  static ansi_c_id_classt get_class(const typet &type);
138 
139  irep_idt lookup_label(const irep_idt base_name)
140  {
141  irep_idt identifier;
142  lookup(base_name, identifier, false, true);
143  return identifier;
144  }
145 
147  {
148  source_location.remove(ID_pragma);
149  for(const auto &pragma_set : pragma_cprover)
150  {
151  for(const auto &pragma : pragma_set)
152  source_location.add_pragma(pragma);
153  }
154  }
155 };
156 
158 
159 int yyansi_cerror(const std::string &error);
161 
162 #endif // CPROVER_ANSI_C_ANSI_C_PARSER_H
int yyansi_cerror(const std::string &error)
ansi_c_parsert ansi_c_parser
void ansi_c_scanner_init()
int yyansi_cparse()
ansi_c_id_classt
Definition: ansi_c_scope.h:18
void set_pragma_cprover()
std::list< exprt > pragma_pack
Definition: ansi_c_parser.h:68
bool asm_block_following
Definition: ansi_c_parser.h:65
void new_scope(const std::string &prefix)
bool ts_18661_3_Floatn_types
Definition: ansi_c_parser.h:81
ansi_c_identifiert identifiert
Definition: ansi_c_parser.h:83
void add_declarator(exprt &declaration, irept &declarator)
ansi_c_scopet scopet
Definition: ansi_c_parser.h:84
std::list< std::set< irep_idt > > pragma_cprover
Definition: ansi_c_parser.h:69
scopet & root_scope()
Definition: ansi_c_parser.h:89
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:26
unsigned parenthesis_counter
Definition: ansi_c_parser.h:66
configt::ansi_ct::flavourt modet
Definition: ansi_c_parser.h:71
void add_tag_with_body(irept &tag)
std::list< scopet > scopest
Definition: ansi_c_parser.h:86
static ansi_c_id_classt get_class(const typet &type)
virtual void clear() override
Definition: ansi_c_parser.h:45
ansi_c_id_classt lookup(const irep_idt &base_name, irep_idt &identifier, bool tag, bool label)
void copy_item(const ansi_c_declarationt &declaration)
scopet & current_scope()
virtual bool parse() override
Definition: ansi_c_parser.h:40
std::string string_literal
Definition: ansi_c_parser.h:67
irep_idt lookup_label(const irep_idt base_name)
const scopet & root_scope() const
Definition: ansi_c_parser.h:94
std::string prefix
Definition: ansi_c_scope.h:47
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
const irep_idt & id() const
Definition: irep.h:407
void remove(const irep_namet &name)
Definition: irep.cpp:96
Definition: parser.h:24
source_locationt source_location
Definition: parser.h:135
virtual void clear()
Definition: parser.h:32
void add_pragma(const irep_idt &pragma)
The type of an expression, extends irept.
Definition: type.h:28
Parser utilities.