From 539addf1deb2833d27187fec26c62569d587dc0c Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 6 Sep 2018 13:20:59 -0700 Subject: [PATCH] Biabduction state: option for last_node Summary: Using a dummy node here made the whole reporting wrong because it didn't fail getting a `node_key` when reporting issues from checkers not using the biabduction state. Now that it's fixed, let's fail hard if someone ever tries again. Reviewed By: jeremydubreil Differential Revision: D9654137 fbshipit-source-id: c00273e53 --- infer/src/backend/errdesc.ml | 12 ++++++------ infer/src/backend/exe_env.ml | 4 ++-- infer/src/backend/reporting.ml | 8 ++++---- infer/src/biabduction/Abs.ml | 2 +- infer/src/biabduction/BuiltinDefn.ml | 2 +- infer/src/biabduction/Prover.ml | 2 +- infer/src/biabduction/Rearrange.ml | 20 ++++++++++--------- infer/src/biabduction/RetainCycles.ml | 4 ++-- infer/src/biabduction/State.ml | 28 +++++++++++++-------------- infer/src/biabduction/State.mli | 4 ++-- infer/src/biabduction/SymExec.ml | 18 +++++++++-------- infer/src/biabduction/Tabulation.ml | 8 ++++---- infer/src/biabduction/Timeout.ml | 2 +- infer/src/biabduction/interproc.ml | 2 +- 14 files changed, 59 insertions(+), 57 deletions(-) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 35802a3fd..a7d6e4c9d 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -462,8 +462,8 @@ let find_typ_without_ptr prop pvar = If there is an alloc attribute, print the function call and line number. *) let explain_leak tenv hpred prop alloc_att_opt bucket = let instro = State.get_instr () in - let loc = State.get_loc () in - let node = State.get_node () in + let loc = State.get_loc_exn () in + let node = State.get_node_exn () in let node_instrs = Procdesc.Node.get_instrs node in let hpred_typ_opt = find_hpred_typ hpred in let value_str_from_pvars_vpath pvars vpath = @@ -513,7 +513,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = L.d_str "explain_leak: current instruction is Nullify for pvar " ; Pvar.d pvar ; L.d_ln () ) ; - match exp_lv_dexp tenv (State.get_node ()) (Exp.Lvar pvar) with + match exp_lv_dexp tenv (State.get_node_exn ()) (Exp.Lvar pvar) with | Some de when not (DExp.has_tmp_var de) -> Some (DExp.to_string de) | _ -> @@ -989,7 +989,7 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa | _ -> None in - let node = State.get_node () in + let node = State.get_node_exn () in match find_exp_dereferenced () with | None -> if verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None" ; @@ -1041,8 +1041,8 @@ let dexp_apply_pvar_off dexp pvar_off = (** Produce a description of the nth parameter of the function call, if the current instruction is a function call with that parameter *) let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n pvar_off = - let node = State.get_node () in - let loc = State.get_loc () in + let node = State.get_node_exn () in + let loc = State.get_loc_exn () in match State.get_instr () with | Some (Sil.Call (_, _, args, _, _)) -> ( try diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index 96cc48b24..f4d411b2d 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -91,12 +91,12 @@ let get_tenv exe_env proc_name = | Some tenv -> tenv | None -> - let loc = State.get_loc () in + let loc = State.get_loc_exn () in L.(die InternalError) "get_tenv: tenv not found for %a in file '%a' at %a" Typ.Procname.pp proc_name SourceFile.pp loc.Location.file Location.pp loc ) | None -> - let loc = State.get_loc () in + let loc = State.get_loc_exn () in L.(die InternalError) "get_tenv: file_data not found for %a in file '%a' at %a" Typ.Procname.pp proc_name SourceFile.pp loc.Location.file Location.pp loc ) diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml index 68464ea9e..5e032e931 100644 --- a/infer/src/backend/reporting.ml +++ b/infer/src/backend/reporting.ml @@ -53,11 +53,11 @@ let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn = match Summary.get proc_name with | Some summary -> let node = - let node = match node with None -> State.get_node () | Some node -> node in + let node = match node with None -> State.get_node_exn () | Some node -> node in Errlog.BackendNode {node} in let session = State.get_session () in - let loc = match loc with None -> State.get_loc () | Some loc -> loc in + let loc = match loc with None -> State.get_loc_exn () | Some loc -> loc in let ltr = match ltr with None -> State.get_loc_trace () | Some ltr -> ltr in log_issue_from_summary severity summary ~node ~session ~loc ~ltr exn | None -> @@ -85,9 +85,9 @@ let log_issue_external procname severity ~loc ~ltr ?access issue_type error_mess let log_error_using_state summary exn = - let node = Errlog.BackendNode {node= State.get_node ()} in + let node = Errlog.BackendNode {node= State.get_node_exn ()} in let session = State.get_session () in - let loc = State.get_loc () in + let loc = State.get_loc_exn () in let ltr = State.get_loc_trace () in log_issue_from_summary Exceptions.Error summary ~node ~session ~loc ~ltr ?access:None exn diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml index 1bfb8be63..7d0b8cdcc 100644 --- a/infer/src/biabduction/Abs.ml +++ b/infer/src/biabduction/Abs.ml @@ -975,7 +975,7 @@ let check_observer_is_unsubscribed_deallocation tenv prop e = | _ -> None in - let loc = State.get_loc () in + let loc = State.get_loc_exn () in match Attribute.get_observer tenv prop e with | Some (Apred (Aobserver, _)) -> ( match pvar_opt with diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index af0e3cb3b..1e3d93d20 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -31,7 +31,7 @@ let mk_empty_array len = Sil.Earray (len, [], Sil.inst_none) it requires that the function is called with the array allocated. If not infer return a null pointer deref *) let mk_empty_array_rearranged len = - Sil.Earray (len, [], Sil.inst_rearrange true (State.get_loc ()) (State.get_path_pos ())) + Sil.Earray (len, [], Sil.inst_rearrange true (State.get_loc_exn ()) (State.get_path_pos ())) let extract_array_type typ = diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 252429755..3f925171a 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -883,7 +883,7 @@ let check_atom tenv prop a0 = if Config.smt_output then ( let key = get_smt_key a prop_no_fp in let key_filename = - let source = (State.get_loc ()).file in + let source = (State.get_loc_exn ()).file in DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) [key ^ ".cns"] in let outc = Out_channel.create (DB.filename_to_string key_filename) in diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index b17ec3cdd..f946904a4 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -140,7 +140,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp | [] -> ([], Sil.Earray (len, [], inst), t) | Sil.Off_index e :: off' -> - bounds_check tenv pname orig_prop len e (State.get_loc ()) ; + bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ; let atoms', se', res_t' = create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst in @@ -269,7 +269,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp | ( Off_index e :: off' , Sil.Earray (len, esel, inst_arr) , Tarray {elt= typ'; length= len_for_typ'; stride} ) -> ( - bounds_check tenv pname orig_prop len e (State.get_loc ()) ; + bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ; match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with | Some (_, se') -> let atoms_se_typ_list' = @@ -452,7 +452,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst : L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ; let deref_str = Localise.deref_str_dangling None in let err_desc = - Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc ()) + Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc_exn ()) in raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) ) ; let off_foot, eqs = laundry_offset_for_footprint max_stamp off in @@ -892,7 +892,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc = false in let warn accessed_fld guarded_by_str = - let loc = State.get_loc () in + let loc = State.get_loc_exn () in let err_desc = Localise.desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc in let exn = Exceptions.Unsafe_guarded_by_access (err_desc, __POS__) in Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn @@ -1336,7 +1336,7 @@ let check_type_size tenv pname prop texp off typ_from_instr = && not (Prover.check_type_size_leq typ_from_instr typ_of_object) then let deref_str = Localise.deref_str_pointer_size_mismatch typ_from_instr typ_of_object in - let loc = State.get_loc () in + let loc = State.get_loc_exn () in let exn = Exceptions.Pointer_size_mismatch (Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__) @@ -1630,7 +1630,9 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = match attribute_opt with | Some (Apred (Adangling dk, _)) -> let deref_str = Localise.deref_str_dangling (Some dk) in - let err_desc = Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc ()) in + let err_desc = + Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc_exn ()) + in raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__)) | Some (Apred (Aundef _, _)) -> () @@ -1670,7 +1672,7 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc = (* when e is a temp var, try to find the pvar defining e*) match e with | Exp.Var id -> ( - match Errdesc.find_ident_assignment (State.get_node ()) id with + match Errdesc.find_ident_assignment (State.get_node_exn ()) id with | Some (_, e') -> e' | None -> @@ -1682,7 +1684,7 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc = (* Exp called in the block's function call*) match State.get_instr () with | Some (Sil.Call (_, Exp.Var id, _, _, _)) -> - Errdesc.find_ident_assignment (State.get_node ()) id + Errdesc.find_ident_assignment (State.get_node_exn ()) id | _ -> None in @@ -1761,7 +1763,7 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc : Prop.d_prop prop ; L.d_ln () ; L.d_ln () ; - if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc ()) ; + if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc_exn ()) ; let pname = Procdesc.get_proc_name pdesc in let prop' = match pname with diff --git a/infer/src/biabduction/RetainCycles.ml b/infer/src/biabduction/RetainCycles.ml index c6ff51d27..1dd841e88 100644 --- a/infer/src/biabduction/RetainCycles.ml +++ b/infer/src/biabduction/RetainCycles.ml @@ -12,7 +12,7 @@ let desc_retain_cycle tenv (cycle : RetainCyclesType.t) = Logging.d_strln "Proposition with retain cycle:" ; let do_edge index_ edge = let index = index_ + 1 in - let node = State.get_node () in + let node = State.get_node_exn () in let from_exp_str edge_obj = let type_str = let typ_str = Typ.to_string edge_obj.rc_from.rc_node_typ in @@ -229,7 +229,7 @@ let exn_retain_cycle tenv cycle = Utils.create_dir rc_dotty_dir ; let rc_dotty_file = Filename.temp_file ~in_dir:rc_dotty_dir "rc" ".dot" in RetainCyclesType.write_dotty_to_file rc_dotty_file cycle ) ; - let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) (Some cycle_dotty) in + let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc_exn ()) (Some cycle_dotty) in Exceptions.Retain_cycle (desc, __POS__) diff --git a/infer/src/biabduction/State.ml b/infer/src/biabduction/State.ml index 9ec75ee21..a33d8aee7 100644 --- a/infer/src/biabduction/State.ml +++ b/infer/src/biabduction/State.ml @@ -31,7 +31,7 @@ type t = ; mutable diverging_states_proc: Paths.PathSet.t (** Diverging states since the last reset for the procedure *) ; mutable last_instr: Sil.instr option (** Last instruction seen *) - ; mutable last_node: Procdesc.Node.t (** Last node seen *) + ; mutable last_node: Procdesc.Node.t option (** Last node seen *) ; mutable last_path: (Paths.Path.t * PredSymb.path_pos option) option (** Last path seen *) ; mutable last_prop_tenv_pdesc: (Prop.normal Prop.t * Tenv.t * Procdesc.t) option (** Last prop,tenv,pdesc seen *) @@ -42,7 +42,7 @@ let initial () = { diverging_states_node= Paths.PathSet.empty ; diverging_states_proc= Paths.PathSet.empty ; last_instr= None - ; last_node= Procdesc.Node.dummy None + ; last_node= None ; last_path= None ; last_prop_tenv_pdesc= None ; last_session= 0 @@ -84,15 +84,15 @@ let get_diverging_states_proc () = !gs.diverging_states_proc let get_instr () = !gs.last_instr -let get_loc () = +let get_node_exn () = Option.value_exn !gs.last_node + +let get_loc_exn () = match !gs.last_instr with | Some instr -> Sil.instr_get_loc instr | None -> - Procdesc.Node.get_loc !gs.last_node - + get_node_exn () |> Procdesc.Node.get_loc -let get_node () = !gs.last_node (** normalize the list of instructions by renaming let-bound ids *) let instrs_normalize instrs = @@ -159,17 +159,15 @@ let mk_find_duplicate_nodes : Procdesc.t -> Procdesc.Node.t -> Procdesc.NodeSet. find_duplicate_nodes -let get_node_id () = Procdesc.Node.get_id !gs.last_node - let get_inst_update pos = - let loc = get_loc () in + let loc = get_loc_exn () in Sil.inst_update loc pos let get_path () = match !gs.last_path with | None -> - (Paths.Path.start !gs.last_node, None) + (Paths.Path.start (get_node_exn ()), None) | Some (path, pos_opt) -> (path, pos_opt) @@ -220,7 +218,7 @@ let get_path_pos () = | None -> Typ.Procname.from_string_c_fun "unknown_procedure" in - let nid = get_node_id () in + let nid = Procdesc.Node.get_id (get_node_exn ()) in (pname, (nid :> int)) @@ -239,13 +237,13 @@ let mark_execution_end node = let mark_instr_ok () = - let fs = get_failure_stats (get_node ()) in + let fs = get_failure_stats (get_node_exn ()) in fs.instr_ok <- fs.instr_ok + 1 let mark_instr_fail exn = - let loc = get_loc () in - let node = get_node () in + let loc = get_loc_exn () in + let node = get_node_exn () in let session = get_session () in let loc_trace = get_loc_trace () in let fs = get_failure_stats node in @@ -285,7 +283,7 @@ let set_prop_tenv_pdesc prop tenv pdesc = !gs.last_prop_tenv_pdesc <- Some (prop let set_node (node : Procdesc.Node.t) = !gs.last_instr <- None ; - !gs.last_node <- node + !gs.last_node <- Some node let set_session (session : int) = !gs.last_session <- session diff --git a/infer/src/biabduction/State.mli b/infer/src/biabduction/State.mli index 2589365ee..c61f11d65 100644 --- a/infer/src/biabduction/State.mli +++ b/infer/src/biabduction/State.mli @@ -28,13 +28,13 @@ val get_inst_update : PredSymb.path_pos -> Sil.inst val get_instr : unit -> Sil.instr option (** Get last instruction seen in symbolic execution *) -val get_loc : unit -> Location.t +val get_loc_exn : unit -> Location.t (** Get last location seen in symbolic execution *) val get_loc_trace : unit -> Errlog.loc_trace (** Get the location trace of the last path seen in symbolic execution *) -val get_node : unit -> Procdesc.Node.t +val get_node_exn : unit -> Procdesc.Node.t (** Get last node seen in symbolic execution *) val get_normalized_pre : diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index ef33b5722..3793cd5a0 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -416,14 +416,16 @@ let check_constant_string_dereference lexp = let check_arith_norm_exp tenv pname exp prop = match Attribute.find_arithmetic_problem tenv (State.get_path_pos ()) prop exp with | Some (Attribute.Div0 div), prop' -> - let desc = Errdesc.explain_divide_by_zero tenv div (State.get_node ()) (State.get_loc ()) in + let desc = + Errdesc.explain_divide_by_zero tenv div (State.get_node_exn ()) (State.get_loc_exn ()) + in let exn = Exceptions.Divide_by_zero (desc, __POS__) in Reporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ; (Prop.exp_normalize_prop tenv prop exp, prop') | Some (Attribute.UminusUnsigned (e, typ)), prop' -> let desc = - Errdesc.explain_unary_minus_applied_to_unsigned_expression tenv e typ (State.get_node ()) - (State.get_loc ()) + Errdesc.explain_unary_minus_applied_to_unsigned_expression tenv e typ + (State.get_node_exn ()) (State.get_loc_exn ()) in let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in Reporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ; @@ -480,8 +482,8 @@ let check_already_dereferenced tenv pname cond prop = match dereferenced_line with | Some (id, (n, _)) -> let desc = - Errdesc.explain_null_test_after_dereference tenv (Exp.Var id) (State.get_node ()) n - (State.get_loc ()) + Errdesc.explain_null_test_after_dereference tenv (Exp.Var id) (State.get_node_exn ()) n + (State.get_loc_exn ()) in let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in Reporting.log_issue_deprecated_using_state Exceptions.Warning pname exn @@ -1299,7 +1301,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) in match Prop.exp_normalize_prop tenv Prop.prop_emp cond with | Exp.Const (Const.Cint i) when report_condition_always_true_false i -> - let node = State.get_node () in + let node = State.get_node_exn () in let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in let exn = Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) @@ -1870,7 +1872,7 @@ and proc_call ?dynamic_dispatch exe_env callee_summary | (e, t_e) :: etl', _ :: tl' -> (e, t_e) :: comb etl' tl' | _, [] -> - Errdesc.warning_err (State.get_loc ()) + Errdesc.warning_err (State.get_loc_exn ()) "likely use of variable-arguments function, or function prototype missing@." ; L.d_warning "likely use of variable-arguments function, or function prototype missing" ; L.d_ln () ; @@ -1961,7 +1963,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr let instr_is_abstraction = function Sil.Abstract _ -> true | _ -> false in Instrs.exists ~f:instr_is_abstraction (ProcCfg.Exceptional.instrs node) in - let curr_node = State.get_node () in + let curr_node = State.get_node_exn () in match ProcCfg.Exceptional.Node.kind curr_node with | Procdesc.Node.Prune_node _ when not (node_has_abstraction curr_node) -> (* don't check for leaks in prune nodes, unless there is abstraction anyway,*) diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index c50ee01e4..52c73a626 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -367,7 +367,7 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo let desc use_buckets deref_str = let error_desc = Errdesc.explain_dereference_as_caller_expression caller_pname tenv ~use_buckets deref_str - actual_pre spec_pre e (State.get_node ()) (State.get_loc ()) formal_params + actual_pre spec_pre e (State.get_node_exn ()) (State.get_loc_exn ()) formal_params in L.d_strln_color Red "found error in dereference" ; L.d_strln "spec_pre:" ; @@ -459,7 +459,7 @@ let check_path_errors_in_post tenv caller_pname post post_path = | Sil.Apred (Adiv0 path_pos, [e]) -> if Prover.check_zero tenv e then ( let desc = - Errdesc.explain_divide_by_zero tenv e (State.get_node ()) (State.get_loc ()) + Errdesc.explain_divide_by_zero tenv e (State.get_node_exn ()) (State.get_loc_exn ()) in let new_path, path_pos_opt = let current_path, _ = State.get_path () in @@ -1057,8 +1057,8 @@ let inconsistent_actualpre_missing tenv actual_pre split_opt = let class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc = let desc = - Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp (State.get_node ()) - (State.get_loc ()) + Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp (State.get_node_exn ()) + (State.get_loc_exn ()) in Exceptions.Class_cast_exception (desc, ml_loc) diff --git a/infer/src/biabduction/Timeout.ml b/infer/src/biabduction/Timeout.ml index dfac20527..86b8226a6 100644 --- a/infer/src/biabduction/Timeout.ml +++ b/infer/src/biabduction/Timeout.ml @@ -117,5 +117,5 @@ let exe_timeout f x = None ) ~finally:resume_previous_timeout with SymOp.Analysis_failure_exe kind -> - Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ; + Errdesc.warning_err (State.get_loc_exn ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ; Some kind diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 6c84402e8..f1bf682eb 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -283,7 +283,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then ( - Errdesc.warning_err (State.get_loc ()) "Propagating Divergence@." ; + Errdesc.warning_err (State.get_loc_exn ()) "Propagating Divergence@." ; let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in let diverging_states = State.get_diverging_states_node () in let prop_incons =