@@ -336,16 +336,18 @@ let every f =
336336let final f =
337337 final_func := f
338338
339+ let print_trace () =
340+ List. iter (fun { proc_id ; op ; obj_ptr } ->
341+ let last_run_ptr = Option. map string_of_int obj_ptr |> Option. value ~default: " " in
342+ Format. printf " Process %d: %s %s@." proc_id (atomic_op_str op) last_run_ptr
343+ ) (List. rev ! schedule_for_checks)
344+
339345let check f =
340346 let tracing_at_start = ! tracing in
341347 tracing := false ;
342348 if not (f () ) then begin
343- Format. printf " @.@.Found assertion violation at run %d:@." ! num_runs;
344- List. iter (fun { proc_id ; op ; obj_ptr } ->
345- let last_run_ptr = Option. map string_of_int obj_ptr |> Option. value ~default: " " in
346- Format. printf " Process %d: %s %s@." proc_id (atomic_op_str op) last_run_ptr
347- ) (List. rev ! schedule_for_checks) ;
348- assert (false )
349+ Format. printf " Check: found assertion violation!@." ;
350+ assert false
349351 end ;
350352 tracing := tracing_at_start
351353
@@ -357,7 +359,12 @@ let trace func =
357359 let empty_state_planned = (IntSet. empty, [] ) in
358360 let empty_clock = IntMap. empty in
359361 let empty_last_access = IntMap. empty, IntMap. empty in
360- explore func 1 empty_state empty_state_planned empty_schedule empty_clock empty_last_access
362+ try explore func 1 empty_state empty_state_planned empty_schedule empty_clock empty_last_access
363+ with exn ->
364+ Format. printf " Found error at run %d:@." ! num_runs;
365+ print_trace () ;
366+ Format. printf " Unhandled exception: %s@." (Printexc. to_string exn ) ;
367+ Printexc. print_backtrace stdout
361368
362369let trace func =
363370 Fun. protect
0 commit comments