From 5f9b1805404d384d4c2b1a01c2cd5bb832592d7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 13 Oct 2022 09:41:12 +0200
Subject: [PATCH] [Dive] Avoids using Seq.take, removes it from transitioning.
---
src/libraries/stdlib/transitioning.ml | 15 ++++-----------
src/libraries/stdlib/transitioning.mli | 6 +++---
src/plugins/dive/build.ml | 7 +++----
3 files changed, 10 insertions(+), 18 deletions(-)
diff --git a/src/libraries/stdlib/transitioning.ml b/src/libraries/stdlib/transitioning.ml
index ba4203fb98d..eaab4f83716 100644
--- a/src/libraries/stdlib/transitioning.ml
+++ b/src/libraries/stdlib/transitioning.ml
@@ -62,17 +62,10 @@ module Seq = struct
| Nil -> ys ()
| Cons (x, xt) -> Cons (x, append xt ys)
- let take n xs =
- if n < 0 then invalid_arg "Seq.take";
- let rec aux n xs =
- if n = 0
- then empty
- else fun () ->
- match xs () with
- | Nil -> Nil
- | Cons (x, xs) -> Cons (x, aux (n-1) xs)
- in
- aux n xs
+ let is_empty xs =
+ match xs () with
+ | Nil -> true
+ | Cons _ -> false
let drop n xs =
if n < 0
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index eff4a5548f6..d33ebe8091f 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -46,6 +46,9 @@ end
module Seq: sig
open Stdlib.Seq
+ (** since 4.14.0 *)
+ val is_empty: 'a t -> bool
+
(** since 4.14.0 *)
val mapi: (int -> 'a -> 'b) -> 'a t -> 'b t
@@ -55,9 +58,6 @@ module Seq: sig
(** since 4.11.0 *)
val append : 'a t -> 'a t -> 'a t
- (** since 4.14.0 *)
- val take : int -> 'a t -> 'a t
-
(** since 4.14.0 *)
val drop : int -> 'a t -> 'a t
end
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 993c989e2d4..2bb9dbb53a7 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -183,10 +183,9 @@ let build_node_kind ~is_folded_base lval kinstr =
(* Build a scalar node even if kinstr is dead *)
Scalar (vi, Cil.typeOfLval lval, offset)
| Mem _, _ ->
- match
- enumerate_cells ~is_folded_base lval kinstr |> Seq.take 2 |> List.of_seq
- with
- | [node_kind] -> node_kind
+ let cells_seq = enumerate_cells ~is_folded_base lval kinstr in
+ match cells_seq () with
+ | Seq.Cons (node_kind, seq) when Seq.is_empty seq -> node_kind
| _ -> Scattered (lval, kinstr)
let default_node_locality callstack =
--
GitLab