From 02933d81ba5b08ef210a41af8f422922676f0ae2 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 22 Feb 2021 02:36:40 -0800 Subject: [PATCH] [impurity] Suppress internal error with too strong assumption Summary: The impurity checker assumed that in pulse summary, all key addresses of PRE state should exist in POST state. However, the assumption is not always true. For example, ``` void foo(int x) { int y = x; // HERE } ``` At `HERE`, pulse's summary is ``` POST={ roots={ &x=v1 }; mem ={ v1 -> { * -> v4 } }; } PRE={ roots={ &x=v1 }; mem ={ v1 -> { * -> v4 }, v4 -> { } }; } ``` The `v4` entry exists only at `PRE`. Although the `v4` entry is luckily removed in the summary by the canonicalization in this example, basically there is no guarantee about the entry sets of PRE and POST. Reviewed By: jvillard Differential Revision: D26550338 fbshipit-source-id: 99a31cd43 --- infer/src/checkers/impurity.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 341249e9e..b9bf8abc9 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -84,12 +84,12 @@ let add_to_modified pname ~pvar ~access ~addr pre_heap post modified_vars = | None, None -> aux (access_list, modified_vars) ~addr_to_explore ~visited | Some _, None -> - L.die InternalError - "It is unexpected to have an address which has a binding in pre but not in post!@\n\ - %a is in the pre but not the post of the call to %a@\n\ + L.debug Analysis Verbose + "%a is in the pre but not the post of the call to %a@\n\ callee heap pre: @[%a@]@\n\ callee post: @[%a@]@\n" - AbstractValue.pp addr Procname.pp pname BaseMemory.pp pre_heap BaseDomain.pp post + AbstractValue.pp addr Procname.pp pname BaseMemory.pp pre_heap BaseDomain.pp post ; + aux (access_list, modified_vars) ~addr_to_explore ~visited | None, Some (_, attrs_post) -> aux (add_invalid_and_modified ~pvar ~access ~check_empty:false attrs_post access_list