File tree 1 file changed +31
-1
lines changed 1 file changed +31
-1
lines changed Original file line number Diff line number Diff line change @@ -278,7 +278,37 @@ void show_state_header(
278
278
else
279
279
out << " State " << step_nr;
280
280
281
- out << " " << source_location << " thread " << state.thread_nr << " \n " ;
281
+ if (!source_location.get_file ().empty ())
282
+ {
283
+ out << ' ' ;
284
+ out << source_location.get_file ();
285
+ }
286
+
287
+ if (!source_location.get_line ().empty ())
288
+ {
289
+ out << ' ' ;
290
+ out << source_location.get_line ();
291
+ }
292
+
293
+ if (!source_location.get_function ().empty ())
294
+ {
295
+ out << ' ' ;
296
+
297
+ const symbolt *function_symbol;
298
+ if (ns.lookup (source_location.get_function (), function_symbol))
299
+ out << function_symbol->display_name ();
300
+ else
301
+ out << source_location.get_function ();
302
+ }
303
+
304
+ if (!source_location.get_java_bytecode_index ().empty ())
305
+ {
306
+ out << ' ' ;
307
+ out << source_location.get_java_bytecode_index ();
308
+ }
309
+
310
+ out << " thread " << state.thread_nr << " \n " ;
311
+
282
312
out << " ----------------------------------------------------"
283
313
<< " \n " ;
284
314
You can’t perform that action at this time.
0 commit comments