From f32fcbfbcb187492ef04d53d19893d7711d73d23 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 19 Dec 2024 16:45:58 +0100 Subject: [PATCH] Use equal_idx function --- src/dynarray/stm_tests.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/dynarray/stm_tests.ml b/src/dynarray/stm_tests.ml index ea13ab4c..187b2ba1 100644 --- a/src/dynarray/stm_tests.ml +++ b/src/dynarray/stm_tests.ml @@ -36,6 +36,8 @@ module Dynarray_spec (Elem : Elem) = struct type idx = I of int [@@unboxed] + let equal_idx (I i1) (I i2) = Int.equal i1 i2 + type cmd = | Create | Make of int * elem @@ -354,7 +356,12 @@ module Dynarray_spec (Elem : Elem) = struct | Append_list (arr_i, l) -> update_model arr_i (fun arr -> arr @ l) state | Append (arr_i1, arr_i2) -> - update_model arr_i1 (fun arr -> arr @ get_model arr_i2 state) state + (* "Warning: append a a is a programming error because it iterates on a and + adds elements to it at the same time [...] It fails with Invalid_argument." *) + update_model arr_i1 (fun arr -> arr @ get_model arr_i2 state) state + (* In practice: + Invalid_argument "Dynarray.append: a length change from 3 to 6 occurred during iteration" + and the state change happens *) | Append_seq (arr_i, arr') -> update_model arr_i (fun arr -> arr @ Array.to_list arr') state | Append_iter (arr_i, arr') -> @@ -452,7 +459,7 @@ module Dynarray_spec (Elem : Elem) = struct valid_arr_idx i state && valid_arr_idx j state && (match res with | Ok () -> true - | Error (Invalid_argument _) -> i=j + | Error (Invalid_argument _) -> equal_idx i j | Error _ -> false) | Append_seq (i,_), Res ((Result (Unit, Exn), _), res) -> valid_arr_idx i state && res = Ok () | Append_iter (i,_), Res ((Result (Unit, Exn), _), res) -> valid_arr_idx i state && res = Ok ()