16
16
| Fill of int * int * char
17
17
| Blit_string of string * int * int * int
18
18
| Index of char
19
+ | Index_opt of char
19
20
| To_seq
20
21
21
22
let pp_cmd par fmt x =
31
32
| Fill (x , y , z ) -> cst3 pp_int pp_int pp_char " Fill" par fmt x y z
32
33
| Blit_string (x , y , z , w ) -> cst4 pp_string pp_int pp_int pp_int " Blit_string" par fmt x y z w
33
34
| Index x -> cst1 pp_char " Index" par fmt x
35
+ | Index_opt x -> cst1 pp_char " Index_opt" par fmt x
34
36
| To_seq -> cst0 " To_seq" fmt
35
37
36
38
let show_cmd = Util.Pp. to_show pp_cmd
64
66
map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen char_gen; (* hack: reusing int_gen for length*)
65
67
map4 (fun src spos dpos l -> Blit_string (src,spos,dpos,l)) string_small int_gen int_gen int_gen; (* hack: reusing int_gen for length*)
66
68
map (fun c -> Index c) char_gen;
69
+ map (fun c -> Index_opt c) char_gen;
67
70
return To_seq ;
68
71
])
69
72
89
92
then List. mapi (fun j c' -> if dpos < = j && j < = dpos+ l-1 then src.[spos+ j- dpos] else c') s
90
93
else s
91
94
| Index _ -> s
95
+ | Index_opt _ -> s
92
96
| To_seq -> s
93
97
94
98
let init_sut () = Bytes. make byte_size 'a'
@@ -108,6 +112,7 @@ struct
108
112
| Fill (i ,l ,c ) -> Res (result unit exn , protect (Bytes. fill b i l) c)
109
113
| Blit_string (src ,spos ,dpos ,l ) -> Res (result unit exn , protect (Bytes. blit_string src spos b dpos) l)
110
114
| Index c -> Res (result int exn , protect (Bytes. index b) c)
115
+ | Index_opt c -> Res (option int , Bytes. index_opt b c)
111
116
| To_seq -> Res (seq char , List. to_seq (List. of_seq (Bytes. to_seq b)))
112
117
113
118
let postcond c (s : char list ) res = match c, res with
@@ -142,6 +147,8 @@ struct
142
147
(match List. find_index (fun c' -> c' = c) s with
143
148
| Some i -> r = Ok i
144
149
| None -> r = Error Not_found )
150
+ | Index_opt c , Res ((Option Int,_ ), r ) ->
151
+ r = List. find_index (fun c' -> c' = c) s
145
152
| To_seq , Res ((Seq Char,_ ),r ) -> Seq. equal (= ) r (List. to_seq s)
146
153
| _ , _ -> false
147
154
end
0 commit comments