File tree Expand file tree Collapse file tree 3 files changed +7
-2
lines changed
Expand file tree Collapse file tree 3 files changed +7
-2
lines changed Original file line number Diff line number Diff line change @@ -827,7 +827,7 @@ module Make (S:SemExtra.S) : S with module S = S = struct
827827 | E. IdSome ii ->
828828 fprintf chan " proc:%s poi:%i\\ l"
829829 (Proc. pp ii.A. proc)
830- ii.A. program_order_index
830+ ii.A. static_poi
831831
832832(*
833833 This complex function is not meant to be used directly,
Original file line number Diff line number Diff line change @@ -69,6 +69,7 @@ val same_instance : event -> event -> bool
6969 val same_proc : event -> event -> bool
7070 val same_proc_not_init : event -> event -> bool
7171 val progorder_of : event -> A .program_order_index option
72+ val static_poi : event -> A .program_order_index option
7273
7374(* Is e1 before e2 w.r.t. prog order ? Nothing assumed on e1 and e2 *)
7475 val po_strict : event -> event -> bool
@@ -643,6 +644,10 @@ module Make (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
643644 | IdSome i -> Some i.A. program_order_index
644645 | IdInit |IdSpurious -> None
645646
647+ let static_poi e =
648+ match e.iiid with
649+ | IdSome i -> Some i.A. static_poi
650+ | IdInit | IdSpurious -> None
646651
647652(* ***********************)
648653(* Predicates on events *)
Original file line number Diff line number Diff line change @@ -23,7 +23,7 @@ module Make(S : SemExtra.S) = struct
2323 let by_po =
2424 E.EventSet. fold
2525 (fun e k ->
26- match E. progorder_of e with
26+ match E. static_poi e with
2727 | None -> k
2828 | Some poi ->
2929 let es_poi = IntMap. safe_find [] poi k in
You can’t perform that action at this time.
0 commit comments