correction du call ca marche

lib/drivers/alt_ergo.drv

@@ -4,9 +4,13 @@
 prelude "(* this is a prelude for Alt-Ergo*)"
 
 printer "alt-ergo"
-filename "%f-%t-%s.why"
+filename "%f-%t-%s.mlw"
 call_on_file  "alt-ergo %s"
 
+valid "Valid"
+invalid "Invalid"
+unknown "I don't know" "Unknown"
+
 (*
 tranformations
   "simplify_recursive_definition"      
@@ -18,10 +22,9 @@ theory BuiltIn
   syntax type int "int"
   syntax type real "real"
 
-  syntax logic (_=_) "(%1 = %1)"
+  syntax logic (_=_) "(%1 = %2)"
 
- (* inutile car  "<>" devient "not =" *)
-  syntax logic (_<>_) "(%1 = %1)"
+  syntax logic (_<>_) "(%1 = %2)"
 
 end
 

src/output/call_provers.ml

@@ -67,10 +67,10 @@ let remove_file ?(debug=false) f =
 
 let timed_sys_command ?stdin ?(debug=false) ?timeout cmd =
   let t0 = Unix.times () in
-  if debug then Format.eprintf "command line: %s@." cmd;
   let cmd = match timeout with
     | None -> Format.sprintf "%s 2>&1" cmd
-    | Some timeout -> Format.sprintf "%s %d %s 2>&1" !cpulimit timeout cmd in
+    | Some timeout -> Format.sprintf "%s" (*!cpulimit timeout*) cmd in
+  if debug then Format.eprintf "command line: %s@." cmd;
   let (cin,cout) as p = Unix.open_process cmd in
   (match stdin with
     | None -> ()
@@ -144,7 +144,7 @@ let check_prover prover =
   if prover.pr_call_file = None && prover.pr_call_stdin = None then
     raise NoCommandlineProvided
 
-let regexp_call_file = Str.regexp "%\\([a-f]\\)"
+let regexp_call_file = Str.regexp "%\\([a-z]\\)"
 
 let rec on_file ?debug ?timeout pr filename = 
   check_prover pr;
@@ -153,7 +153,7 @@ let rec on_file ?debug ?timeout pr filename =
         let cmd = 
           let repl_fun s = 
             match Str.matched_group 1 s with
-              | "f" -> filename
+              | "s" -> filename
               | _ -> assert false in (*TODO mettre une belle exception*)
           Str.global_substitute regexp_call_file repl_fun cmd in
         let res = timed_sys_command ?debug ?timeout cmd in
@@ -164,14 +164,15 @@ let rec on_file ?debug ?timeout pr filename =
 
 and on_buffer ?debug ?timeout ?filename pr buf =
   check_prover pr;
-  match pr.pr_call_file with
+  match pr.pr_call_stdin with
     | Some cmd -> 
         let res = timed_sys_command ?debug ?timeout ~stdin:buf cmd in
         treat_result pr res
     | None -> 
         match filename with
           | None -> raise NoCommandlineProvided
-          | Some filename -> Sysutil.open_temp_file filename
+          | Some filename -> Sysutil.open_temp_file ?debug filename
               (fun file cout ->
                  Buffer.output_buffer cout buf;
+                 flush cout;
                  on_file ?timeout ?debug pr file)

src/output/driver.ml

@@ -285,8 +285,8 @@ let load_driver file env =
     | RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps
     | Filename s -> set_or_raise loc filename s "filename"
   in
-  let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
   List.iter add f.f_global;
+  let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
   { drv_printer    = !printer;
     drv_context    = Context.init_context env;
     drv_prover     = {Call_provers.pr_call_stdin = !call_stdin;

src/test.why

@@ -5,7 +5,8 @@ theory Test
   use import prelude.Int
   logic id(x: int) : int = x
   logic even(x: int) = 2*(x/2) = x
-  goal G : forall x:int. 0 = zero
+  goal G : forall x:int. 0 = 0
+  goal G2 : forall x:int. 0 = 1
 end
 
 (*

src/util/sysutil.ml

@@ -40,15 +40,15 @@ let file_contents_buf f =
 
 let file_contents f = Buffer.contents (file_contents_buf f)
 
-let open_temp_file filesuffix usefile =
+let open_temp_file ?(debug=false) filesuffix usefile =
   let file,cout = Filename.open_temp_file "why" filesuffix in
   try
     let res = usefile file cout in
-    Sys.remove file;
+    if not debug then Sys.remove file;
     close_out cout;
     res
   with
     | e ->    
-        Sys.remove file;
+        if not debug then Sys.remove file;
         close_out cout;
         raise e

src/util/sysutil.mli

@@ -26,7 +26,9 @@ val file_contents : string -> string
 (* return the content of a file *)
 val file_contents_buf : string -> Buffer.t
 
-val open_temp_file : string -> (string -> out_channel -> 'a) -> 'a
+val open_temp_file : 
+  ?debug:bool -> (* don't remove the file *)
+  string -> (string -> out_channel -> 'a) -> 'a
 (* open_temp_file suffix usefile 
    Create a temporary file with suffix suffix,
    and call usefile on this file (filename and open_out).