diff options
| -rw-r--r-- | stm/stm.ml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 61b8140ae6..5e453ecfe6 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2729,12 +2729,29 @@ let rec join_admitted_proofs id = join_admitted_proofs view.next | _ -> join_admitted_proofs view.next +(* Error resiliency may have tolerated some broken commands *) +let rec check_no_err_states ~doc visited id = + let open Stateid in + if Set.mem id visited then visited else + match state_of_id ~doc id with + | `Error e -> raise e + | _ -> + let view = VCS.visit id in + match view.step with + | `Qed(_,id) -> + let visited = check_no_err_states ~doc (Set.add id visited) id in + check_no_err_states ~doc visited view.next + | _ -> check_no_err_states ~doc (Set.add id visited) view.next + let join ~doc = let doc = wait ~doc in stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); stm_prerr_endline (fun () -> "Joining Admitted proofs"); join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master); + stm_prerr_endline (fun () -> "Checking no error states"); + ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial) + (VCS.get_branch_pos VCS.Branch.master)); VCS.print (); doc |