@@ -24,10 +24,12 @@ struct
2424 type sut = unit
2525
2626 let arb_cmd _s =
27- let str_gen = Gen. (oneofl [" a" ;" b" ;" c" ]) in
28- let path_gen = Gen. (oneofl [[" /root/bbb" ]]) in
29- (* let perm_gen = Gen.map3 (fun d1 d2 d3 -> ( let n = d1*100 + d2*10 + d3*1 in Format.printf "perm generated : %d\n" n; n) ) (Gen.int_bound 7) (Gen.int_bound 7) (Gen.int_bound 7) in *)
30- let perm_gen = Gen. (oneofl [0o777 ]) in
27+ let str_gen = Gen. (oneofl [" a" ; " b" ; " c" ]) in
28+ let name_gen = Gen. (oneofl [" aaa" ; " bbb" ; " ccc" ; " ddd" ; " eee" ]) in
29+ (* let path_gen = Gen.(oneofl [["root"] ; ["root" ; "aaa"] ; ["root" ; "bbb"] ; ["root" ; "b" ; "c" ; "b"]]) in *)
30+ let path_gen = Gen. map (fun path -> " root" :: path) (Gen. list_size (Gen. int_bound 5 ) name_gen) in
31+ let perm_gen = Gen. (oneofl [0o777 ]) in
32+ (* let perm_gen = Gen.map3 (fun d1 d2 d3 -> d1*100 + d2*10 + d3*1) (Gen.int_bound 7) (Gen.int_bound 7) (Gen.int_bound 7) in *)
3133 QCheck. make ~print: show_cmd
3234 Gen. (oneof
3335 [
@@ -38,16 +40,11 @@ struct
3840 let static_path = (Sys. getcwd () ) ^ " /sandbox"
3941
4042 let init_state =
41- Directory {perm = 0o777 ; dir_name = " /root" ; fs_list = [
42- Directory {perm = 0o700 ; dir_name = " aaa" ; fs_list = [] };
43- Directory {perm = 0o000 ; dir_name = " bbb" ; fs_list = [
44- Directory {perm = 0o777 ; dir_name = " lb" ; fs_list = [] }
45- ]}
46- ]}
43+ Directory {perm = 0o777 ; dir_name = " root" ; fs_list = [] }
4744
4845 let rec is_perm_ok (fsl : filesys list ) path =
4946 match fsl with
50- | [] -> false
47+ | [] -> true
5148 | Directory d :: tl -> (match path with
5249 | [] -> true
5350 | hd_path :: tl_path -> if d.dir_name = hd_path
@@ -65,15 +62,17 @@ struct
6562
6663 let rec find (fsl : filesys list ) path name =
6764 match fsl with
68- | [] -> None
65+ | [] ->
66+ (* Format.printf "on a pas trouvé %s\n"name; *)
67+ None
6968 | Directory d :: tl -> (match path with
7069 | [] -> if d.dir_name = name
7170 then Some (Directory d)
7271 else find tl path name
7372 | hd_path :: tl_path -> if d.dir_name = hd_path
7473 then if d.perm > 447
7574 then find d.fs_list tl_path name
76- else ( Format. printf " 2 PERM DENIED \n " ; None )
75+ else None
7776 else find tl path name)
7877 | File f :: _tl -> if path = [] && f.file_name = name
7978 then Some (File f)
@@ -84,11 +83,12 @@ struct
8483 | Directory d :: tl -> (match path with
8584 | hd_path :: tl_path -> if (hd_path = d.dir_name) && (List. length path = 1 )
8685 then (
87- if perm > 447
86+ let b = perm > 447 in
87+ if b
8888 then (
8989 let update = Directory {d with fs_list = (Directory {perm; dir_name; fs_list = [] } :: d.fs_list)} in
9090 update :: [] )
91- else ( Format. printf " 1 PERM DENIED \n " ; Directory d :: [] ) )
91+ else Directory d :: [] )
9292 else if hd_path = d.dir_name
9393 then Directory {d with fs_list = (mkdir d.fs_list tl_path dir_name perm)} :: []
9494 else Directory d :: (mkdir tl path dir_name perm)
@@ -104,42 +104,62 @@ struct
104104
105105 let reset_root path = Sys. command (" rm -r -d -f " ^ path)
106106
107- let init_sut () = try
108- Sys. mkdir (static_path ^ " /root" ) 0o777 ;
109- Sys. mkdir (static_path ^ " /root/aaa" ) 0o700 ;
110- Sys. mkdir (static_path ^ " /root/bbb" ) 0o000 ;
111- Sys. mkdir (static_path ^ " /root/bbb/lb" ) 0o777 ;
112- with Sys_error _ -> ()
107+ let init_sut () = try Sys. mkdir (static_path ^ " /" ^ " root" ) 0o777 with Sys_error _ -> ()
113108
114- let cleanup _ = ignore (reset_root (static_path ^ " /root" ))
109+ let cleanup _ = ignore (reset_root (static_path ^ " /" ^ " root" ))
115110
116111 let precond _c _s = true
117112
118113 let run c _file_name = match c with
119- | File_exists (path , name ) -> Res (bool , Sys. file_exists (static_path ^ (String. concat " /" path) ^ " /" ^ name))
114+ | File_exists (path , name ) -> Res (bool , Sys. file_exists (static_path ^ " / " ^ (String. concat " /" path) ^ " /" ^ name))
120115 | Mkdir (path , dir_name , perm ) ->
121- Res (result unit exn , protect (Sys. mkdir (static_path ^ (String. concat " /" path) ^ " /" ^ dir_name))perm)
116+ (* Format.printf "ce quon mkdir :: %s\n" (static_path ^ "/" ^ (String.concat "/" path) ^ "/" ^ dir_name); *)
117+ Res (result unit exn , protect (Sys. mkdir (static_path ^ " /" ^ (String. concat " /" path) ^ " /" ^ dir_name))perm)
122118
123119 let file_exists (fs : filesys ) path name =
124120 match (find [fs] path name) with
125121 | Some _ -> true
126122 | None -> false
127123
128124 let postcond c (fs : filesys ) res =
125+ let p path dir_name = static_path ^ " /" ^ (String. concat " /" path) ^ " /" ^ dir_name in
126+ (* Format.printf "\n\n\nSTATUS >> %s\n" (show_filesys fs); *)
129127 match c, res with
130- | File_exists (path , name ), Res ((Bool,_ ),b ) -> b = file_exists fs path name
128+ | File_exists (path , name ), Res ((Bool,_ ),b ) ->
129+ (* Format.printf "\n\npath :: %s \t FILEXISTS COMMAND : %b\t %s\n" (p path name) (file_exists fs path name) (show_filesys fs); *)
130+ b = file_exists fs path name
131+
131132 | Mkdir (path, dir_name, _perm), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
132- when s = static_path ^ (String. concat " /" path) ^ " /" ^ dir_name ^ " : Permission denied" ->
133- not (is_perm_ok [fs] path)
133+ when s = (p path dir_name) ^ " : Permission denied" ->
134+ (* Format.printf "\n\npath :: %s \t PERM %s\n" ((p path dir_name) ^ ": Permission denied") (show_filesys fs); *)
135+ let b = not (is_perm_ok [fs] path) in
136+ assert (b);
137+ b
138+
134139 | Mkdir (path, dir_name, _perm), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
135- when s = static_path ^ (String. concat " /" path) ^ " /" ^ dir_name ^ " : File exists" ->
136- file_exists fs path dir_name
140+ when s = (p path dir_name) ^ " : File exists" ->
141+ (* Format.printf "\n\npath :: %s \t FILE EXIST %s\n" ((p path dir_name) ^ ": File exists" ) (show_filesys fs); *)
142+ let b = file_exists fs path dir_name in
143+ assert (b);
144+ b
145+
137146 | Mkdir (path, dir_name, _perm), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
138- when s = static_path ^ (String. concat " /" path) ^ " /" ^ dir_name ^ " : No such file or directory" ->
139- (match path with
147+ when s = (p path dir_name) ^ " : No such file or directory" ->
148+ (* Format.printf "\n\npath :: %s \t NO SUCH %s\n" ((p path dir_name)^ ": No such file or directory") (show_filesys fs); *)
149+ let b = match path with
150+ | [] -> false
151+ | hd_path :: tl_path -> not (file_exists fs tl_path hd_path) in
152+ assert (b);
153+ b
154+
155+ | Mkdir (path , dir_name , _perm ), Res ((Result (Unit,Exn),_ ), Ok () ) ->
156+ assert (is_perm_ok [fs] path); (* good perm*)
157+ assert (not (file_exists fs path dir_name)); (* not already exists*)
158+ assert (match path with (* path is good*)
140159 | [] -> true
141- | hd_path :: tl_path -> not (file_exists fs tl_path hd_path))
142- | Mkdir (_path , _dir_name , _perm ), Res ((Result (Unit,Exn),_ ), Ok () ) -> true
160+ | hd_path :: tl_path -> file_exists fs tl_path hd_path);
161+ (* Format.printf "\n\n OKKK\n" ; *)
162+ true
143163 | Mkdir (_path , _dir_name , _perm ), Res ((Result (Unit,Exn),_ ), _r ) -> assert (false )
144164 | _ ,_ -> false
145165end
0 commit comments