File tree 1 file changed +9
-13
lines changed
1 file changed +9
-13
lines changed Original file line number Diff line number Diff line change @@ -290,8 +290,11 @@ std::string string_refinementt::string_of_array
290
290
unsigned n=integer_of_expr (to_constant_expr (size));
291
291
if (n>500 ) return " very long string" ;
292
292
if (n==0 ) return " \"\" " ;
293
- unsigned str[n];
293
+
294
+ std::ostringstream buf;
295
+ buf << " \" " ;
294
296
exprt val=get (arr);
297
+
295
298
if (val.id ()==" array-list" )
296
299
{
297
300
for (size_t i=0 ; i<val.operands ().size ()/2 ; i++)
@@ -301,7 +304,11 @@ std::string string_refinementt::string_of_array
301
304
if (idx<n)
302
305
{
303
306
exprt value=val.operands ()[i*2 +1 ];
304
- str[idx]=integer_of_expr (to_constant_expr (value));
307
+ char c=static_cast <char >(integer_of_expr (to_constant_expr (value)));
308
+ if (31 <c)
309
+ buf << c;
310
+ else
311
+ buf << " ?" ;
305
312
}
306
313
}
307
314
}
@@ -310,17 +317,6 @@ std::string string_refinementt::string_of_array
310
317
return " unable to get array-list" ;
311
318
}
312
319
313
- std::ostringstream buf;
314
- buf << " \" " ;
315
- for (unsigned i=0 ; i<n; i++)
316
- {
317
- char c=static_cast <char >(str[i]);
318
- if (31 <c)
319
- buf << c;
320
- else
321
- buf << " ?" ;
322
- }
323
-
324
320
buf << " \" " ;
325
321
return buf.str ();
326
322
}
You can’t perform that action at this time.
0 commit comments