Add a "OutOfMemory" proof result

ROADMAP

@@ -71,6 +71,17 @@
 * extraction vers Caml
  - PRIORITAIRE, JCF, ANDREI
 
+* terminaison
+** generer une obligation de preuve de well-foundedness quand on utilise
+   un variant avec "with R" (une seule fois pour chaque R !)
+** quand une definition logique recursive ne peut pas etre verifiee
+   bien-fondee statiquement, generer une obligation de preuve
+   (feature wish de F Besson)
+
+* Coq detection
+** refuser de detecter Coq si on n'a pas compilé avec le support de Coq
+   (i.e. si Coq a ete installé apres)
+
 * Coq tactic
 ** ajout de bases de hint
 

src/coq-tactic/why3tac.ml

@@ -1119,6 +1119,7 @@ let why3tac ?(timelimit=timelimit) s gl =
       | Unknown s -> error ("Don't know: " ^ s)
       | Failure s -> error ("Failure: " ^ s)
       | Timeout -> error "Timeout"
+      | OutOfMemory -> error "Out Of Memory"
       | HighFailure ->
           error ("Prover failure\n" ^ res.pr_output ^ "\n")
   with

src/driver/call_provers.ml

@@ -73,6 +73,7 @@ type prover_answer =
   | Valid
   | Invalid
   | Timeout
+  | OutOfMemory
   | Unknown of string
   | Failure of string
   | HighFailure
@@ -88,6 +89,7 @@ let print_prover_answer fmt = function
   | Valid -> fprintf fmt "Valid"
   | Invalid -> fprintf fmt "Invalid"
   | Timeout -> fprintf fmt "Timeout"
+  | OutOfMemory -> fprintf fmt "Ouf Of Memory"
   | Unknown "" -> fprintf fmt "Unknown"
   | Failure "" -> fprintf fmt "Failure"
   | Unknown s -> fprintf fmt "Unknown: %s" s
@@ -113,7 +115,7 @@ let rec grep out l = match l with
       begin try
         ignore (Str.search_forward re out 0);
         match pa with
-        | Valid | Invalid | Timeout -> pa
+        | Valid | Invalid | Timeout | OutOfMemory -> pa
         | Unknown s -> Unknown (Str.replace_matched s out)
         | Failure s -> Failure (Str.replace_matched s out)
         | HighFailure -> assert false

src/driver/call_provers.mli

@@ -27,6 +27,8 @@ type prover_answer =
       (** The task is invalid *)
   | Timeout
       (** the task timeout, ie it takes more time than specified *)
+  | OutOfMemory
+      (** the task timeout, ie it takes more time than specified *)
   | Unknown of string
       (** The prover can't determine if the task is valid *)
   | Failure of string

src/driver/driver.ml

@@ -98,12 +98,14 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | RegexpValid s -> add_to_list regexps (Str.regexp s, Valid)
     | RegexpInvalid s -> add_to_list regexps (Str.regexp s, Invalid)
     | RegexpTimeout s -> add_to_list regexps (Str.regexp s, Timeout)
+    | RegexpOutOfMemory s -> add_to_list regexps (Str.regexp s, OutOfMemory)
     | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
     | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
     | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
     | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
     | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
     | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
+    | ExitCodeOutOfMemory s -> add_to_list exitcodes (s, OutOfMemory)
     | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
     | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
     | Filename s -> set_or_raise loc filename s "filename"

src/driver/driver_ast.ml

@@ -51,12 +51,14 @@ type global =
   | RegexpValid of string
   | RegexpInvalid of string
   | RegexpTimeout of string
+  | RegexpOutOfMemory of string
   | RegexpUnknown of string * string
   | RegexpFailure of string * string
   | TimeRegexp of string
   | ExitCodeValid of int
   | ExitCodeInvalid of int
   | ExitCodeTimeout of int
+  | ExitCodeOutOfMemory of int
   | ExitCodeUnknown of int * string
   | ExitCodeFailure of int * string
   | Filename of string

src/ide/gconfig.ml

@@ -324,11 +324,13 @@ let iconname_valid = "accept32"
 let iconname_unknown = "help32"
 let iconname_invalid = "delete32"
 let iconname_timeout = "clock32"
+let iconname_outofmemory = "deletefile32"
 let iconname_failure = "bug32"
 let iconname_valid_obs = "obsaccept32"
 let iconname_unknown_obs = "obshelp32"
 let iconname_invalid_obs = "obsdelete32"
 let iconname_timeout_obs = "obsclock32"
+let iconname_outofmemory_obs = "obsdeletefile32"
 let iconname_failure_obs = "obsbug32"
 let iconname_yes = "accept32"
 let iconname_no = "delete32"
@@ -340,7 +342,7 @@ let iconname_editor = "edit32"
 let iconname_replay = "refresh32"
 let iconname_cancel = "cut32"
 let iconname_reload = "movefile32"
-let iconname_remove = "deletefile32"
+let iconname_remove = "delete32"
 let iconname_cleaning = "trashb32"
 
 let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
@@ -352,11 +354,13 @@ let image_valid = ref !image_default
 let image_unknown = ref !image_default
 let image_invalid = ref !image_default
 let image_timeout = ref !image_default
+let image_outofmemory = ref !image_default
 let image_failure = ref !image_default
 let image_valid_obs = ref !image_default
 let image_unknown_obs = ref !image_default
 let image_invalid_obs = ref !image_default
 let image_timeout_obs = ref !image_default
+let image_outofmemory_obs = ref !image_default
 let image_failure_obs = ref !image_default
 let image_yes = ref !image_default
 let image_no = ref !image_default
@@ -382,11 +386,13 @@ let resize_images size =
   image_unknown := image ~size iconname_unknown;
   image_invalid := image ~size iconname_invalid;
   image_timeout := image ~size iconname_timeout;
+  image_outofmemory := image ~size iconname_outofmemory;
   image_failure := image ~size iconname_failure;
   image_valid_obs := image ~size iconname_valid_obs;
   image_unknown_obs := image ~size iconname_unknown_obs;
   image_invalid_obs := image ~size iconname_invalid_obs;
   image_timeout_obs := image ~size iconname_timeout_obs;
+  image_outofmemory_obs := image ~size iconname_outofmemory_obs;
   image_failure_obs := image ~size iconname_failure_obs;
   image_yes := image ~size iconname_yes;
   image_no := image ~size iconname_no;
@@ -441,6 +447,8 @@ let show_legend_window () =
 *)
   ib image_timeout;
   i "   External prover reached the time limit\n";
+  ib image_outofmemory;
+  i "   External prover ran out of memory\n";
   ib image_unknown;
   i "   External prover answer not conclusive\n";
   ib image_failure;

src/ide/gconfig.mli

@@ -82,11 +82,13 @@ val image_running : GdkPixbuf.pixbuf ref
 val image_valid : GdkPixbuf.pixbuf ref
 val image_invalid : GdkPixbuf.pixbuf ref
 val image_timeout : GdkPixbuf.pixbuf ref
+val image_outofmemory : GdkPixbuf.pixbuf ref
 val image_unknown : GdkPixbuf.pixbuf ref
 val image_failure : GdkPixbuf.pixbuf ref
 val image_valid_obs : GdkPixbuf.pixbuf ref
 val image_invalid_obs : GdkPixbuf.pixbuf ref
 val image_timeout_obs : GdkPixbuf.pixbuf ref
+val image_outofmemory_obs : GdkPixbuf.pixbuf ref
 val image_unknown_obs : GdkPixbuf.pixbuf ref
 val image_failure_obs : GdkPixbuf.pixbuf ref
 

src/ide/gmain.ml

@@ -426,6 +426,8 @@ let image_of_result ~obsolete result =
             if obsolete then !image_invalid_obs else !image_invalid
         | Call_provers.Timeout ->
             if obsolete then !image_timeout_obs else !image_timeout
+        | Call_provers.OutOfMemory ->
+            if obsolete then !image_outofmemory_obs else !image_outofmemory
         | Call_provers.Unknown _ ->
             if obsolete then !image_unknown_obs else !image_unknown
         | Call_provers.Failure _ ->

src/ide/replay.ml

@@ -306,6 +306,7 @@ let same_result r1 r2 =
     | Call_provers.Valid, Call_provers.Valid -> true
     | Call_provers.Invalid, Call_provers.Invalid -> true
     | Call_provers.Timeout, Call_provers.Timeout -> true
+    | Call_provers.OutOfMemory, Call_provers.OutOfMemory -> true
     | Call_provers.Unknown _, Call_provers.Unknown _-> true
     | Call_provers.Failure _, Call_provers.Failure _-> true
     | _ -> false

src/session/session.ml

@@ -333,6 +333,7 @@ let save_result fmt r =
        | Call_provers.Unknown _ -> "unknown"
        | Call_provers.HighFailure -> "highfailure"
        | Call_provers.Timeout -> "timeout"
+       | Call_provers.OutOfMemory -> "outofmemory"
        | Call_provers.Invalid -> "invalid")
     r.Call_provers.pr_time
 
@@ -739,6 +740,7 @@ let load_result r =
             | "invalid" -> Call_provers.Invalid
             | "unknown" -> Call_provers.Unknown ""
             | "timeout" -> Call_provers.Timeout
+            | "outofmemory" -> Call_provers.OutOfMemory
             | "failure" -> Call_provers.Failure ""
             | "highfailure" -> Call_provers.Failure ""
             | s ->

src/why3session/why3session_html.ml

@@ -142,12 +142,17 @@ let print_results fmt provers proofs =
                   fprintf fmt "FF0000\">Invalid"
 		| Call_provers.Timeout ->
                   fprintf fmt "FF8000\">Timeout"
+		| Call_provers.OutOfMemory ->
+                  fprintf fmt "FF8000\">Out Of Memory"
 		| Call_provers.Unknown _ ->
                   fprintf fmt "FF8000\">%.2f" res.Call_provers.pr_time
-		| _ ->
+		| Call_provers.Failure _ ->
                   fprintf fmt "FF8000\">Failure "
+		| Call_provers.HighFailure _ ->
+                  fprintf fmt "FF8000\">High Failure "
 	    end
-	  | _ -> fprintf fmt "E0E0E0\">Undone"
+	  | S.Undone _ -> fprintf fmt "E0E0E0\">Undone"
+	  | S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure"
       with Not_found -> fprintf fmt "E0E0E0\">---"
     end;
     fprintf fmt "</td>") provers

src/why3session/why3session_latex.ml

@@ -132,17 +132,20 @@ let print_result_prov proofs prov fmt=
     let pr = S.PHprover.find proofs p in
     let s = pr.S.proof_state in
       match s with
-	  Session.Done res ->
+	| Session.Done res ->
 	    begin
 	      match res.Call_provers.pr_answer with
 		  Call_provers.Valid ->
                     fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
 		| Call_provers.Invalid -> fprintf fmt "& \\invalid "
 		| Call_provers.Timeout -> fprintf fmt "& \\timeout "
-		| Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
-		| _ -> fprintf fmt "& \\failure "
+		| Call_provers.OutOfMemory -> fprintf fmt "& \\outofmemory "
+		| Call_provers.Unknown _ -> fprintf fmt "& \\unknown "
+		| Call_provers.Failure _ -> fprintf fmt "& \\failure "
+		| Call_provers.HighFailure _ -> fprintf fmt "& \\highfailure "
 	    end
-	| _ -> fprintf fmt "& Undone"
+	| Session.InternalFailure _ -> fprintf fmt "& Internal Failure"
+	| Session.Undone _ -> fprintf fmt "& Undone"
   with Not_found -> fprintf fmt "& \\noresult") prov;
   fprintf fmt "\\\\ @."