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