cprover
Loading...
Searching...
No Matches
parser.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Parser utilities
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_UTIL_PARSER_H
13#define CPROVER_UTIL_PARSER_H
14
15#include <iosfwd>
16#include <string>
17#include <vector>
18
19#include "expr.h"
20#include "message.h"
21#include "file_util.h"
22
23class parsert:public messaget
24{
25public:
26 std::istream *in;
27
28 std::string this_line, last_line;
29
30 std::vector<exprt> stack;
31
32 virtual void clear()
33 {
34 line_no=0;
36 column=1;
37 stack.clear();
40 }
41
43 virtual ~parsert() { }
44
45 // The following are for the benefit of the scanner
46
47 bool read(char &ch)
48 {
49 if(!in->read(&ch, 1))
50 return false;
51
52 if(ch=='\n')
53 {
54 last_line.swap(this_line);
56 }
57 else
59
60 return true;
61 }
62
63 virtual bool parse()=0;
64
65 bool eof()
66 {
67 return in->eof();
68 }
69
70 void parse_error(
71 const std::string &message,
72 const std::string &before);
73
75 {
76 ++line_no;
77 column=1;
78 }
79
80 void set_line_no(unsigned _line_no)
81 {
83 }
84
91
93 {
95 }
96
97 unsigned get_line_no() const
98 {
99 return line_no;
100 }
101
102 unsigned get_column() const
103 {
104 return column;
105 }
106
107 void set_column(unsigned _column)
108 {
110 }
111
113 {
114 // Only set line number when needed, as this destroys sharing.
116 {
119 }
120
122 }
123
124 void set_function(const irep_idt &function)
125 {
127 }
128
130 {
132 }
133
134protected:
137 unsigned column;
138};
139
140exprt &_newstack(parsert &parser, unsigned &x);
141
142#define newstack(x) _newstack(PARSER, (x))
143
144#define parser_stack(x) (PARSER.stack[x])
145#define stack_expr(x) (PARSER.stack[x])
146#define stack_type(x) \
147 (static_cast<typet &>(static_cast<irept &>(PARSER.stack[x])))
148
149#define YY_INPUT(buf, result, max_size) \
150 do { \
151 for(result=0; result<max_size;) \
152 { \
153 char ch; \
154 if(!PARSER.read(ch)) /* NOLINT(readability/braces) */ \
155 { \
156 if(result==0) \
157 result=YY_NULL; \
158 break; \
159 } \
160 \
161 if(ch!='\r') /* NOLINT(readability/braces) */ \
162 { \
163 buf[result++]=ch; \
164 if(ch=='\n') /* NOLINT(readability/braces) */ \
165 { \
166 PARSER.inc_line_no(); \
167 break; \
168 } \
169 } \
170 } \
171 } while(0)
172
173// The following tracks the column of the token, and is nicely explained here:
174// http://oreilly.com/linux/excerpts/9780596155971/error-reporting-recovery.html
175
176#define YY_USER_ACTION PARSER.advance_column(yyleng);
177
178#endif // CPROVER_UTIL_PARSER_H
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
source_locationt & add_source_location()
Definition expr.h:235
void clear()
Definition irep.h:452
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
void advance_column(unsigned token_width)
Definition parser.h:129
source_locationt source_location
Definition parser.h:135
std::istream * in
Definition parser.h:26
void inc_line_no()
Definition parser.h:74
void set_column(unsigned _column)
Definition parser.h:107
bool eof()
Definition parser.h:65
void set_file(const irep_idt &file)
Definition parser.h:85
unsigned get_line_no() const
Definition parser.h:97
std::string last_line
Definition parser.h:28
virtual ~parsert()
Definition parser.h:43
virtual bool parse()=0
unsigned column
Definition parser.h:137
void set_source_location(exprt &e)
Definition parser.h:112
std::string this_line
Definition parser.h:28
parsert()
Definition parser.h:42
bool read(char &ch)
Definition parser.h:47
unsigned previous_line_no
Definition parser.h:136
void parse_error(const std::string &message, const std::string &before)
Definition parser.cpp:30
irep_idt get_file() const
Definition parser.h:92
std::vector< exprt > stack
Definition parser.h:30
unsigned line_no
Definition parser.h:136
void set_line_no(unsigned _line_no)
Definition parser.h:80
virtual void clear()
Definition parser.h:32
unsigned get_column() const
Definition parser.h:102
void set_function(const irep_idt &function)
Definition parser.h:124
void set_working_directory(const irep_idt &cwd)
const irep_idt & get_file() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
std::string get_current_working_directory()
Definition file_util.cpp:51
exprt & _newstack(parsert &parser, unsigned &x)
Definition parser.cpp:19
Definition kdev_t.h:19