77
88 type cmd =
99 | File_exists of path
10+ | Is_directory of path
1011 | Mkdir of path * string
1112 | Rmdir of path * string
1213 | Readdir of path
7273 QCheck. make ~print: show_cmd
7374 Gen. (oneof [
7475 map (fun path -> File_exists path) (path_gen s);
76+ map (fun path -> Is_directory path) (path_gen s);
7577 map (fun (path ,new_dir_name ) -> Mkdir (path, new_dir_name)) (pair_gen s);
7678 map (fun (path ,delete_dir_name ) -> Rmdir (path, delete_dir_name)) (pair_gen s);
7779 map (fun path -> Readdir path) (path_gen s);
@@ -169,6 +171,7 @@ struct
169171 if mem_model fs (path @ [new_dir_name])
170172 then fs
171173 else mkdir_model fs path new_dir_name
174+ | Is_directory _path -> fs
172175 | Rmdir (path ,delete_dir_name ) ->
173176 if mem_model fs (path @ [delete_dir_name])
174177 then rmdir_model fs path delete_dir_name
@@ -200,6 +203,7 @@ struct
200203 let run c _file_name =
201204 match c with
202205 | File_exists path -> Res (bool , Sys. file_exists (p path))
206+ | Is_directory path -> Res (result bool exn , protect Sys. is_directory (p path))
203207 | Mkdir (path , new_dir_name ) ->
204208 Res (result unit exn , protect (Sys. mkdir ((p path) / new_dir_name)) 0o755 )
205209 | Rmdir (path , delete_dir_name ) ->
@@ -216,9 +220,25 @@ struct
216220 | None -> false
217221 | Some target_fs -> fs_is_a_dir target_fs
218222
223+ let rec path_prefixes path = match path with
224+ | [] -> []
225+ | [_] -> []
226+ | n ::ns -> [n]::(List. map (fun p -> n::p) (path_prefixes ns))
227+
219228 let postcond c (fs : filesys ) res =
220229 match c, res with
221230 | File_exists path , Res ((Bool,_ ),b ) -> b = mem_model fs path
231+ | Is_directory path , Res ((Result (Bool,Exn),_ ),res ) ->
232+ (match res with
233+ | Ok b ->
234+ (match find_opt_model fs path with
235+ | Some (Directory _ ) -> b = true
236+ | Some File -> b = false
237+ | None -> false )
238+ | Error (Sys_error s ) ->
239+ (s = (p path) ^ " : No such file or directory" && find_opt_model fs path = None ) ||
240+ (s = p path ^ " : Not a directory" && List. exists (fun pref -> Some File = find_opt_model fs pref) (path_prefixes path))
241+ | _ -> false )
222242 | Mkdir (path , new_dir_name ), Res ((Result (Unit,Exn),_ ), res ) ->
223243 let complete_path = (path @ [new_dir_name]) in
224244 (match res with
0 commit comments