Skip to content

Commit a6777d9

Browse files
committed
Use event ctx for privatizations instead of octx
1 parent 531a831 commit a6777d9

File tree

2 files changed

+8
-8
lines changed

2 files changed

+8
-8
lines changed

src/analyses/apron/apronAnalysis.apron.ml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -408,16 +408,16 @@ struct
408408
let threadspawn ctx lval f args fctx =
409409
ctx.local
410410

411-
let event ctx e aprx =
411+
let event ctx e octx =
412412
let st = ctx.local in
413413
match e with
414414
| Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
415-
Priv.lock (Analyses.ask_of_ctx aprx) aprx.global st addr
415+
Priv.lock (Analyses.ask_of_ctx octx) octx.global st addr
416416
| Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
417-
Priv.unlock (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st addr
417+
Priv.unlock (Analyses.ask_of_ctx octx) octx.global octx.sideg st addr
418418
(* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *)
419419
| Events.EnterMultiThreaded ->
420-
Priv.enter_multithreaded (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st
420+
Priv.enter_multithreaded (Analyses.ask_of_ctx octx) octx.global octx.sideg st
421421
| _ ->
422422
st
423423

src/analyses/base.ml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2369,13 +2369,13 @@ struct
23692369
match e with
23702370
| Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
23712371
if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr;
2372-
Priv.lock (Analyses.ask_of_ctx octx) (priv_getg octx.global) st addr
2372+
Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr
23732373
| Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
2374-
Priv.unlock (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st addr
2374+
Priv.unlock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr
23752375
| Events.Escape escaped ->
2376-
Priv.escape (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st escaped
2376+
Priv.escape (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped
23772377
| Events.EnterMultiThreaded ->
2378-
Priv.enter_multithreaded (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st
2378+
Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
23792379
| Events.AssignSpawnedThread (lval, tid) ->
23802380
(* TODO: is this type right? *)
23812381
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid))

0 commit comments

Comments
 (0)