@ -33,12 +33,15 @@ let make_unlock = make_lock_action "release" (fun a -> Unlock a)
let make_trylock = make_lock_action " conditionally acquire " ( fun a -> LockedIfTrue a )
let make_trylock = make_lock_action " conditionally acquire " ( fun a -> LockedIfTrue a )
let make_guard_construct procname = function
let make_guard_construct procname = function
| [ _ guard ] ->
(* constructor is called without a mutex *)
NoEffect
| [ guard ; lock ] ->
| [ guard ; lock ] ->
GuardConstruct { guard ; lock ; acquire_now = true }
GuardConstruct { guard ; lock ; acquire_now = true }
| [ guard ; lock ; _ defer_lock ] ->
| [ guard ; lock ; _ defer_lock ] ->
GuardConstruct { guard ; lock ; acquire_now = false }
GuardConstruct { guard ; lock ; acquire_now = false }
| actuals ->
| actuals ->
L . internal_error " Cannot parse guard constructor call %a(%a) " Procname . pp procname
L . internal_error " Cannot parse guard constructor call %a(%a) @\n " Procname . pp procname
( PrettyPrintable . pp_collection ~ pp_item : HilExp . pp )
( PrettyPrintable . pp_collection ~ pp_item : HilExp . pp )
actuals ;
actuals ;
NoEffect
NoEffect
@ -48,7 +51,7 @@ let make_guard_action type_str action procname = function
| [ guard ] ->
| [ guard ] ->
action guard
action guard
| actuals ->
| actuals ->
L . internal_error " Cannot parse guard %s call %a(%a) " type_str Procname . pp procname
L . internal_error " Cannot parse guard %s call %a(%a) @\n " type_str Procname . pp procname
( PrettyPrintable . pp_collection ~ pp_item : HilExp . pp )
( PrettyPrintable . pp_collection ~ pp_item : HilExp . pp )
actuals ;
actuals ;
NoEffect
NoEffect
@ -148,8 +151,8 @@ end = struct
let qname_str = QualifiedCppName . to_qual_string qname in
let qname_str = QualifiedCppName . to_qual_string qname in
match List . find lock_models ~ f : ( fun mdl -> String . equal qname_str mdl . classname ) with
match List . find lock_models ~ f : ( fun mdl -> String . equal qname_str mdl . classname ) with
| None ->
| None ->
L . internal_error " is_recursive_lock_type: Could not find lock type %a@ ." QualifiedCppName . pp
L . internal_error " is_recursive_lock_type: Could not find lock type %a@ \n "
qname ;
QualifiedCppName . pp qname ;
true
true
| Some mdl ->
| Some mdl ->
mdl . recursive
mdl . recursive