diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 0ad9bf91d02..27acd07bbdc 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -9,13 +9,13 @@ struct module G = DefaultSpec.G module V = DefaultSpec.V - let add ctx (l,_) = + let add ctx (l,r) = if D.mem l ctx.local then match D.Addr.to_var_must l with | Some v when ctx.ask (Queries.IsRecursiveMutex v)-> ctx.local | _ -> - (M.warn "double locking"; ctx.local) + (M.warn ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a (possibly non-recursive) mutex that may be already held"; ctx.local) else D.add l ctx.local diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml index 4f61684f563..f0a1d819286 100644 --- a/src/util/messageCategory.ml +++ b/src/util/messageCategory.ml @@ -12,6 +12,7 @@ type undefined_behavior = | NullPointerDereference | UseAfterFree | Uninitialized + | DoubleLocking [@@deriving eq, ord, hash] type behavior = @@ -61,6 +62,7 @@ struct let nullpointer_dereference: category = create @@ NullPointerDereference let use_after_free: category = create @@ UseAfterFree let uninitialized: category = create @@ Uninitialized + let double_locking: category = create @@ DoubleLocking module ArrayOutOfBounds = struct @@ -95,6 +97,7 @@ struct | "nullpointer_dereference" -> nullpointer_dereference | "use_after_free" -> use_after_free | "uninitialized" -> uninitialized + | "double_locking" -> double_locking | _ -> Unknown let path_show (e: t) = @@ -103,6 +106,7 @@ struct | NullPointerDereference -> ["NullPointerDereference"] | UseAfterFree -> ["UseAfterFree"] | Uninitialized -> ["Uninitialized"] + | DoubleLocking -> ["DoubleLocking"] end let from_string_list (s: string list): category = @@ -208,6 +212,7 @@ let behaviorName = function |NullPointerDereference -> "NullPointerDereference" |UseAfterFree -> "UseAfterFree" |Uninitialized -> "Uninitialized" + |DoubleLocking -> "DoubleLocking" | ArrayOutOfBounds aob -> match aob with | PastEnd -> "PastEnd" | BeforeStart -> "BeforeStart"