new prover option in_place to run the verification on the original file

the original file is properly saved and restored upon completion
(whatever the result is)

share/provers-detection-data.conf.in

@@ -354,6 +354,7 @@ version_regexp = "PVS Version \\([^ \n]+\\)"
 version_ok = "5.0"
 command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
 driver = "drivers/pvs.drv"
+in_place = true
 editor = "pvs"
 
 [editor pvs]

src/bench/benchdb.ml

@@ -80,7 +80,7 @@ let rec goal whyconf env path dbgoal wgoal =
       let old = if edited_as = "" then None else
           begin
             eprintf "Info: proving using edited file %s@." edited_as;
-            (Some (open_in edited_as))
+            (Some edited_as)
           end
       in
       let call_prover : Call_provers.pre_prover_call =

src/driver/autodetection.ml

@@ -42,6 +42,7 @@ type prover_autodetection_data =
       prover_command : string;
       prover_driver : string;
       prover_editor : string;
+      prover_in_place : bool;
     }
 
 let prover_keys =
@@ -49,7 +50,7 @@ let prover_keys =
   List.fold_left add Sstr.empty
     ["name";"exec";"version_switch";"version_regexp";
      "version_ok";"version_old";"version_bad";"command";
-     "editor";"driver"]
+     "editor";"driver";"in_place"]
 
 let load_prover kind (id,section) =
   check_exhaustive section prover_keys;
@@ -65,6 +66,7 @@ let load_prover kind (id,section) =
     prover_command = get_string section "command";
     prover_driver = get_string section "driver";
     prover_editor = get_string section ~default:"" "editor";
+    prover_in_place = get_bool section ~default:false "in_place";
   }
 
 let editor_keys =
@@ -187,6 +189,7 @@ let detect_exec main data com =
               command = c;
               driver  = Filename.concat (datadir main) data.prover_driver;
               editor = data.prover_editor;
+              in_place = data.prover_in_place;
               interactive = (match data.kind with ITP -> true | ATP -> false);
               extra_options = [];
               extra_drivers = [] }

src/driver/call_provers.ml

@@ -128,9 +128,11 @@ type post_prover_call = unit -> prover_result
 type prover_call = Unix.wait_flag list -> post_prover_call
 type pre_prover_call = unit -> prover_call
 
+let save f = f ^ ".save"
+
 let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
                  ~regexps ~timeregexps ~exitcodes
-                 ?(cleanup=false) fin =
+                 ?(cleanup=false) ?(inplace=false) fin =
 
   let arglist = Cmdline.cmdline_split command in
   let command = List.hd arglist in
@@ -150,8 +152,12 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
     | _ -> failwith "unknown specifier, use %%f, %%t, %%m, %%l, or %%d"
   in
   let subst s =
-    try Str.global_substitute cmd_regexp replace s
-    with e -> if cleanup then Sys.remove fin; raise e
+    try
+      Str.global_substitute cmd_regexp replace s
+    with e ->
+      if cleanup then Sys.remove fin;
+      if inplace then Sys.rename (save fin) fin;
+      raise e
   in
   let arglist = List.map subst arglist in
   Debug.dprintf debug "@[<hov 2>Call_provers: command is: %a@]@."
@@ -179,6 +185,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
       fun () ->
         if Debug.nottest_flag debug then begin
           if cleanup then Sys.remove fin;
+          if inplace then Sys.rename (save fin) fin;
           Sys.remove fout
         end;
         let ans = match ret with
@@ -205,12 +212,18 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
           pr_time   = time }
 
 let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
-                   ~regexps ~timeregexps ~exitcodes ~filename buffer =
-
-  let fin,cin = Filename.open_temp_file "why_" ("_" ^ filename) in
+                   ~regexps ~timeregexps ~exitcodes ~filename
+                   ?(inplace=false) buffer =
+
+  let fin,cin =
+    if inplace then begin
+      Sys.rename filename (save filename);
+      filename, open_out filename
+    end else
+      Filename.open_temp_file "why_" ("_" ^ filename) in
   Buffer.output_buffer cin buffer; close_out cin;
   call_on_file ~command ~timelimit ~memlimit
-               ~regexps ~timeregexps ~exitcodes ~cleanup:true fin
+               ~regexps ~timeregexps ~exitcodes ~cleanup:true ~inplace fin
 
 let query_call call = try Some (call [Unix.WNOHANG]) with Exit -> None
 

src/driver/call_provers.mli

@@ -85,6 +85,7 @@ val call_on_file :
   timeregexps : timeregexp list ->
   exitcodes   : (int * prover_answer) list ->
   ?cleanup    : bool ->
+  ?inplace    : bool ->
   string -> pre_prover_call
 
 val call_on_buffer :
@@ -95,6 +96,7 @@ val call_on_buffer :
   timeregexps : timeregexp list ->
   exitcodes   : (int * prover_answer) list ->
   filename    : string ->
+  ?inplace    : bool ->
   Buffer.t -> pre_prover_call
 (** Call a prover on the task printed in the {!type: Buffer.t} given.
 

src/driver/driver.ml

@@ -227,13 +227,13 @@ let file_of_task drv input_file theory_name task =
 let file_of_theory drv input_file th =
   get_filename drv input_file th.th_name.Ident.id_string "null"
 
-let call_on_buffer ~command ?timelimit ?memlimit ~filename drv buffer =
+let call_on_buffer ~command ?timelimit ?memlimit ?inplace ~filename drv buffer =
   let regexps = drv.drv_regexps in
   let timeregexps = drv.drv_timeregexps in
   let exitcodes = drv.drv_exitcodes in
   Call_provers.call_on_buffer
     ~command ?timelimit ?memlimit ~regexps ~timeregexps
-    ~exitcodes ~filename buffer
+    ~exitcodes ~filename ?inplace buffer
 
 (** print'n'prove *)
 
@@ -300,25 +300,31 @@ let print_theory ?old drv fmt th =
   let task = Task.use_export None th in
   print_task ?old drv fmt task
 
-let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
+let prove_task_prepared
+  ~command ?timelimit ?memlimit ?old ?inplace drv task =
   let buf = Buffer.create 1024 in
   let fmt = formatter_of_buffer buf in
-  print_task_prepared ?old drv fmt task; pp_print_flush fmt ();
-  let filename =
-    let pr = Task.task_goal task in
-    let fn = match pr.pr_name.id_loc with
-      | Some loc -> let fn,_,_,_ = Loc.get loc in Filename.basename fn
-      | None -> "" in
-    let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
-    get_filename drv fn "T" pr.pr_name.id_string
+  let old_channel = option_map open_in old in
+  print_task_prepared ?old:old_channel drv fmt task; pp_print_flush fmt ();
+  option_iter close_in old_channel;
+  let filename = match old, inplace with
+    | Some fn, Some true -> fn
+    | _ ->
+        let pr = Task.task_goal task in
+        let fn = match pr.pr_name.id_loc with
+          | Some loc -> let fn,_,_,_ = Loc.get loc in Filename.basename fn
+          | None -> "" in
+        let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
+        get_filename drv fn "T" pr.pr_name.id_string
   in
-  let res = call_on_buffer ~command ?timelimit ?memlimit ~filename drv buf in
+  let res =
+    call_on_buffer ~command ?timelimit ?memlimit ?inplace ~filename drv buf in
   Buffer.reset buf;
   res
 
-let prove_task ~command ?timelimit ?memlimit ?old drv task =
+let prove_task ~command ?timelimit ?memlimit ?old ?inplace drv task =
   let task = prepare_task drv task in
-  prove_task_prepared ~command ?timelimit ?memlimit ?old drv task
+  prove_task_prepared ~command ?timelimit ?memlimit ?old ?inplace drv task
 
 (* exception report *)
 

src/driver/driver.mli

@@ -47,6 +47,7 @@ val call_on_buffer :
   command    : string ->
   ?timelimit : int ->
   ?memlimit  : int ->
+  ?inplace   : bool ->
   filename   : string ->
   driver -> Buffer.t -> Call_provers.pre_prover_call
 
@@ -64,7 +65,8 @@ val prove_task :
   command    : string ->
   ?timelimit : int ->
   ?memlimit  : int ->
-  ?old       : in_channel ->
+  ?old       : string ->
+  ?inplace   : bool ->
   driver -> Task.task -> Call_provers.pre_prover_call
 
 (** Split the previous function in two simpler functions *)
@@ -78,6 +80,7 @@ val prove_task_prepared :
   command    : string ->
   ?timelimit : int ->
   ?memlimit  : int ->
-  ?old       : in_channel ->
+  ?old       : string ->
+  ?inplace   : bool ->
   driver -> Task.task -> Call_provers.pre_prover_call
 

src/driver/whyconf.ml

@@ -113,6 +113,7 @@ type config_prover = {
   id      : string;
   command : string;
   driver  : string;
+  in_place: bool;
   editor  : string;
   interactive : bool;
   extra_options : string list;
@@ -236,6 +237,7 @@ let set_prover _ prover (ids,family) =
   let section = set_string ~default:"" section "alternative" prover.prover.prover_altern in
   let section = set_string section "editor" prover.editor in
   let section = set_bool section "interactive" prover.interactive in
+  let section = set_bool section "in_place" prover.in_place in
   (Sstr.add prover.id ids,(prover.id,section)::family)
 
 let set_provers rc provers =
@@ -298,6 +300,7 @@ let load_prover dirname provers (id,section) =
       prover  = prover;
       command = get_string section "command";
       driver  = absolute_filename dirname (get_string section "driver");
+      in_place = get_bool ~default:false section "in_place";
       editor  = get_string ~default:"" section "editor";
       interactive = get_bool ~default:false section "interactive";
       extra_options = [];

src/driver/whyconf.mli

@@ -109,6 +109,7 @@ type config_prover = {
   id      : string; (* unique name for command line *)
   command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
   driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
+  in_place: bool;     (* verification should be performed in-place *)
   editor  : string;   (* Dedicated editor *)
   interactive : bool; (* Interactive theorem prover *)
   extra_options : string list;

src/session/session_scheduler.ml

@@ -93,7 +93,7 @@ let running a = match a.proof_state with
 (*************************)
 
 type action =
-  | Action_proof_attempt of int * int * in_channel option * string *
+  | Action_proof_attempt of int * int * string option * bool * string *
       Driver.driver * (proof_attempt_status -> unit) * Task.task
   | Action_delayed of (unit -> unit)
 
@@ -218,14 +218,14 @@ let idle_handler t =
   try
     begin
       match Queue.pop t.actions_queue with
-        | Action_proof_attempt(timelimit,memlimit,old,command,driver,
+        | Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
                                callback,goal) ->
             callback (Undone Scheduled);
             begin
               try
                 let pre_call =
                   Driver.prove_task
-                    ?old ~command ~timelimit ~memlimit driver goal
+                    ?old ~inplace ~command ~timelimit ~memlimit driver goal
                 in
                 Queue.push (callback,pre_call) t.proof_attempts_queue;
                 run_timeout_handler t
@@ -264,7 +264,7 @@ let cancel_scheduled_proofs t =
   try
     while true do
       match Queue.pop t.actions_queue with
-        | Action_proof_attempt(_timelimit,_memlimit,_old,_command,
+        | Action_proof_attempt(_timelimit,_memlimit,_old,_inplace,_command,
                                _driver,callback,_goal) ->
             callback (Undone Interrupted)
         | Action_delayed _ as a->
@@ -282,13 +282,13 @@ let cancel_scheduled_proofs t =
           O.notify_timer_state 0 0 (List.length t.running_proofs)
 
 
-let schedule_proof_attempt ~timelimit ~memlimit ?old
+let schedule_proof_attempt ~timelimit ~memlimit ?old ~inplace
     ~command ~driver ~callback t goal =
     dprintf debug "[Sched] Scheduling a new proof attempt (goal : %a)@."
       (fun fmt g -> Format.pp_print_string fmt
        (Task.task_goal g).Decl.pr_name.Ident.id_string) goal;
   Queue.push
-    (Action_proof_attempt(timelimit,memlimit,old,command,driver,
+    (Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
                         callback,goal))
     t.actions_queue;
   run_idle_handler t
@@ -475,20 +475,21 @@ let run_external_proof eS eT ?callback a =
               | Some f ->
                 if Sys.file_exists f then begin
                   dprintf debug "Info: proving using edited file %s@." f;
-                  (Some (open_in f))
+                  (Some f)
                 end
                 else begin
                   dprintf debug "Warning: the file %s is not found@." f;
                   None
                 end
           in
+          let inplace = npc.prover_config.Whyconf.in_place in
           let command =
             String.concat " " (npc.prover_config.Whyconf.command ::
                                  npc.prover_config.Whyconf.extra_options) in
           (* eprintf "scheduling it...@."; *)
           schedule_proof_attempt
             ~timelimit ~memlimit
-            ?old ~command
+            ?old ~inplace ~command
             ~driver:npc.prover_driver
             ~callback
             eT
@@ -677,11 +678,12 @@ let check_external_proof eS eT todo a =
                   if Sys.file_exists f then
                     begin
                     (* Format.eprintf "Info: proving using edited file %s@." f; *)
-                      (Some (open_in f))
+                      (Some f)
                     end
                   else
                     raise (NoFile f)
             in
+            let inplace = npc.prover_config.Whyconf.in_place in
             let timelimit = adapt_timelimit a in
             let memlimit = a.proof_memlimit in
             let callback result =
@@ -710,7 +712,7 @@ let check_external_proof eS eT todo a =
                                    npc.prover_config.Whyconf.extra_options) in
             schedule_proof_attempt eT
               ~timelimit ~memlimit
-              ?old ~command
+              ?old ~inplace ~command
               ~driver:npc.prover_driver
               ~callback
               (goal_task g)

tests/test-jcf.why

 
 theory T
 
-  type t = None | Some int
+  use import int.Int
 
-  goal G: forall x: t. x <> None ->
-          match x with None -> false | Some z -> z = 0 end
+  goal G: 1+3 > 2
 
 end