CBMC
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 <map>
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 
21 int yyansi_cparse();
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_stack.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 
72 
73  // recognize C++98 and C++11 keywords
74  bool cpp98, cpp11;
75 
76  // in C99 and upwards, for(;;) has a scope
78 
79  // ISO/IEC TS 18661-3:2015
81 
84 
85  typedef std::list<scopet> scopest;
87 
89  {
90  return scopes.front();
91  }
92 
93  const scopet &root_scope() const
94  {
95  return scopes.front();
96  }
97 
98  void pop_scope()
99  {
100  scopes.pop_back();
101  }
102 
104  {
105  assert(!scopes.empty());
106  return scopes.back();
107  }
108 
109  enum class decl_typet { TAG, MEMBER, PARAMETER, OTHER };
110 
111  // convert a declarator and then add it to existing an declaration
112  void add_declarator(exprt &declaration, irept &declarator);
113 
114  // adds a tag to the current scope
115  void add_tag_with_body(irept &tag);
116 
117  void copy_item(const ansi_c_declarationt &declaration)
118  {
119  assert(declaration.id()==ID_declaration);
120  parse_tree.items.push_back(declaration);
121  }
122 
123  void new_scope(const std::string &prefix)
124  {
125  const scopet &current=current_scope();
126  scopes.push_back(scopet());
127  scopes.back().prefix=current.prefix+prefix;
128  }
129 
131  const irep_idt &base_name, // in
132  irep_idt &identifier, // out
133  bool tag,
134  bool label);
135 
136  static ansi_c_id_classt get_class(const typet &type);
137 
138  irep_idt lookup_label(const irep_idt base_name)
139  {
140  irep_idt identifier;
141  lookup(base_name, identifier, false, true);
142  return identifier;
143  }
144 
146  bool pragma_cprover_empty();
147 
149  void pragma_cprover_push();
150 
152  void pragma_cprover_pop();
153 
155  void pragma_cprover_add_check(const irep_idt &name, bool enabled);
156 
159  bool pragma_cprover_clash(const irep_idt &name, bool enabled);
160 
163  void set_pragma_cprover();
164 
165 private:
166  std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
167 };
168 
170 
171 int yyansi_cerror(const std::string &error);
172 void ansi_c_scanner_init();
173 
174 #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:36
complexity_violationt::NONE
@ NONE
ansi_c_parsert::pragma_cprover_add_check
void pragma_cprover_add_check(const irep_idt &name, bool enabled)
Adds a check to the CPROVER pragma stack.
Definition: ansi_c_parser.cpp:194
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:83
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:74
ansi_c_id_classt
ansi_c_id_classt
Definition: ansi_c_scope.h:17
ansi_c_parsert::decl_typet
decl_typet
Definition: ansi_c_parser.h:109
ansi_c_parse_treet::items
itemst items
Definition: ansi_c_parse_tree.h:22
parsert::clear
virtual void clear()
Definition: parser.h:32
exprt
Base class for all expressions.
Definition: expr.h:55
ansi_c_parsert::modet
configt::ansi_ct::flavourt modet
Definition: ansi_c_parser.h:70
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:66
ansi_c_parsert::copy_item
void copy_item(const ansi_c_declarationt &declaration)
Definition: ansi_c_parser.h:117
ansi_c_parsert::new_scope
void new_scope(const std::string &prefix)
Definition: ansi_c_parser.h:123
ansi_c_parsert::asm_block_following
bool asm_block_following
Definition: ansi_c_parser.h:65
ansi_c_parsert::pragma_cprover_clash
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.
Definition: ansi_c_parser.cpp:204
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
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:68
ansi_c_parsert::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: ansi_c_parser.h:80
ansi_c_parsert::lookup_label
irep_idt lookup_label(const irep_idt base_name)
Definition: ansi_c_parser.h:138
ansi_c_parsert::pragma_cprover_pop
void pragma_cprover_pop()
Pops a level in the CPROVER pragma stack.
Definition: ansi_c_parser.cpp:189
ansi_c_parsert::decl_typet::OTHER
@ OTHER
ansi_c_parsert::pop_scope
void pop_scope()
Definition: ansi_c_parser.h:98
ansi_c_parsert::set_pragma_cprover
void set_pragma_cprover()
Tags source_location with the current CPROVER pragma stack.
Definition: ansi_c_parser.cpp:211
ansi_c_parsert::get_class
static ansi_c_id_classt get_class(const typet &type)
Definition: ansi_c_parser.cpp:157
ansi_c_scopet
Definition: ansi_c_scope.h:39
ansi_c_parsert::scopest
std::list< scopet > scopest
Definition: ansi_c_parser.h:85
ansi_c_parsert::decl_typet::PARAMETER
@ PARAMETER
ansi_c_parsert::ansi_c_parsert
ansi_c_parsert()
Definition: ansi_c_parser.h:28
ansi_c_parsert::clear
virtual void clear() override
Definition: ansi_c_parser.h:45
ansi_c_parser
ansi_c_parsert ansi_c_parser
Definition: ansi_c_parser.cpp:13
ansi_c_parsert
Definition: ansi_c_parser.h:23
ansi_c_scanner_init
void ansi_c_scanner_init()
ansi_c_parsert::string_literal
std::string string_literal
Definition: ansi_c_parser.h:67
ansi_c_parse_treet
Definition: ansi_c_parse_tree.h:17
irept::id
const irep_idt & id() const
Definition: irep.h:396
ansi_c_parsert::decl_typet::MEMBER
@ MEMBER
ansi_c_identifiert
Definition: ansi_c_scope.h:28
parsert
Definition: parser.h:23
ansi_c_parsert::tag_following
bool tag_following
Definition: ansi_c_parser.h:64
ansi_c_parsert::pragma_cprover_stack
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
Definition: ansi_c_parser.h:166
ansi_c_parsert::cpp11
bool cpp11
Definition: ansi_c_parser.h:74
ansi_c_parsert::mode
modet mode
Definition: ansi_c_parser.h:71
ansi_c_parsert::scopes
scopest scopes
Definition: ansi_c_parser.h:86
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:26
ansi_c_parsert::root_scope
const scopet & root_scope() const
Definition: ansi_c_parser.h:93
parser.h
ansi_c_parsert::current_scope
scopet & current_scope()
Definition: ansi_c_parser.h:103
ansi_c_parsert::pragma_cprover_empty
bool pragma_cprover_empty()
True iff the CPROVER pragma stack is empty.
Definition: ansi_c_parser.cpp:179
ansi_c_parsert::pragma_cprover_push
void pragma_cprover_push()
Pushes an empty level in the CPROVER pragma stack.
Definition: ansi_c_parser.cpp:184
ansi_c_parsert::parse
virtual bool parse() override
Definition: ansi_c_parser.h:40
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:359
ansi_c_parsert::identifiert
ansi_c_identifiert identifiert
Definition: ansi_c_parser.h:82
configt::ansi_ct::flavourt
flavourt
Definition: config.h:227
ansi_c_parsert::root_scope
scopet & root_scope()
Definition: ansi_c_parser.h:88
ansi_c_parsert::for_has_scope
bool for_has_scope
Definition: ansi_c_parser.h:77
ansi_c_parse_treet::clear
void clear()
Definition: ansi_c_parse_tree.cpp:18