diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 8551e9abb..88d2758fd 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -185,12 +185,6 @@ let pvar_is_cil_tmp pvar = let name = Sil.pvar_to_string pvar in string_is_prefix "_tmp" name -(** Check whether the program variable is a temporary one generated by EDG *) -let pvar_is_edg_tmp pvar = - Sil.pvar_is_local pvar && - let name = Sil.pvar_to_string pvar in - string_is_prefix "__T" name - (** Check whether the program variable is a temporary one generated by sawja *) let pvar_is_sawja_tmp pvar = Sil.pvar_is_local pvar && @@ -199,18 +193,10 @@ let pvar_is_sawja_tmp pvar = string_is_prefix "$T" name || string_is_prefix "$bc" name -let edg_native_tmp_var_name_prefix = "__temp_var_" - -(** Check whether the program variable is a temporary one generated by EDG *) -let pvar_is_edg_tmp pvar = - Sil.pvar_is_local pvar && - let name = Sil.pvar_to_string pvar in - string_is_prefix edg_native_tmp_var_name_prefix name - (** Check whether the program variable is a temporary generated by the front-end *) let pvar_is_frontend_tmp pvar = if !Config.curr_language = Config.Java then pvar_is_sawja_tmp pvar - else pvar_is_cil_tmp pvar || pvar_is_edg_tmp pvar + else pvar_is_cil_tmp pvar (** Find the Letderef instruction used to declare normal variable [id], and return the expression dereferenced to initialize [id] *) diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 8f7d5ab0d..6ec76ce6d 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -126,15 +126,9 @@ val explain_memory_access : Localise.deref_str -> 'a Prop.t -> Location.t -> Loc val explain_null_test_after_dereference : Sil.exp -> Cfg.Node.t -> int -> Location.t -> Localise.error_desc -(** temporary variable name which is used to create edg native temp variables (see Trans_edg) *) -val edg_native_tmp_var_name_prefix : string - (** Check whether the program variable is a temporary one generated by CIL *) val pvar_is_cil_tmp : Sil.pvar -> bool -(** Check whether the program variable is a temporary one generated by EDG *) -val pvar_is_edg_tmp : Sil.pvar -> bool - (** Check whether the program variable is a temporary generated by the front-end *) val pvar_is_frontend_tmp : Sil.pvar -> bool diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 093f7520b..7e01cc98e 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -376,11 +376,6 @@ let check_assignement_guard node = | Sil.Lvar pv -> Errdesc.pvar_is_cil_tmp pv | _ -> false in - let is_edg_tmp e = - match e with - | Sil.Lvar pv -> - Errdesc.pvar_is_edg_tmp pv - | _ -> false in let succs = Cfg.Node.get_succs node in let l_node = Cfg.Node.get_last_loc node in (* e is prune if in all successors prune nodes we have for some temp n$1: *) @@ -436,7 +431,7 @@ let check_assignement_guard node = instr in (match set_instr_at_succs_loc with | [Sil.Set(e, _, _, _)] -> (* we now check if e is the same expression used to prune*) - if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) && not (is_edg_tmp e) then ( + if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) then ( let desc = Errdesc.explain_condition_is_assignment l_node in let exn = Exceptions.Condition_is_assignment (desc, __POS__) in let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in