|
|
@ -501,13 +501,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
~callee_astate:locks
|
|
|
|
~callee_astate:locks
|
|
|
|
in
|
|
|
|
in
|
|
|
|
let threads =
|
|
|
|
let threads =
|
|
|
|
match (astate.threads, threads) with
|
|
|
|
(* if we know the callee runs on the main thread, assume the caller does too.
|
|
|
|
| _, ThreadsDomain.AnyThreadButSelf | AnyThreadButSelf, _ ->
|
|
|
|
otherwise, keep the caller's thread context *)
|
|
|
|
ThreadsDomain.AnyThreadButSelf
|
|
|
|
match threads with
|
|
|
|
| _, ThreadsDomain.AnyThread ->
|
|
|
|
| ThreadsDomain.AnyThreadButSelf ->
|
|
|
|
astate.threads
|
|
|
|
threads
|
|
|
|
| _ ->
|
|
|
|
| _ ->
|
|
|
|
ThreadsDomain.join threads astate.threads
|
|
|
|
astate.threads
|
|
|
|
in
|
|
|
|
in
|
|
|
|
let accesses =
|
|
|
|
let accesses =
|
|
|
|
add_callee_accesses astate accesses locks threads actuals callee_pname pdesc
|
|
|
|
add_callee_accesses astate accesses locks threads actuals callee_pname pdesc
|
|
|
|