cprover
ansi_c_parser.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
22
24{
25public:
27
29 : tag_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 {
49
50 // scanner state
51 tag_following=false;
54 string_literal.clear();
55 pragma_pack.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
139 {
140 irep_idt identifier;
141 lookup(base_name, identifier, false, true);
142 return identifier;
143 }
144
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
165private:
166 std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
167};
168
170
171int yyansi_cerror(const std::string &error);
173
174#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 pragma_cprover_pop()
Pops a level in the CPROVER pragma stack.
void set_pragma_cprover()
Tags source_location with the current CPROVER pragma stack.
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 pragma_cprover_empty()
True iff the CPROVER pragma stack is empty.
bool ts_18661_3_Floatn_types
Definition: ansi_c_parser.h:80
ansi_c_identifiert identifiert
Definition: ansi_c_parser.h:82
void add_declarator(exprt &declaration, irept &declarator)
ansi_c_scopet scopet
Definition: ansi_c_parser.h:83
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:26
std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
unsigned parenthesis_counter
Definition: ansi_c_parser.h:66
scopet & root_scope()
Definition: ansi_c_parser.h:88
scopet & current_scope()
configt::ansi_ct::flavourt modet
Definition: ansi_c_parser.h:70
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.
const scopet & root_scope() const
Definition: ansi_c_parser.h:93
std::list< scopet > scopest
Definition: ansi_c_parser.h:85
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)
void pragma_cprover_push()
Pushes an empty level in the CPROVER pragma stack.
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)
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
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:372
const irep_idt & id() const
Definition: irep.h:396
Definition: parser.h:24
virtual void clear()
Definition: parser.h:32
The type of an expression, extends irept.
Definition: type.h:29
@ OTHER
Definition: goto_program.h:37
Parser utilities.