CBMC
cpp_token_buffer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Parser: Token Buffer
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_token_buffer.h"
13 
14 #include <ansi-c/ansi_c_parser.h>
15 
16 int cpp_token_buffert::LookAhead(unsigned offset)
17 {
18  assert(current_pos<=token_vector.size());
19 
20  offset+=current_pos;
21 
22  while(offset>=token_vector.size())
23  read_token();
24 
25  return token_vector[offset]->kind;
26 }
27 
29 {
30  assert(current_pos<=token_vector.size());
31 
32  if(token_vector.size()==current_pos)
33  read_token();
34 
35  token=*token_vector[current_pos];
36 
37  current_pos++;
38 
39  return token.kind;
40 }
41 
43 {
44  assert(current_pos<=token_vector.size());
45 
46  if(token_vector.size()==current_pos)
47  read_token();
48 
49  int kind=token_vector[current_pos]->kind;
50 
51  current_pos++;
52 
53  return kind;
54 }
55 
56 int cpp_token_buffert::LookAhead(unsigned offset, cpp_tokent &token)
57 {
58  assert(current_pos<=token_vector.size());
59 
60  offset+=current_pos;
61 
62  while(offset>=token_vector.size())
63  read_token();
64 
65  token=*token_vector[offset];
66 
67  return token.kind;
68 }
69 
70 int yyansi_clex();
71 extern char *yyansi_ctext;
72 
74 {
75  tokens.push_back(cpp_tokent());
76  token_vector.push_back(--tokens.end());
77 
78  int kind;
79 
80  ansi_c_parser.stack.clear();
81  kind=yyansi_clex();
82  tokens.back().text=yyansi_ctext;
83  if(ansi_c_parser.stack.size()==1)
84  {
85  tokens.back().data=ansi_c_parser.stack.front();
86  tokens.back().line_no=ansi_c_parser.get_line_no();
87  tokens.back().filename=ansi_c_parser.get_file();
88  }
89 
90  // std::cout << "TOKEN: " << kind << " " << tokens.back().text << '\n';
91 
92  tokens.back().kind=kind;
93 
94  // std::cout << "II: " << token_vector.back()->kind << '\n';
95  // std::cout << "I2: " << token_vector.size() << '\n';
96 }
97 
99 {
100  return current_pos;
101 }
102 
104 {
106 }
107 
109 {
110  assert(current_pos<=token_vector.size());
111 
112  if(token_vector.size()==current_pos)
113  read_token();
114 
115  *token_vector[current_pos]=token;
116 }
117 
119 {
120  assert(current_pos<=token_vector.size());
121 
122  tokens.push_back(token);
123 
124  token_vector.insert(token_vector.begin()+current_pos,
125  --tokens.end());
126 }
ansi_c_parser
ansi_c_parsert ansi_c_parser
Definition: ansi_c_parser.cpp:13
cpp_tokent::kind
int kind
Definition: cpp_token.h:22
cpp_token_buffert::LookAhead
int LookAhead(unsigned offset)
Definition: cpp_token_buffer.cpp:16
pos
literalt pos(literalt a)
Definition: literal.h:194
cpp_token_buffert::tokens
tokenst tokens
Definition: cpp_token_buffer.h:56
yyansi_ctext
char * yyansi_ctext
cpp_token_buffert::Replace
void Replace(const cpp_tokent &token)
Definition: cpp_token_buffer.cpp:108
cpp_tokent
Definition: cpp_token.h:19
cpp_token_buffert::Insert
void Insert(const cpp_tokent &token)
Definition: cpp_token_buffer.cpp:118
cpp_token_buffert::current_pos
post current_pos
Definition: cpp_token_buffer.h:60
cpp_token_buffer.h
parsert::get_file
irep_idt get_file() const
Definition: parser.h:92
yyansi_clex
int yyansi_clex()
parsert::stack
std::vector< exprt > stack
Definition: parser.h:30
cpp_token_buffert::Save
post Save()
Definition: cpp_token_buffer.cpp:98
cpp_token_buffert::post
unsigned int post
Definition: cpp_token_buffer.h:28
cpp_token_buffert::Restore
void Restore(post pos)
Definition: cpp_token_buffer.cpp:103
ansi_c_parser.h
cpp_token_buffert::get_token
int get_token()
Definition: cpp_token_buffer.cpp:42
parsert::get_line_no
unsigned get_line_no() const
Definition: parser.h:97
cpp_token_buffert::token_vector
std::vector< tokenst::iterator > token_vector
Definition: cpp_token_buffer.h:58
cpp_token_buffert::read_token
void read_token()
Definition: cpp_token_buffer.cpp:73