Category for Double Locking

Author: michael-schwarz

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
 

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"

tests/regression/60-doublelocking/05-rec.c

@@ -46,5 +46,4 @@ int main(int argc, char const *argv[])
 
     return 0;
 }
-  }
 #endif