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 "expr.h"
16#include "message.h"
17
18#include <filesystem>
19#include <iosfwd>
20#include <string>
21#include <vector>
22
24{
25public:
26 std::istream *in;
27
28 std::string this_line, last_line;
29
30 std::vector<exprt> stack;
31
32 explicit parsert(message_handlert &message_handler)
33 : in(nullptr),
34 log(message_handler),
35 line_no(0),
37 column(1)
38 {
39 }
40
41 virtual ~parsert() { }
42
43 // The following are for the benefit of the scanner
44
45 bool read(char &ch)
46 {
47 if(!in->read(&ch, 1))
48 return false;
49
50 if(ch=='\n')
51 {
52 last_line.swap(this_line);
53 this_line.clear();
54 }
55 else
56 this_line+=ch;
57
58 return true;
59 }
60
61 virtual bool parse()=0;
62
63 bool eof()
64 {
65 return in->eof();
66 }
67
68 void parse_error(
69 const std::string &message,
70 const std::string &before);
71
73 {
74 ++line_no;
75 column=1;
76 }
77
78 void set_line_no(unsigned _line_no)
79 {
80 line_no=_line_no;
81 }
82
83 void set_file(const irep_idt &file)
84 {
87 std::filesystem::current_path().string());
88 }
89
91 {
93 }
94
95 unsigned get_line_no() const
96 {
97 return line_no;
98 }
99
100 unsigned get_column() const
101 {
102 return column;
103 }
104
105 void set_column(unsigned _column)
106 {
107 column=_column;
108 }
109
111 {
112 // Only set line number when needed, as this destroys sharing.
114 {
117 }
118
120 }
121
122 void set_function(const irep_idt &function)
123 {
125 }
126
127 void advance_column(unsigned token_width)
128 {
129 column+=token_width;
130 }
131
132protected:
136 unsigned column;
137};
138
139exprt &_newstack(parsert &parser, unsigned &x);
140
141#define newstack(x) _newstack(PARSER, (x))
142
143#define parser_stack(x) (PARSER.stack[x])
144#define stack_expr(x) (PARSER.stack[x])
145#define stack_type(x) \
146 (static_cast<typet &>(static_cast<irept &>(PARSER.stack[x])))
147
148#define YY_INPUT(buf, result, max_size) \
149 do { \
150 for(result=0; result<max_size;) \
151 { \
152 char ch; \
153 if(!PARSER.read(ch)) /* NOLINT(readability/braces) */ \
154 { \
155 if(result==0) \
156 result=YY_NULL; \
157 break; \
158 } \
159 \
160 if(ch!='\r') /* NOLINT(readability/braces) */ \
161 { \
162 buf[result++]=ch; \
163 if(ch=='\n') /* NOLINT(readability/braces) */ \
164 { \
165 PARSER.inc_line_no(); \
166 break; \
167 } \
168 } \
169 } \
170 } while(0)
171
172// The following tracks the column of the token, and is nicely explained here:
173// http://oreilly.com/linux/excerpts/9780596155971/error-reporting-recovery.html
174
175#define YY_USER_ACTION PARSER.advance_column(yyleng);
176
177#endif // CPROVER_UTIL_PARSER_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
source_locationt & add_source_location()
Definition expr.h:236
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
void advance_column(unsigned token_width)
Definition parser.h:127
source_locationt source_location
Definition parser.h:134
parsert(message_handlert &message_handler)
Definition parser.h:32
std::istream * in
Definition parser.h:26
void inc_line_no()
Definition parser.h:72
void set_column(unsigned _column)
Definition parser.h:105
bool eof()
Definition parser.h:63
void set_file(const irep_idt &file)
Definition parser.h:83
unsigned get_line_no() const
Definition parser.h:95
std::string last_line
Definition parser.h:28
virtual ~parsert()
Definition parser.h:41
virtual bool parse()=0
unsigned column
Definition parser.h:136
void set_source_location(exprt &e)
Definition parser.h:110
messaget log
Definition parser.h:133
std::string this_line
Definition parser.h:28
bool read(char &ch)
Definition parser.h:45
unsigned previous_line_no
Definition parser.h:135
void parse_error(const std::string &message, const std::string &before)
Definition parser.cpp:30
irep_idt get_file() const
Definition parser.h:90
std::vector< exprt > stack
Definition parser.h:30
unsigned line_no
Definition parser.h:135
void set_line_no(unsigned _line_no)
Definition parser.h:78
unsigned get_column() const
Definition parser.h:100
void set_function(const irep_idt &function)
Definition parser.h:122
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)
exprt & _newstack(parsert &parser, unsigned &x)
Definition parser.cpp:19
Definition kdev_t.h:19