File tree Expand file tree Collapse file tree 1 file changed +7
-12
lines changed Expand file tree Collapse file tree 1 file changed +7
-12
lines changed Original file line number Diff line number Diff line change @@ -323,27 +323,22 @@ Function: irep_serializationt::read_gb_string
323
323
irep_idt irep_serializationt::read_gb_string (std::istream &in)
324
324
{
325
325
char c;
326
- size_t i =0 ;
326
+ size_t length =0 ;
327
327
328
328
while ((c = in.get ()) != 0 )
329
329
{
330
- if (i >=read_buffer.size ())
330
+ if (length >=read_buffer.size ())
331
331
read_buffer.resize (read_buffer.size ()*2 , 0 );
332
332
333
333
if (c==' \\ ' ) // escaped chars
334
- read_buffer[i ] = in.get ();
334
+ read_buffer[length ] = in.get ();
335
335
else
336
- read_buffer[i ] = c;
336
+ read_buffer[length ] = c;
337
337
338
- i ++;
338
+ length ++;
339
339
}
340
-
341
- if (i>=read_buffer.size ())
342
- read_buffer.resize (read_buffer.size ()*2 , 0 );
343
-
344
- read_buffer[i] = 0 ;
345
-
346
- return irep_idt (&(read_buffer[0 ]));
340
+
341
+ return irep_idt (std::string (read_buffer.data (), length));
347
342
}
348
343
349
344
/* ******************************************************************\
You can’t perform that action at this time.
0 commit comments