diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 942d7a75d4..e4179598fa 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -675,6 +675,8 @@ struct Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) begin match addr with + | UnknownPtr {node = Some node} -> + M.info ~category:Unsound "Unknown mutex (origin: %a) unlocked, relation privatization unsound" Node.pretty node; (* TODO: something more sound *) | UnknownPtr _ -> M.info ~category:Unsound "Unknown mutex unlocked, relation privatization unsound"; (* TODO: something more sound *) | _ -> () diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 2f4b124922..9b1e16d70e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2661,6 +2661,8 @@ struct Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) begin match addr with + | UnknownPtr {node = Some node} -> + M.info ~category:Unsound "Unknown mutex (origin: %a) unlocked, base privatization unsound" Node.pretty node; (* TODO: something more sound *) | UnknownPtr _ -> M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *) | _ -> () diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index e194a2a27c..01a59824b0 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -317,7 +317,7 @@ struct if is_recovered_to_st && not @@ Mutexes.is_top held_weak then Mutexes.iter (fun addr -> ctx.sideg (V.protected addr) protected) held_weak; ) - | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." + | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." (* TODO: show origin *) in let module AD = Queries.AD in let has_escaped g = octx.ask (Queries.MayEscape g) in