CBMC: /home/runner/work/cbmc/cbmc/src/util/parser.h Source File

CBMC
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 <limits>
21#include <string>
22#include <vector>
23
24 class parsert
25{
26public:
27 std::istream *in;
28
29 std::string this_line, last_line;
30
31 std::vector<exprt> stack;
32
33 explicit parsert(message_handlert &message_handler)
34 : in(nullptr),
35 log(message_handler),
36 line_no(0),
38 column(1)
39 {
40 }
41
42 virtual ~parsert() { }
43
44 // The following are for the benefit of the scanner
45
46 bool read(char &ch)
47 {
48 if(!in->read(&ch, 1))
49 return false;
50
51 if(ch=='\n')
52 {
53 last_line.swap(this_line);
55 }
56 else
58
59 return true;
60 }
61
62 virtual bool parse()=0;
63
64 bool eof()
65 {
66 return in->eof();
67 }
68
69 void parse_error(
70 const std::string &message,
71 const std::string &before);
72
74 {
75 ++line_no;
76 column=1;
77 }
78
79 void set_line_no(unsigned _line_no)
80 {
82 }
83
84 void set_file(const irep_idt &file)
85 {
88 std::filesystem::current_path().string());
89 }
90
92{
94 }
95
96 unsigned get_line_no() const
97{
98 return line_no;
99 }
100
101 unsigned get_column() const
102{
103 return column;
104 }
105
106 void set_column(unsigned _column)
107 {
109 }
110
112 {
113 // Only set line number when needed, as this destroys sharing.
115 {
117
118 // for the case of a file with no newlines
119 if(line_no == 0)
121 else
123 }
124
125 return _source_location;
126 }
127
132
133 void set_function(const irep_idt &function)
134 {
136 }
137
142
144 {
146 }
147
148protected:
152 unsigned column;
153};
154
155exprt &_newstack(parsert &parser, unsigned &x);
156
157 #define newstack(x) _newstack(PARSER, (x))
158
159 #define parser_stack(x) (PARSER.stack[x])
160 #define stack_expr(x) (PARSER.stack[x])
161 #define stack_type(x) \
162 (static_cast<typet &>(static_cast<irept &>(PARSER.stack[x])))
163
164 #define YY_INPUT(buf, result, max_size) \
165 do { \
166 for(result=0; result<max_size;) \
167 { \
168 char ch; \
169 if(!PARSER.read(ch)) /* NOLINT(readability/braces) */ \
170 { \
171 if(result==0) \
172 result=YY_NULL; \
173 break; \
174 } \
175 \
176 if(ch!='\r') /* NOLINT(readability/braces) */ \
177 { \
178 buf[result++]=ch; \
179 if(ch=='\n') /* NOLINT(readability/braces) */ \
180 { \
181 PARSER.inc_line_no(); \
182 break; \
183 } \
184 } \
185 } \
186 } while(0)
187
188// The following tracks the column of the token, and is nicely explained here:
189// http://oreilly.com/linux/excerpts/9780596155971/error-reporting-recovery.html
190
191 #define YY_USER_ACTION PARSER.advance_column(yyleng);
192
193#endif // CPROVER_UTIL_PARSER_H
virtual void clear()
Reset the abstract state.
Definition ai.h:269
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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:57
source_locationt & add_source_location()
Definition expr.h:241
Definition message.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Definition parser.h:25
void advance_column(unsigned token_width)
Definition parser.h:143
parsert(message_handlert &message_handler)
Definition parser.h:33
std::istream * in
Definition parser.h:27
void clear_function()
Definition parser.h:138
void inc_line_no()
Definition parser.h:73
void set_column(unsigned _column)
Definition parser.h:106
bool eof()
Definition parser.h:64
const source_locationt & source_location()
Definition parser.h:111
void set_file(const irep_idt &file)
Definition parser.h:84
unsigned get_line_no() const
Definition parser.h:96
std::string last_line
Definition parser.h:29
virtual ~parsert()
Definition parser.h:42
virtual bool parse()=0
unsigned column
Definition parser.h:152
void set_source_location(exprt &e)
Definition parser.h:128
messaget log
Definition parser.h:149
std::string this_line
Definition parser.h:29
bool read(char &ch)
Definition parser.h:46
unsigned previous_line_no
Definition parser.h:151
void parse_error(const std::string &message, const std::string &before)
Definition parser.cpp:30
source_locationt _source_location
Definition parser.h:150
irep_idt get_file() const
Definition parser.h:91
std::vector< exprt > stack
Definition parser.h:31
unsigned line_no
Definition parser.h:151
void set_line_no(unsigned _line_no)
Definition parser.h:79
unsigned get_column() const
Definition parser.h:101
void set_function(const irep_idt &function)
Definition parser.h:133
void set_working_directory(const irep_idt &cwd)
void clear_function()
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)
STL namespace.
exprt & _newstack(parsert &parser, unsigned &x)
Definition parser.cpp:19

AltStyle によって変換されたページ (->オリジナル) /