From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Mar 2004 17:57:39 +0000 (+0000)
Subject: Added option -timeout. Default is 5s.
X-Git-Tag: v0_0_4~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa4474a3b23b71b8a6e0d36f0daa0e90b3ffed66;p=helm.git

Added option -timeout. Default is 5s.
---

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 107cc3c54..ee1b982c4 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -1,6 +1,8 @@
 
 open Printf
 
+let time_out = ref 5;;
+
 Helm_registry.load_from "gTopLevel.conf.xml";;
 
 let mqi_debug_fun s =
@@ -89,16 +91,33 @@ let test_uri uri =
       debug_print "AInductiveDefinition: boh ..." ;
       assert false
 
+exception TimeOut;;
+                                                                                
+ignore
+ (Sys.signal Sys.sigalrm
+   (Sys.Signal_handle
+     (fun _ ->
+       (* We do this in case that some "with _" intercepts the first exception *)
+       ignore (Unix.alarm 1) ;
+       raise TimeOut)))
+;;
+
+
 let test_uri uri =
   try
+   ignore (Unix.alarm !time_out) ;
    if test_uri uri = 1 then `Ok else `Maybe
   with
+  | TimeOut ->
+     (* We do this to clear the alarm set by the signal handler *)
+     ignore (Unix.alarm 0) ;
+     `TimeOut
   | exn ->
       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
         (Printexc.to_string exn));
       `Nok
 
-let report (ok,nok,maybe) =
+let report (ok,nok,maybe,timeout) =
   print_newline ();
   print_endline "TestLibrary report";
   print_endline "Succeeded URIs:";
@@ -107,9 +126,12 @@ let report (ok,nok,maybe) =
   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok);
   print_endline "Multiple answers URIs:";
   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe);
+  print_newline ();
+  print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):");
+  List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
   print_newline ()
 
-let do_uri (ok, nok, maybe) uri =
+let do_uri (ok, nok, maybe, timeout) uri =
   let uri_str = UriManager.string_of_uri uri in
   printf "Testing URI: %-55s %!" (uri_str ^ " ...");
   match test_uri uri with
@@ -122,6 +144,9 @@ let do_uri (ok, nok, maybe) uri =
   | `Maybe ->
       print_endline "[  MANY  ]";
       maybe := uri_str :: !maybe
+  | `TimeOut ->
+      print_endline "[TIMEOUT!]";
+      timeout := uri_str :: !timeout
 
 let do_file status fname =
   try
@@ -158,6 +183,8 @@ let _ =
         "limit object choices to URIs beginning with prefix" ; 
       "-varsprefix", Arg.Set_string varsprefix,
         "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
+      "-timeout", Arg.Set_int time_out,
+       "number of seconds before a timeout; 0 means no timeout"
     ]
   in
   Arg.parse spec (fun name -> names := name :: !names) usage;
@@ -165,7 +192,7 @@ let _ =
   if !varsprefix = "####" then varsprefix := !prefix ;
   uri_predicate :=
    BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
-  let status = (ref [], ref [], ref []) in  (* <ok, nok, maybe> URIs *)
+  let status = (ref [], ref [], ref [], ref []) in  (* <ok, nok, maybe, timeout> URIs *)
   List.iter
     (fun name ->
       try