Skip to content

Commit ad8870d

Browse files
fix(mcp): apply sync transfer to split paths created during sync
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/351c80a9-dc9f-4603-a357-a186a213399d Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
1 parent b992f66 commit ad8870d

1 file changed

Lines changed: 13 additions & 4 deletions

File tree

src/analyses/mCP.ml

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -173,13 +173,13 @@ struct
173173
in
174174
iter (uncurry side_one) @@ group_assoc_eq V.equal xs
175175

176-
let rec do_splits man pv (xs:(int * (Obj.t * Events.t list)) list) emits =
176+
let rec do_splits ?(local_tf=Fun.id) man pv (xs:(int * (Obj.t * Events.t list)) list) emits =
177177
let split_one n (d,emits') =
178178
let nv = assoc_replace (n,d) pv in
179179
(* Do split-specific emits before general emits.
180180
[emits] and [do_emits] are in reverse order.
181181
[emits'] is in normal order. *)
182-
man.split (do_emits man (emits @ List.rev emits') nv false) []
182+
man.split (local_tf (do_emits man (emits @ List.rev emits') nv false)) []
183183
in
184184
iter (uncurry split_one) xs
185185

@@ -510,7 +510,7 @@ struct
510510
let d = do_emits man !emits d q in
511511
if q then raise Deadcode else d
512512

513-
let sync (man:(D.t, G.t, C.t, V.t) man) reason =
513+
let rec sync_with_split_tf apply_split_tf (man:(D.t, G.t, C.t, V.t) man) reason =
514514
let spawns = ref [] in
515515
let splits = ref [] in
516516
let sides = ref [] in
@@ -523,10 +523,19 @@ struct
523523
let d, q = map_deadcode f @@ spec_list man.local in
524524
do_sideg man !sides;
525525
do_spawns man !spawns;
526-
do_splits man d !splits !emits;
526+
let local_tf =
527+
if apply_split_tf then
528+
fun d -> sync_with_split_tf false {man with local = d} reason
529+
else
530+
Fun.id
531+
in
532+
do_splits ~local_tf man d !splits !emits;
527533
let d = do_emits man !emits d q in
528534
if q then raise Deadcode else d
529535

536+
and sync (man:(D.t, G.t, C.t, V.t) man) reason =
537+
sync_with_split_tf true man reason
538+
530539
let enter (man:(D.t, G.t, C.t, V.t) man) r f a =
531540
let spawns = ref [] in
532541
let sides = ref [] in

0 commit comments

Comments
 (0)