diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 5c7480ad74..c497c68191 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -536,6 +536,7 @@ struct
     | `Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask gs st v t description) acc) s empty
     | `Int _ -> empty
     | `Float _ -> empty
+    | `MutexAttr _ -> empty
     | `Thread _ -> empty (* thread IDs are abstract and nothing known can be reached from them *)
     | `JmpBuf _ -> empty (* Jump buffers are abstract and nothing known can be reached from them *)
     | `Mutex -> empty (* mutexes are abstract and nothing known can be reached from them *)
@@ -677,6 +678,7 @@ struct
           ValueDomain.Structs.fold f s (empty, TS.bot (), false)
         | `Int _ -> (empty, TS.bot (), false)
         | `Float _ -> (empty, TS.bot (), false)
+        | `MutexAttr _ -> (empty, TS.bot (), false)
         | `Thread _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
         | `JmpBuf _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
         | `Mutex -> (empty, TS.bot (), false) (* TODO: is this right? *)
@@ -1254,6 +1256,12 @@ struct
       end
     | Q.EvalInt e ->
       query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
+    | Q.EvalMutexAttr e -> begin
+        let e:exp = Lval (Cil.mkMem ~addr:e ~off:NoOffset) in
+        match eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        | `MutexAttr a -> a
+        | v -> MutexAttrDomain.top ()
+      end
     | Q.EvalLength e -> begin
         match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | `Address a ->
@@ -2095,6 +2103,26 @@ struct
         | _ -> ()
       end;
       raise Deadcode
+    | MutexAttrSetType {attr = attr; typ = mtyp}, _ ->
+      begin
+        let get_type lval =
+          let address = eval_lv (Analyses.ask_of_ctx ctx) gs st lval in
+          AD.get_type address
+        in
+        let dst_lval = mkMem ~addr:(Cil.stripCasts attr) ~off:NoOffset in
+        let dest_typ = get_type dst_lval in
+        let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dst_lval in
+        match eval_rv (Analyses.ask_of_ctx ctx) gs st mtyp with
+        | `Int x ->
+          begin
+            match ID.to_int x with
+            | Some z ->
+              if M.tracing then M.tracel "attr" "setting\n";
+              set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (`MutexAttr (ValueDomain.MutexAttr.of_int z))
+            | None -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (`MutexAttr (ValueDomain.MutexAttr.top ()))
+          end
+        | _ -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (`MutexAttr (ValueDomain.MutexAttr.top ()))
+      end
     | Identity e, _ ->
       begin match lv with
         | Some x -> assign ctx x e
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index e3d52a9cc3..61212fa4d0 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -54,6 +54,8 @@ type special =
   | ThreadExit of { ret_val: Cil.exp; }
   | Signal of Cil.exp
   | Broadcast of Cil.exp
+  | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
+  | MutexInit of { mutex:Cil.exp; attr: Cil.exp; }
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
   | Math of { fun_args: math; }
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index e9747f4d7b..dc7dae59e0 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -147,6 +147,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond);
     ("pthread_cond_wait", special [__ "cond" []; __ "mutex" []] @@ fun cond mutex -> Wait {cond; mutex});
     ("pthread_cond_timedwait", special [__ "cond" []; __ "mutex" []; __ "abstime" [r]] @@ fun cond mutex abstime -> TimedWait {cond; mutex; abstime});
+    ("pthread_mutexattr_settype", special [__ "attr" []; __ "type" []] @@ fun attr typ -> MutexAttrSetType {attr; typ});
+    ("pthread_mutex_init", special [__ "mutex" []; __ "attr" []] @@ fun mutex attr -> MutexInit {mutex; attr});
     ("pthread_attr_destroy", unknown [drop "attr" [f]]);
     ("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]);
     ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index d2edeba776..0f636f6f7e 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -1,20 +1,43 @@
-(** May lockset analysis ([maylocks]). *)
-
-(* TODO: unused *)
+(** May lockset analysis and analysis of double locking ([maylocks]). *)
 
 open Analyses
+open GoblintCil
+module LF = LibraryFunctions
 
-module Arg =
+module Arg:LocksetAnalysis.MayArg =
 struct
-  module D = LockDomain.MayLockset
+  module D = LockDomain.MayLocksetNoRW
   module G = DefaultSpec.G
   module V = DefaultSpec.V
 
-  let add ctx l =
-    D.add l ctx.local
+  let add ctx (l,r) =
+    if D.mem l ctx.local then
+      let default () =
+        M.warn ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a (possibly non-recursive) mutex that may be already held";
+        ctx.local
+      in
+      match D.Addr.to_var_offset l with
+      | Some (v,o) ->
+        (let mtype = ctx.ask (Queries.MutexType (v, Lval.OffsetNoIdx.of_offs o)) in
+         match mtype with
+         | `Lifted MutexAttrDomain.MutexKind.Recursive -> ctx.local
+         | `Lifted MutexAttrDomain.MutexKind.NonRec ->
+           M.warn ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a non-recursive mutex that may be already held";
+           ctx.local
+         | _  -> default ())
+      | _ -> default ()
+    else
+      D.add l ctx.local
 
   let remove ctx l =
-    D.remove (l, true) (D.remove (l, false) ctx.local)
+    if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
+    match D.Addr.to_var_offset l with
+    | Some (v,o) ->
+      (let mtype = ctx.ask (Queries.MutexType (v, Lval.OffsetNoIdx.of_offs o)) in
+       match mtype with
+       | `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
+       | _ -> ctx.local (* we cannot remove them here *))
+    | None -> ctx.local (* we cannot remove them here *)
 end
 
 module Spec =
@@ -23,6 +46,17 @@ struct
   let name () = "maylocks"
 
   let exitstate  v = D.top () (* TODO: why? *)
+
+  let return ctx exp fundec =
+    if not (D.is_bot ctx.local) && ThreadReturn.is_current (Analyses.ask_of_ctx ctx) then M.warn "Exiting thread while still holding a mutex!";
+    ctx.local
+
+  let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
+    (match(LF.find f).special args with
+     | ThreadExit _ -> if not @@ D.is_bot ctx.local then M.warn "Exiting thread while still holding a mutex!"
+     | _ -> ())
+    ;
+    ctx.local
 end
 
 let _ =
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 775a0bae5e..88bccd4bbb 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -71,6 +71,7 @@ struct
       D.add l ctx.local
 
     let remove ctx l =
+      if not (D.mem (l,true) ctx.local || D.mem (l,false) ctx.local) then M.warn "unlocking mutex which may not be held";
       D.remove (l, true) (D.remove (l, false) ctx.local)
 
     let remove_all ctx =
@@ -78,6 +79,7 @@ struct
            ctx.emit (MustUnlock m)
          ) (D.export_locks ctx.local); *)
       (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *)
+      M.warn "unlocking unknown mutex which may not be held";
       D.empty ()
   end
   include LocksetAnalysis.MakeMust (Arg)
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
new file mode 100644
index 0000000000..feb7fb413e
--- /dev/null
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -0,0 +1,75 @@
+(** An analysis tracking the type of a mutex. *)
+
+open GoblintCil
+open Analyses
+
+module MAttr = ValueDomain.MutexAttr
+module LF = LibraryFunctions
+
+module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Lattice.Unit =
+struct
+  include Analyses.IdentitySpec
+
+  let name () = "pthreadMutexType"
+  module D = Lattice.Unit
+  module C = Lattice.Unit
+
+  (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
+  module O = Lval.OffsetNoIdx
+
+  module V = struct
+    include Printable.Prod(CilType.Varinfo)(O)
+    let is_write_only _ = false
+  end
+
+  module G = MAttr
+
+  (* transfer functions *)
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    match lval with
+    | (Var v, o) ->
+      (* There's no way to use the PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP etc for accesses via pointers *)
+      let rec helper o t = function
+        | Field ({fname = "__data"; _}, Field ({fname = "__kind"; _}, NoOffset)) when ValueDomain.Compound.is_mutex_type t ->
+          let kind =
+            (match Cil.constFold true rval with
+             | Const (CInt (c, _, _)) -> MAttr.of_int c
+             | _ -> `Top)
+          in
+          ctx.sideg (v,o) kind;
+          ctx.local
+        | Index (i,o') ->
+          let o'' = O.of_offs (`Index (i, `NoOffset)) in
+          helper (O.add_offset o o'') (Cilfacade.typeOffset t (Index (i,NoOffset))) o'
+        | Field (f,o') ->
+          let o'' = O.of_offs (`Field (f, `NoOffset)) in
+          helper (O.add_offset o o'')  (Cilfacade.typeOffset t (Field (f,NoOffset))) o'
+        | NoOffset -> ctx.local
+      in
+      helper `NoOffset v.vtype o
+    | _ -> ctx.local
+
+  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let desc = LF.find f in
+    match desc.special arglist with
+    | MutexInit {mutex = mutex; attr = attr} ->
+      let attr = ctx.ask (Queries.EvalMutexAttr attr) in
+      let mutexes = ctx.ask (Queries.MayPointTo mutex) in
+      (* It is correct to iter over these sets here, as mutexes need to be intialized before being used, and an analysis that detects usage before initialization is a different analysis. *)
+      Queries.LS.iter (function (v, o) -> ctx.sideg (v,O.of_offs o) attr) mutexes;
+      ctx.local
+    | _ -> ctx.local
+
+  let startstate v = D.bot ()
+  let threadenter ctx lval f args = [D.top ()]
+  let threadspawn ctx lval f args fctx = ctx.local
+  let exitstate  v = D.top ()
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.MutexType (v,o) -> (ctx.global (v,o):MutexAttrDomain.t)
+    | _ -> Queries.Result.top q
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 275de3b005..007a73b34c 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -23,7 +23,6 @@ struct
   let should_join = D.equal
 
   (* transfer functions *)
-
   let return ctx (exp:exp option) (f:fundec) : D.t =
     let tid = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     begin match tid with
diff --git a/src/autoTune.ml b/src/autoTune.ml
index 8ad5f8d655..a267c3bf9b 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -204,7 +204,7 @@ let activateLongjmpAnalysesWhenRequired () =
   let isLongjmp = function
     | LibraryDesc.Longjmp _ -> true
     | _ -> false
-in
+  in
   if hasFunction isLongjmp  then (
     print_endline @@ "longjmp -> enabling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\"";
     enableAnalyses longjmpAnalyses;
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 6a4649b002..a107dbf91a 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -43,13 +43,7 @@ struct
       )
   end
 
-  (* TODO: use SetDomain.Reverse *)
-  module ReverseAddrSet = SetDomain.ToppedSet (Lock)
-      (struct let topname = "All mutexes" end)
-
-  module AddrSet = Lattice.Reverse (ReverseAddrSet)
-
-  include AddrSet
+  include SetDomain.Reverse(SetDomain.ToppedSet (Lock) (struct let topname = "All mutexes" end))
 
   let rec may_be_same_offset of1 of2 =
     match of1, of2 with
@@ -62,7 +56,7 @@ struct
 
   let add (addr,rw) set =
     match (Addr.to_var_offset addr) with
-    | Some (_,x) when Offs.is_definite x -> ReverseAddrSet.add (addr,rw) set
+    | Some (_,x) when Offs.is_definite x -> add (addr,rw) set
     | _ -> set
 
   let remove (addr,rw) set =
@@ -73,18 +67,9 @@ struct
       | None -> false
     in
     match (Addr.to_var_offset addr) with
-    | Some (_,x) when Offs.is_definite x -> ReverseAddrSet.remove (addr,rw) set
-    | Some x -> ReverseAddrSet.filter (collect_diff_varinfo_with x) set
-    | _   -> AddrSet.top ()
-
-  let empty = ReverseAddrSet.empty
-  let is_empty = ReverseAddrSet.is_empty
-
-  let filter = ReverseAddrSet.filter
-  let fold = ReverseAddrSet.fold
-  let singleton = ReverseAddrSet.singleton
-  let mem = ReverseAddrSet.mem
-  let exists = ReverseAddrSet.exists
+    | Some (_,x) when Offs.is_definite x -> remove (addr,rw) set
+    | Some x -> filter (collect_diff_varinfo_with x) set
+    | _   -> top ()
 
   let export_locks ls =
     let f (x,_) set = Mutexes.add x set in
@@ -101,6 +86,11 @@ struct
   let bot = Lockset.top
 end
 
+module MayLocksetNoRW =
+struct
+  include PreValueDomain.AD
+end
+
 module Symbolic =
 struct
   (* TODO: use SetDomain.Reverse *)
diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml
index ea4acac920..656797a3b8 100644
--- a/src/cdomains/lval.ml
+++ b/src/cdomains/lval.ml
@@ -443,32 +443,38 @@ struct
   end
 end
 
-(** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *)
-module NormalLatRepr (Idx: IntDomain.Z) =
-struct
-  include NormalLat (Idx)
-
+(* Helper for offsets without abstract values for index offsets, i.e. with unit index offsets.*)
+module NoIdxOffsetBase = struct
   module UnitIdxDomain =
   struct
     include Lattice.Unit
     let equal_to _ _ = `Top
     let to_int _ = None
   end
+
+  let rec of_offs = function
+    | `NoOffset -> `NoOffset
+    | `Field (f,o) -> `Field (f, of_offs o)
+    | `Index (i,o) -> `Index (UnitIdxDomain.top (), of_offs o)
+end
+
+(** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *)
+module NormalLatRepr (Idx: IntDomain.Z) =
+struct
+  include NormalLat (Idx)
+
   (** Representatives for lvalue sublattices as defined by {!NormalLat}. *)
   module R: DisjointDomain.Representative with type elt = t =
   struct
     type elt = t
+    open NoIdxOffsetBase
 
     (* Offset module for representative without abstract values for index offsets, i.e. with unit index offsets.
        Reason: The offset in the representative (used for buckets) should not depend on the integer domains,
        since different integer domains may be active at different program points. *)
     include Normal (UnitIdxDomain)
 
-    let rec of_elt_offset: (fieldinfo, Idx.t) offs -> (fieldinfo, UnitIdxDomain.t) offs =
-      function
-      | `NoOffset -> `NoOffset
-      | `Field (f,o) -> `Field (f, of_elt_offset o)
-      | `Index (_,o) -> `Index (UnitIdxDomain.top (), of_elt_offset o) (* all indices to same bucket *)
+    let of_elt_offset: (fieldinfo, Idx.t) offs -> (fieldinfo, UnitIdxDomain.t) offs = of_offs
 
     let of_elt (x: elt): t = match x with
       | Addr (v, o) -> Addr (v, of_elt_offset o) (* addrs grouped by var and part of offset *)
@@ -628,3 +634,11 @@ struct
     end
     )
 end
+
+module OffsetNoIdx =
+struct
+  include NoIdxOffsetBase
+  include Offset(UnitIdxDomain)
+
+  let name () = "offset without index"
+end
diff --git a/src/cdomains/mutexAttrDomain.ml b/src/cdomains/mutexAttrDomain.ml
new file mode 100644
index 0000000000..76669fa3a0
--- /dev/null
+++ b/src/cdomains/mutexAttrDomain.ml
@@ -0,0 +1,44 @@
+module MutexKind =
+struct
+  include Printable.StdLeaf
+
+  (* NonRec represents any of PTHREAD_MUTEX_ERRORCHECK / PTHREAD_MUTEX_NORMAL / PTHREAD_MUTEX_DEFAULT *)
+  (* Once Goblint supports the notion of failing lock operations, this should be replaced with more precise definitions *)
+  type t = NonRec | Recursive [@@deriving eq, ord, hash, to_yojson]
+  let name () = "mutexKind"
+  let show x = match x with
+    | NonRec -> "fast/error_checking"
+    | Recursive -> "recursive"
+
+  include Printable.SimpleShow (struct
+      type nonrec t = t
+      let show = show
+    end)
+end
+
+include Lattice.Flat(MutexKind) (struct let bot_name = "Uninitialized" let top_name = "Top" end)
+
+(* Needed because OS X is weird and assigns different constants than normal systems... :( *)
+let recursive_int = lazy (
+  let res = ref (Z.of_int 2) in (* Use OS X as the default, it doesn't have the enum *)
+  GoblintCil.iterGlobals !Cilfacade.current_file (function
+      | GEnumTag (einfo, _) ->
+        List.iter (fun (name, exp, _) ->
+            if name = "PTHREAD_MUTEX_RECURSIVE" then
+              res := Option.get @@ GoblintCil.getInteger exp
+          ) einfo.eitems
+      | _ -> ()
+    );
+  !res
+)
+
+
+let of_int z =
+  if Z.equal z Z.zero then
+    `Lifted MutexKind.NonRec
+  else
+    let recursive_int = Lazy.force recursive_int in
+    if Z.equal z recursive_int then
+      `Lifted MutexKind.Recursive
+    else
+      `Top
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 544ac9f27a..7cba43ecc2 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -8,6 +8,7 @@ include PreValueDomain
 module Offs = Lval.OffsetLat (IndexDomain)
 module M = Messages
 module BI = IntOps.BigIntOps
+module MutexAttr = MutexAttrDomain
 module VDQ = ValueDomainQueries
 module LS = VDQ.LS
 module AddrSetDomain = SetDomain.ToppedSet(Addr)(struct let topname = "All" end)
@@ -29,6 +30,7 @@ sig
   val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) ->  t -> t -> t
   val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
   val is_immediate_type: typ -> bool
+  val is_mutex_type: typ -> bool
   val bot_value: ?varAttr:attributes -> typ -> t
   val is_bot_value: t -> bool
   val init_value: ?varAttr:attributes -> typ -> t
@@ -86,6 +88,7 @@ module rec Compound: S with type t = [
     | `Thread of Threads.t
     | `JmpBuf of JmpBufs.t
     | `Mutex
+    | `MutexAttr of MutexAttr.t
     | `Bot
   ] and type offs = (fieldinfo,IndexDomain.t) Lval.offs =
 struct
@@ -101,9 +104,13 @@ struct
     | `Thread of Threads.t
     | `JmpBuf of JmpBufs.t
     | `Mutex
+    | `MutexAttr of MutexAttrDomain.t
     | `Bot
   ] [@@deriving eq, ord, hash]
 
+  let is_mutexattr_type (t:typ): bool = match t with
+    | TNamed (info, attr) -> info.tname = "pthread_mutexattr_t"
+    | _ -> false
 
   let is_mutex_type (t: typ): bool = match t with
     | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t"
@@ -138,6 +145,7 @@ struct
       let len = array_length_idx (IndexDomain.bot ()) length in
       `Array (CArrays.make ~varAttr ~typAttr len (bot_value ai))
     | t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ())
+    | t when is_mutexattr_type t -> `MutexAttr (MutexAttrDomain.bot ())
     | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.Bufs.empty (), false)
     | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t)
     | _ -> `Bot
@@ -154,6 +162,7 @@ struct
     | `Thread x -> Threads.is_bot x
     | `JmpBuf x -> JmpBufs.is_bot x
     | `Mutex -> true
+    | `MutexAttr x -> MutexAttr.is_bot x
     | `Bot -> true
     | `Top -> false
 
@@ -161,6 +170,7 @@ struct
     match t with
     | t when is_mutex_type t -> `Mutex
     | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
+    | t when is_mutexattr_type t -> `MutexAttr (MutexAttrDomain.top ())
     | TInt (ik,_) -> `Int (ID.top_of ik)
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.top_of fkind)
     | TPtr _ -> `Address AD.top_ptr
@@ -179,6 +189,7 @@ struct
     match t with
     | _ when is_mutex_type t -> `Mutex
     | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
+    | t when is_mutexattr_type t -> `MutexAttr (MutexAttrDomain.top ())
     | TInt (ik,_) -> `Int (ID.(cast_to ik (top_of ik)))
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.top_of fkind)
     | TPtr _ -> `Address AD.top_ptr
@@ -202,6 +213,7 @@ struct
     | `Array x -> CArrays.is_top x
     | `Blob x -> Blobs.is_top x
     | `Thread x -> Threads.is_top x
+    | `MutexAttr x -> MutexAttr.is_top x
     | `JmpBuf x -> JmpBufs.is_top x
     | `Mutex -> true
     | `Top -> true
@@ -211,6 +223,7 @@ struct
     match t with
     | _ when is_mutex_type t -> `Mutex
     | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
+    | t when is_mutexattr_type t -> `MutexAttr (MutexAttrDomain.top ())
     | TInt (ikind, _) -> `Int (ID.of_int ikind BI.zero)
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.of_const fkind 0.0)
     | TPtr _ -> `Address AD.null_ptr
@@ -234,7 +247,7 @@ struct
     | _ -> `Top
 
   let tag_name : t -> string = function
-    | `Top -> "Top" | `Int _ -> "Int" | `Float _ -> "Float" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `JmpBuf _ -> "JmpBuf" | `Bot -> "Bot"
+    | `Top -> "Top" | `Int _ -> "Int" | `Float _ -> "Float" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `MutexAttr _ -> "MutexAttr" | `JmpBuf _ -> "JmpBuf" | `Bot -> "Bot"
 
   include Printable.Std
   let name () = "compound"
@@ -259,6 +272,7 @@ struct
     | `Array n ->  CArrays.pretty () n
     | `Blob n ->  Blobs.pretty () n
     | `Thread n -> Threads.pretty () n
+    | `MutexAttr n -> MutexAttr.pretty () n
     | `JmpBuf n -> JmpBufs.pretty () n
     | `Mutex -> text "mutex"
     | `Bot -> text bot_name
@@ -276,6 +290,7 @@ struct
     | `Thread n -> Threads.show n
     | `JmpBuf n -> JmpBufs.show n
     | `Mutex -> "mutex"
+    | `MutexAttr x -> MutexAttr.show x
     | `Bot -> bot_name
     | `Top -> top_name
 
@@ -398,6 +413,7 @@ struct
     | `Bot
     | `Thread _
     | `Mutex
+    | `MutexAttr _
     | `JmpBuf _ ->
       v
     | _ ->
@@ -509,6 +525,7 @@ struct
     | (`Address x, `Thread y) -> true
     | (`JmpBuf x, `JmpBuf y) -> JmpBufs.leq x y
     | (`Mutex, `Mutex) -> true
+    | (`MutexAttr x, `MutexAttr y) -> MutexAttr.leq x y
     | _ -> warn_type "leq" x y; false
 
   let rec join x y =
@@ -542,6 +559,7 @@ struct
       `Thread y (* TODO: ignores address! *)
     | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.join x y)
     | (`Mutex, `Mutex) -> `Mutex
+    | (`MutexAttr x, `MutexAttr y) -> `MutexAttr (MutexAttr.join x y)
     | _ ->
       warn_type "join" x y;
       `Top
@@ -576,6 +594,7 @@ struct
       `Thread y (* TODO: ignores address! *)
     | (`Mutex, `Mutex) -> `Mutex
     | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.widen x y)
+    | (`MutexAttr x, `MutexAttr y) -> `MutexAttr (MutexAttr.widen x y)
     | _ ->
       warn_type "widen" x y;
       `Top
@@ -635,6 +654,7 @@ struct
       `Address x (* TODO: ignores thread! *)
     | (`Mutex, `Mutex) -> `Mutex
     | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.meet x y)
+    | (`MutexAttr x, `MutexAttr y) -> `MutexAttr (MutexAttr.meet x y)
     | _ ->
       warn_type "meet" x y;
       `Bot
@@ -659,6 +679,7 @@ struct
     | (`Thread y, `Address x) ->
       `Address x (* TODO: ignores thread! *)
     | (`Mutex, `Mutex) -> `Mutex
+    | (`MutexAttr x, `MutexAttr y) -> `MutexAttr (MutexAttr.narrow x y)
     | x, `Top | `Top, x -> x
     | x, `Bot | `Bot, x -> `Bot
     | _ ->
@@ -1130,6 +1151,7 @@ struct
     | `Array n ->  CArrays.printXml f n
     | `Blob n ->  Blobs.printXml f n
     | `Thread n -> Threads.printXml f n
+    | `MutexAttr n -> MutexAttr.printXml f n
     | `JmpBuf n -> JmpBufs.printXml f n
     | `Mutex -> BatPrintf.fprintf f "<value>\n<data>\nmutex\n</data>\n</value>\n"
     | `Bot -> BatPrintf.fprintf f "<value>\n<data>\nbottom\n</data>\n</value>\n"
@@ -1144,6 +1166,7 @@ struct
     | `Array n -> CArrays.to_yojson n
     | `Blob n -> Blobs.to_yojson n
     | `Thread n -> Threads.to_yojson n
+    | `MutexAttr n -> MutexAttr.to_yojson n
     | `JmpBuf n -> JmpBufs.to_yojson n
     | `Mutex -> `String "mutex"
     | `Bot -> `String "⊥"
@@ -1198,6 +1221,7 @@ struct
     | `Blob n -> `Blob (Blobs.relift n)
     | `Thread n -> `Thread (Threads.relift n)
     | `JmpBuf n -> `JmpBuf (JmpBufs.relift n)
+    | `MutexAttr n -> `MutexAttr (MutexAttr.relift n)
     | `Mutex -> `Mutex
     | `Bot -> `Bot
     | `Top -> `Top
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 2d1b25eca9..344a3c62ca 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -83,7 +83,9 @@ type _ t =
   | HeapVar: VI.t t
   | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *)
   | IsMultiple: varinfo -> MustBool.t t (* Is no other copy of this local variable reachable via pointers? *)
+  | MutexType: varinfo * Lval.OffsetNoIdx.t -> MutexAttrDomain.t t
   | EvalThread: exp -> ConcDomain.ThreadSet.t t
+  | EvalMutexAttr: exp -> MutexAttrDomain.t t
   | EvalJumpBuf: exp -> JmpBufDomain.JmpBufSet.t t
   | ActiveJumpBuf: JmpBufDomain.ActiveLongjmps.t t
   | ValidLongJmp: JmpBufDomain.JmpBufSet.t t
@@ -132,6 +134,7 @@ struct
     | MustBeUniqueThread -> (module MustBool)
     | EvalInt _ -> (module ID)
     | EvalLength _ -> (module ID)
+    | EvalMutexAttr _ -> (module MutexAttrDomain)
     | EvalValue _ -> (module VD)
     | BlobSize _ -> (module ID)
     | CurrentThreadId -> (module ThreadIdDomain.ThreadLifted)
@@ -143,6 +146,7 @@ struct
     | DYojson -> (module FlatYojson)
     | PartAccess _ -> Obj.magic (module Unit: Lattice.S) (* Never used, MCP handles PartAccess specially. Must still return module (instead of failwith) here, but the module is never used. *)
     | IsMultiple _ -> (module MustBool) (* see https://github.com/goblint/analyzer/pull/310#discussion_r700056687 on why this needs to be MustBool *)
+    | MutexType _ -> (module MutexAttrDomain)
     | EvalThread _ -> (module ConcDomain.ThreadSet)
     | EvalJumpBuf _ -> (module JmpBufDomain.JmpBufSet)
     | ActiveJumpBuf -> (module JmpBufDomain.ActiveLongjmps)
@@ -185,12 +189,14 @@ struct
     | MayBePublicWithout _ -> MayBool.top ()
     | MayBeThreadReturn -> MayBool.top ()
     | IsHeapVar _ -> MayBool.top ()
+    | MutexType _ -> MutexAttrDomain.top ()
     | MustBeProtectedBy _ -> MustBool.top ()
     | MustBeAtomic -> MustBool.top ()
     | MustBeSingleThreaded _ -> MustBool.top ()
     | MustBeUniqueThread -> MustBool.top ()
     | EvalInt _ -> ID.top ()
     | EvalLength _ -> ID.top ()
+    | EvalMutexAttr _ -> MutexAttrDomain.top ()
     | EvalValue _ -> VD.top ()
     | BlobSize _ -> ID.top ()
     | CurrentThreadId -> ThreadIdDomain.ThreadLifted.top ()
@@ -272,6 +278,8 @@ struct
     | Any ActiveJumpBuf -> 46
     | Any ValidLongJmp -> 47
     | Any (MayBeModifiedSinceSetjmp _) -> 48
+    | Any (MutexType _) -> 49
+    | Any (EvalMutexAttr _ ) -> 50
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -292,6 +300,7 @@ struct
       | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2
       | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2
       | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2
+      | Any (EvalMutexAttr e1), Any (EvalMutexAttr e2) -> CilType.Exp.compare e1 e2
       | Any (EvalValue e1), Any (EvalValue e2) -> CilType.Exp.compare e1 e2
       | Any (BlobSize e1), Any (BlobSize e2) -> CilType.Exp.compare e1 e2
       | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2
@@ -312,6 +321,7 @@ struct
       | Any (Invariant i1), Any (Invariant i2) -> compare_invariant_context i1 i2
       | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
+      | Any (MutexType (v1,o1)), Any (MutexType (v2,o2)) -> [%ord: CilType.Varinfo.t * Lval.OffsetNoIdx.t] (v1,o1) (v2,o2)
       | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
       | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
@@ -334,6 +344,7 @@ struct
     | Any (EvalInt e) -> CilType.Exp.hash e
     | Any (EvalStr e) -> CilType.Exp.hash e
     | Any (EvalLength e) -> CilType.Exp.hash e
+    | Any (EvalMutexAttr e) -> CilType.Exp.hash e
     | Any (EvalValue e) -> CilType.Exp.hash e
     | Any (BlobSize e) -> CilType.Exp.hash e
     | Any (CondVars e) -> CilType.Exp.hash e
@@ -347,6 +358,7 @@ struct
     | Any (EvalJumpBuf e) -> CilType.Exp.hash e
     | Any (WarnGlobal vi) -> Hashtbl.hash vi
     | Any (Invariant i) -> hash_invariant_context i
+    | Any (MutexType (v,o)) -> 31*CilType.Varinfo.hash v + Lval.OffsetNoIdx.hash o
     | Any (InvariantGlobal vi) -> Hashtbl.hash vi
     | Any (MustProtectedVars m) -> hash_mustprotectedvars m
     | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e
@@ -400,6 +412,8 @@ struct
     | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _"
     | Any (IterSysVars _) -> Pretty.dprintf "IterSysVars _"
     | Any (InvariantGlobal i) -> Pretty.dprintf "InvariantGlobal _"
+    | Any (MutexType (v,o)) ->  Pretty.dprintf "MutexType _"
+    | Any (EvalMutexAttr a) ->  Pretty.dprintf "EvalMutexAttr _"
     | Any MayAccessed -> Pretty.dprintf "MayAccessed"
     | Any MayBeTainted -> Pretty.dprintf "MayBeTainted"
     | Any DYojson -> Pretty.dprintf "DYojson"
diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml
index ef8ee5d6a9..2cc4553005 100644
--- a/src/util/messageCategory.ml
+++ b/src/util/messageCategory.ml
@@ -12,6 +12,7 @@ type undefined_behavior =
   | NullPointerDereference
   | UseAfterFree
   | Uninitialized
+  | DoubleLocking
   | Other
 [@@deriving eq, ord, hash]
 
@@ -63,6 +64,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
     let other: category = create @@ Other
 
     module ArrayOutOfBounds =
@@ -98,6 +100,7 @@ struct
         | "nullpointer_dereference" -> nullpointer_dereference
         | "use_after_free" -> use_after_free
         | "uninitialized" -> uninitialized
+        | "double_locking" -> double_locking
         | "other" -> other
         | _ -> Unknown
 
@@ -107,6 +110,7 @@ struct
       | NullPointerDereference -> ["NullPointerDereference"]
       | UseAfterFree -> ["UseAfterFree"]
       | Uninitialized -> ["Uninitialized"]
+      | DoubleLocking -> ["DoubleLocking"]
       | Other -> ["Other"]
   end
 
@@ -215,6 +219,7 @@ let behaviorName = function
     |NullPointerDereference -> "NullPointerDereference"
     |UseAfterFree -> "UseAfterFree"
     |Uninitialized -> "Uninitialized"
+    |DoubleLocking -> "DoubleLocking"
     |Other -> "Other"
     | ArrayOutOfBounds aob -> match aob with
       | PastEnd -> "PastEnd"
diff --git a/tests/regression/71-doublelocking/01-simple.c b/tests/regression/71-doublelocking/01-simple.c
new file mode 100644
index 0000000000..f2c961cb63
--- /dev/null
+++ b/tests/regression/71-doublelocking/01-simple.c
@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] 'maylocks'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
+
+void* f1(void* ptr) {
+    int top;
+
+    g = 1;
+    if(top) {
+        pthread_mutex_lock(&mut);
+    }
+    pthread_mutex_lock(&mut); //WARN
+    pthread_mutex_unlock(&mut);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_join(t1, NULL);
+
+    pthread_mutex_lock(&mut); //NOWARN
+    pthread_mutex_unlock(&mut);
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/02-unknown.c b/tests/regression/71-doublelocking/02-unknown.c
new file mode 100644
index 0000000000..9ad70a03b3
--- /dev/null
+++ b/tests/regression/71-doublelocking/02-unknown.c
@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] 'maylocks'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+pthread_mutex_t mut[8];
+
+void* f1(void* ptr) {
+    int top;
+    int x = 2;
+    if(top) {
+        x = 3;
+    }
+
+
+    pthread_mutex_lock(&mut[x]);
+    pthread_mutex_lock(&mut[3]); //WARN
+    pthread_mutex_unlock(&mut[3]);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_join(t1, NULL);
+
+    pthread_mutex_lock(&mut[0]); //NOWARN
+    pthread_mutex_unlock(&mut[0]);
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/03-thread-exit-with-mutex.c b/tests/regression/71-doublelocking/03-thread-exit-with-mutex.c
new file mode 100644
index 0000000000..d71f3fb616
--- /dev/null
+++ b/tests/regression/71-doublelocking/03-thread-exit-with-mutex.c
@@ -0,0 +1,39 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+#include <stdlib.h>
+
+pthread_mutex_t mut[8];
+
+void* f1(void* ptr) {
+    int top;
+    int x = 2;
+    if(top) {
+        x = 3;
+    }
+
+    pthread_mutex_lock(&mut[x]);
+
+    if(top) {
+        pthread_exit(NULL); //WARN
+    }
+
+    return NULL; //WARN
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_join(t1, NULL);
+
+    pthread_mutex_lock(&mut[0]); //NOWARN
+    pthread_mutex_unlock(&mut[0]);
+
+    return 0; // We would actually want to not warn here, but the mutex type analysis is currently too imprecise
+}
diff --git a/tests/regression/71-doublelocking/04-unlock.c b/tests/regression/71-doublelocking/04-unlock.c
new file mode 100644
index 0000000000..1cc5f26654
--- /dev/null
+++ b/tests/regression/71-doublelocking/04-unlock.c
@@ -0,0 +1,35 @@
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mut2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_cond_t cond = PTHREAD_COND_INITIALIZER;
+
+void* f1(void* ptr) {
+    int top;
+
+    pthread_mutex_lock(&mut);
+    pthread_mutex_unlock(&mut2); //WARN
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_join(t1, NULL);
+
+    pthread_mutex_lock(&mut);
+    pthread_mutex_unlock(&mut); //NOWARN
+
+    pthread_cond_wait(&cond,&mut); //WARN
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/05-rec.c b/tests/regression/71-doublelocking/05-rec.c
new file mode 100644
index 0000000000..5bc94dbeda
--- /dev/null
+++ b/tests/regression/71-doublelocking/05-rec.c
@@ -0,0 +1,47 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+
+int g;
+
+pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
+
+#ifndef __APPLE__
+pthread_mutex_t mut2 = PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP;
+#endif
+
+
+void* f1(void* ptr) {
+    int top;
+
+    g = 1;
+    if(top) {
+        pthread_mutex_lock(&mut);
+    }
+    pthread_mutex_lock(&mut); //WARN
+    pthread_mutex_unlock(&mut);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_join(t1, NULL);
+
+#ifndef __APPLE__
+    pthread_mutex_lock(&mut2); //NOWARN
+    pthread_mutex_lock(&mut2); //NOWARN
+    pthread_mutex_unlock(&mut2);
+    pthread_mutex_unlock(&mut2);
+#endif
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/06-rec-dyn.c b/tests/regression/71-doublelocking/06-rec-dyn.c
new file mode 100644
index 0000000000..aed19210c5
--- /dev/null
+++ b/tests/regression/71-doublelocking/06-rec-dyn.c
@@ -0,0 +1,43 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_unlock(mut);
+    pthread_mutex_unlock(mut);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_mutex_t mut;
+
+    pthread_mutexattr_t attr;
+    pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    pthread_mutex_init(&mut, &attr);
+
+
+    pthread_create(&t1,NULL,f1,&mut);
+
+
+    pthread_mutex_lock(&mut); //NOWARN
+    pthread_mutex_lock(&mut); //NOWARN
+    pthread_mutex_unlock(&mut);
+    pthread_mutex_unlock(&mut);
+
+    pthread_join(t1, NULL);
+
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/07-rec-dyn-osx.c b/tests/regression/71-doublelocking/07-rec-dyn-osx.c
new file mode 100644
index 0000000000..bb3cf65657
--- /dev/null
+++ b/tests/regression/71-doublelocking/07-rec-dyn-osx.c
@@ -0,0 +1,103 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// Here, we do not include pthread.h, so MutexAttr.recursive_int remains at `2`, emulating the behavior of OS X.
+#define GOBLINT_NO_PTHREAD_ONCE 1
+typedef signed char __int8_t;
+typedef unsigned char __uint8_t;
+typedef short __int16_t;
+typedef unsigned short __uint16_t;
+typedef int __int32_t;
+typedef unsigned int __uint32_t;
+typedef long long __int64_t;
+typedef unsigned long long __uint64_t;
+typedef long __darwin_intptr_t;
+typedef unsigned int __darwin_natural_t;
+typedef int __darwin_ct_rune_t;
+
+
+struct __darwin_pthread_handler_rec {
+ void (*__routine)(void *);
+ void *__arg;
+ struct __darwin_pthread_handler_rec *__next;
+};
+
+struct _opaque_pthread_attr_t {
+ long __sig;
+ char __opaque[56];
+};
+
+struct _opaque_pthread_mutex_t {
+ long __sig;
+ char __opaque[56];
+};
+
+struct _opaque_pthread_mutexattr_t {
+ long __sig;
+ char __opaque[8];
+};
+
+struct _opaque_pthread_t {
+ long __sig;
+ struct __darwin_pthread_handler_rec *__cleanup_stack;
+ char __opaque[8176];
+};
+
+typedef struct _opaque_pthread_attr_t __darwin_pthread_attr_t;
+typedef struct _opaque_pthread_mutex_t __darwin_pthread_mutex_t;
+typedef struct _opaque_pthread_mutexattr_t __darwin_pthread_mutexattr_t;
+typedef struct _opaque_pthread_t *__darwin_pthread_t;
+
+typedef __darwin_pthread_attr_t pthread_attr_t;
+typedef __darwin_pthread_mutex_t pthread_mutex_t;
+typedef __darwin_pthread_mutexattr_t pthread_mutexattr_t;
+typedef __darwin_pthread_t pthread_t;
+
+int pthread_create(pthread_t _Nullable restrict,
+  const pthread_attr_t * _Nullable restrict,
+  void * ,
+  void *);
+
+int pthread_join(pthread_t , void *);
+int pthread_mutex_init(pthread_mutex_t * restrict, const pthread_mutexattr_t * _Nullable restrict);
+int pthread_mutex_lock(pthread_mutex_t *);
+int pthread_mutex_unlock(pthread_mutex_t *);
+int pthread_mutexattr_destroy(pthread_mutexattr_t *);
+int pthread_mutexattr_init(pthread_mutexattr_t *);
+int pthread_mutexattr_settype(pthread_mutexattr_t *, int);
+
+
+int g;
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut);
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_unlock(mut);
+    pthread_mutex_unlock(mut);
+    return ((void *)0);
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_mutex_t mut;
+
+    pthread_mutexattr_t attr;
+    pthread_mutexattr_settype(&attr, 2);
+    pthread_mutex_init(&mut, &attr);
+
+
+    pthread_create(&t1,((void *)0),f1,&mut);
+
+
+    pthread_mutex_lock(&mut);
+    pthread_mutex_lock(&mut); //NOWARN
+    pthread_mutex_unlock(&mut);
+    pthread_mutex_unlock(&mut);
+
+    pthread_join(t1, ((void *)0));
+
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/08-other-type.c b/tests/regression/71-doublelocking/08-other-type.c
new file mode 100644
index 0000000000..0f4a2f7887
--- /dev/null
+++ b/tests/regression/71-doublelocking/08-other-type.c
@@ -0,0 +1,66 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+
+int g;
+
+pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
+
+#ifndef __APPLE__
+pthread_mutex_t mut2 = PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP;
+pthread_mutex_t mut3 = PTHREAD_ERRORCHECK_MUTEX_INITIALIZER_NP;
+#else
+// OS X does not define PTHREAD_ERRORCHECK_MUTEX_INITIALIZER_NP
+// we thus use the default one there, which should also create warnings
+pthread_mutex_t mut3;
+#endif
+
+
+void* f1(void* ptr) {
+    int top;
+
+    g = 1;
+    if(top) {
+        pthread_mutex_lock(&mut);
+    }
+    pthread_mutex_lock(&mut); //WARN
+    pthread_mutex_unlock(&mut);
+    return NULL;
+}
+
+void* f2(void* ptr) {
+    int top;
+
+    g = 1;
+    if(top) {
+        pthread_mutex_lock(&mut3);
+    }
+    pthread_mutex_lock(&mut3); //WARN
+    pthread_mutex_unlock(&mut3);
+    return NULL;
+}
+
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_create(&t2,NULL,f2,NULL);
+    pthread_join(t1, NULL);
+
+#ifndef __APPLE__
+    pthread_mutex_lock(&mut2); //NOWARN
+    pthread_mutex_lock(&mut2); //NOWARN
+    pthread_mutex_unlock(&mut2); //NOWARN
+    pthread_mutex_unlock(&mut2);
+#endif
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/09-other-dyn.c b/tests/regression/71-doublelocking/09-other-dyn.c
new file mode 100644
index 0000000000..cb4ef064f9
--- /dev/null
+++ b/tests/regression/71-doublelocking/09-other-dyn.c
@@ -0,0 +1,55 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut);
+    pthread_mutex_lock(mut); //WARN
+
+    return NULL;
+}
+
+
+void* f2(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut);
+    pthread_mutex_unlock(mut);
+
+    // To check that this is now actually removed from the may lockset
+    return NULL; //NOWARN
+}
+
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+    pthread_mutex_t mut;
+
+    pthread_mutexattr_t attr;
+    pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_NORMAL);
+    pthread_mutex_init(&mut, &attr);
+
+
+    pthread_create(&t1,NULL,f1,&mut);
+
+
+    pthread_mutex_lock(&mut);
+    pthread_mutex_lock(&mut); //WARN
+
+
+    pthread_join(t1, NULL);
+
+    pthread_create(&t2,NULL,f2,&mut);
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/10-thread-exit-recursive.c b/tests/regression/71-doublelocking/10-thread-exit-recursive.c
new file mode 100644
index 0000000000..f360a98e48
--- /dev/null
+++ b/tests/regression/71-doublelocking/10-thread-exit-recursive.c
@@ -0,0 +1,33 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_unlock(mut);
+    return NULL; //WARN
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_mutex_t mut;
+
+    pthread_mutexattr_t attr;
+    pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    pthread_mutex_init(&mut, &attr);
+
+
+    pthread_create(&t1,NULL,f1,&mut);
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/11-rec-dyn-branch.c b/tests/regression/71-doublelocking/11-rec-dyn-branch.c
new file mode 100644
index 0000000000..4fee99a765
--- /dev/null
+++ b/tests/regression/71-doublelocking/11-rec-dyn-branch.c
@@ -0,0 +1,50 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+// Like 06, but tests mutexattr survives joins
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_unlock(mut);
+    pthread_mutex_unlock(mut);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_mutex_t mut;
+
+    pthread_mutexattr_t attr;
+
+    if(argc == 2) {
+        pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    } else {
+        pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    }
+
+    pthread_mutex_init(&mut, &attr);
+
+
+    pthread_create(&t1,NULL,f1,&mut);
+
+
+    pthread_mutex_lock(&mut); //NOWARN
+    pthread_mutex_lock(&mut); //NOWARN
+    pthread_mutex_unlock(&mut);
+    pthread_mutex_unlock(&mut);
+
+    pthread_join(t1, NULL);
+
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/12-rec-dyn-struct.c b/tests/regression/71-doublelocking/12-rec-dyn-struct.c
new file mode 100644
index 0000000000..bf30db6898
--- /dev/null
+++ b/tests/regression/71-doublelocking/12-rec-dyn-struct.c
@@ -0,0 +1,56 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+// Like 06, but tests mutexattr survives joins
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+struct s {
+    pthread_mutex_t mut;
+};
+
+typedef struct s s_t;
+
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = &(((s_t*) ptr)->mut);
+
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_unlock(mut);
+    pthread_mutex_unlock(mut);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    s_t mut_str;
+
+    pthread_mutexattr_t attr;
+
+    if(argc == 2) {
+        pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    } else {
+        pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    }
+
+    pthread_mutex_init(&mut_str.mut, &attr);
+
+
+    pthread_create(&t1,NULL,f1,&mut_str);
+
+
+    pthread_mutex_lock(&mut_str.mut); //NOWARN
+    pthread_mutex_lock(&mut_str.mut); //NOWARN
+    pthread_mutex_unlock(&mut_str.mut);
+    pthread_mutex_unlock(&mut_str.mut);
+
+    pthread_join(t1, NULL);
+
+
+    return 0;
+}
diff --git a/tests/regression/71-doublelocking/13-rec-struct.c b/tests/regression/71-doublelocking/13-rec-struct.c
new file mode 100644
index 0000000000..272353e33b
--- /dev/null
+++ b/tests/regression/71-doublelocking/13-rec-struct.c
@@ -0,0 +1,53 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+
+int g;
+
+struct s {
+    pthread_mutex_t m;
+};
+
+typedef struct s s_t;
+
+s_t mut = { PTHREAD_MUTEX_INITIALIZER };
+
+#ifndef __APPLE__
+s_t mut2 = { PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP };
+#endif
+
+
+void* f1(void* ptr) {
+    int top;
+
+    g = 1;
+    if(top) {
+        pthread_mutex_lock(&mut.m);
+    }
+    pthread_mutex_lock(&mut.m); //WARN
+    pthread_mutex_unlock(&mut.m);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_join(t1, NULL);
+
+#ifndef __APPLE__
+    pthread_mutex_lock(&mut2.m); //NOWARN
+    pthread_mutex_lock(&mut2.m); //NOWARN
+    pthread_mutex_unlock(&mut2.m);
+    pthread_mutex_unlock(&mut2.m);
+#endif
+
+    return 0;
+}