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
8384 QCheck. make ~print: show_cmd
8485 Gen. (oneof [
8586 map (fun path -> File_exists path) (path_gen s);
87+ map (fun path -> Is_directory path) (path_gen s);
8688 map (fun (path ,new_dir_name ) -> Mkdir (path, new_dir_name)) (pair_gen s);
8789 map (fun (path ,delete_dir_name ) -> Rmdir (path, delete_dir_name)) (pair_gen s);
8890 map (fun path -> Readdir path) (path_gen s);
@@ -180,6 +182,7 @@ struct
180182 if mem_model fs (path @ [new_dir_name])
181183 then fs
182184 else mkdir_model fs path new_dir_name
185+ | Is_directory _path -> fs
183186 | Rmdir (path ,delete_dir_name ) ->
184187 if mem_model fs (path @ [delete_dir_name])
185188 then rmdir_model fs path delete_dir_name
@@ -212,6 +215,7 @@ struct
212215 let run c _file_name =
213216 match c with
214217 | File_exists path -> Res (bool , Sys. file_exists (p path))
218+ | Is_directory path -> Res (result bool exn , protect Sys. is_directory (p path))
215219 | Mkdir (path , new_dir_name ) ->
216220 Res (result unit exn , protect (Sys. mkdir ((p path) / new_dir_name)) 0o755 )
217221 | Rmdir (path , delete_dir_name ) ->
@@ -228,9 +232,25 @@ struct
228232 | None -> false
229233 | Some target_fs -> fs_is_a_dir target_fs
230234
235+ let rec path_prefixes path = match path with
236+ | [] -> []
237+ | [_] -> []
238+ | n ::ns -> [n]::(List. map (fun p -> n::p) (path_prefixes ns))
239+
231240 let postcond c (fs : filesys ) res =
232241 match c, res with
233242 | File_exists path , Res ((Bool,_ ),b ) -> b = mem_model fs path
243+ | Is_directory path , Res ((Result (Bool,Exn),_ ),res ) ->
244+ (match res with
245+ | Ok b ->
246+ (match find_opt_model fs path with
247+ | Some (Directory _ ) -> b = true
248+ | Some File -> b = false
249+ | None -> false )
250+ | Error (Sys_error s ) ->
251+ (s = (p path) ^ " : No such file or directory" && find_opt_model fs path = None ) ||
252+ (s = p path ^ " : Not a directory" && List. exists (fun pref -> Some File = find_opt_model fs pref) (path_prefixes path))
253+ | _ -> false )
234254 | Mkdir (path , new_dir_name ), Res ((Result (Unit,Exn),_ ), res ) ->
235255 let complete_path = (path @ [new_dir_name]) in
236256 (match res with
0 commit comments