<commit_before>(** Deadlock analysis using data race detection. *)

open Cil
open Pretty
open Analyses

module Spec =
struct
  include Analyses.DefaultSpec2

  let name = "Deadlock Checking by Data Race Detection"
  module MSpec = Mutex.Spec
  module D = MSpec.D
  module G = MSpec.G
  module C = MSpec.C
  
  let extra_var = makeGlobalVar "__deadlock_variable" intType
  let gate_var = makeGlobalVar "__gatelock_variable" intType
  
  let init     () = MSpec.init ()
  let finalize () = MSpec.finalize ()
  
  let sync = MSpec.sync

  (* transfer functions *)
  let assign ctx (lval:lval) (rval:exp) : D.t = MSpec.assign ctx lval rval
  let branch ctx (exp:exp) (tv:bool) : D.t = MSpec.branch ctx exp tv 
  let body ctx (f:fundec) : D.t = MSpec.body ctx f
  let return ctx (exp:exp option) (f:fundec) : D.t =  MSpec.return ctx exp f
  let enter ctx (lval: lval option) (f:varinfo) (args:exp list) : (D.t * D.t) list = MSpec.enter ctx lval f args
  let combine ctx (lval:lval option) fexp (f:varinfo) (args:exp list) (au:D.t) : D.t = MSpec.combine ctx lval fexp f args au
  
  let fake_unlock = makeGlobalVar "pthread_mutex_unlock" intType
  
  let add_access may must tid = true
  let add_gatelock may must tid = true
  
  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
    let thread = Obj.obj (List.assoc "thread-id-location") in
    let maylocks = Obj.obj (List.assoc "maylocks") in
    match (LibraryFunctions.classify f.vname arglist, f.vname) with<commit_msg>Fix previous commit.<commit_after>(** Deadlock analysis using data race detection. *)

open Cil
open Pretty
open Analyses

module Spec =
struct
  include Analyses.DefaultSpec2

  let name = "Deadlock Checking by Data Race Detection"
  module MSpec = Mutex.Spec
  module D = MSpec.D
  module G = MSpec.G
  module C = MSpec.C
  
  let extra_var = makeGlobalVar "__deadlock_variable" intType
  let gate_var = makeGlobalVar "__gatelock_variable" intType
  
  let init     () = MSpec.init ()
  let finalize () = MSpec.finalize ()
  
  let sync = MSpec.sync

  (* transfer functions *)
  let assign ctx (lval:lval) (rval:exp) : D.t = MSpec.assign ctx lval rval
  let branch ctx (exp:exp) (tv:bool) : D.t = MSpec.branch ctx exp tv 
  let body ctx (f:fundec) : D.t = MSpec.body ctx f
  let return ctx (exp:exp option) (f:fundec) : D.t =  MSpec.return ctx exp f
  let enter ctx (lval: lval option) (f:varinfo) (args:exp list) : (D.t * D.t) list = MSpec.enter ctx lval f args
  let combine ctx (lval:lval option) fexp (f:varinfo) (args:exp list) (au:D.t) : D.t = MSpec.combine ctx lval fexp f args au
  
  let fake_unlock = makeGlobalVar "pthread_mutex_unlock" intType
  
  let add_access may must tid = true
  let add_gatelock may must tid = true
  
  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
    let thread = Obj.obj (List.assoc "thread-id-location" ctx.presub2) in
    let maylocks = Obj.obj (List.assoc "maylocks" ctx.presub2) in
    match (LibraryFunctions.classify f.vname arglist, f.vname) with
{'fraction_non_alphanumeric': 0.10433918516064922, 'fraction_numerical': 0.001324942033786022, 'mean_word_length': 3.494047619047619, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '342469', 'n_tokens_mistral': 1101, 'n_tokens_neox': 1088, 'n_words': 359}