[herd] More accurate "Some outcome may be missing" warning

WIP
herd · Oct 4, 2024 · c7dc85f · c7dc85f
1 parent 8e11223
commit c7dc85f
Showing 1 changed file with 12 additions and 8 deletions.
diff --git a/herd/top_herd.ml b/herd/top_herd.ml
@@ -237,9 +237,7 @@ module Make(O:Config)(M:XXXMem.S) =
       let check = check_prop test in
 
       fun conc (st,flts) (set_pp,vbpp) flags c ->
-        if not showcutoff && S.exists_cutoff conc then
-          { c with cutoff = true; }
-        else if do_observed && not (all_observed test conc) then c
+        if do_observed && not (all_observed test conc) then c
         else if
           match O.throughflag with
           | None -> false
@@ -330,7 +328,7 @@ module Make(O:Config)(M:XXXMem.S) =
                 if O.outcomereads then
                   A.LocSet.union (PU.all_regs_that_read conc.S.str) c.reads
                 else c.reads;
-              cutoff =  c.cutoff || S.exists_cutoff conc;
+              cutoff =  c.cutoff;
             } in
           if not O.badexecs && is_bad flags then raise (Over r) ;
           let r = match O.nshow with
@@ -353,6 +351,7 @@ module Make(O:Config)(M:XXXMem.S) =
           cs
           ochan test do_restrict cstr
           conc (st,flts) (set_pp,vbpp) flags c  =
+
       let open S.M.VC in
       match cs with
       | Some (Failed e) ->
@@ -419,13 +418,18 @@ module Make(O:Config)(M:XXXMem.S) =
       end else
         (* Thanks to the existence of check_test, XXMem modules
            apply their internal functors once *)
-        let check_test =
-            M.check_event_structure test in
-        let call_model conc ofail =
+        let call_model conc ofail c =
+        let check_test = M.check_event_structure test in
+        (* Checked pruned executions before even calling model *)
+        let cutoff =  S.exists_cutoff conc in
+        let c = if cutoff then { c with cutoff = true; } else c in
+        (* Discard pruned executions if not explicitely required *)
+        if not showcutoff && cutoff then c
+        else
           check_test
             conc kfail
             (check_failed_model_kont
-               ofail ochan test final_state_restrict_locs cstr) in
+               ofail ochan test final_state_restrict_locs cstr) c in
       let c =
         if O.statelessrc11
         then let module SL = Slrc11.Make(struct include MC let skipchecks = O.skipchecks end) in