Commit 87967761 authored by MARCHE Claude's avatar MARCHE Claude

Better handling of "out of memory" in particular from CVC3

parent f4c86e97
...@@ -7,8 +7,8 @@ filename "%f-%t-%g.cvc" ...@@ -7,8 +7,8 @@ filename "%f-%t-%g.cvc"
(* 'fail' must be before 'valid'; otherwise it is ignored *) (* 'fail' must be before 'valid'; otherwise it is ignored *)
fail "Parse Error: \\(.*\\)" "\\1" fail "Parse Error: \\(.*\\)" "\\1"
valid "Valid." valid "Valid\\."
unknown "Unknown." "" unknown "Unknown\\." ""
outofmemory "Out of memory\\|std::bad_alloc" outofmemory "Out of memory\\|std::bad_alloc"
time "why3cpulimit time : %s s" time "why3cpulimit time : %s s"
......
...@@ -181,10 +181,10 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ...@@ -181,10 +181,10 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
let ans = match ret with let ans = match ret with
| Unix.WSTOPPED n -> | Unix.WSTOPPED n ->
Debug.dprintf debug "Call_provers: stopped by signal %d@." n; Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
HighFailure grep out regexps
| Unix.WSIGNALED n -> | Unix.WSIGNALED n ->
Debug.dprintf debug "Call_provers: killed by signal %d@." n; Debug.dprintf debug "Call_provers: killed by signal %d@." n;
HighFailure grep out regexps
| Unix.WEXITED n -> | Unix.WEXITED n ->
Debug.dprintf debug "Call_provers: exited with status %d@." n; Debug.dprintf debug "Call_provers: exited with status %d@." n;
(try List.assoc n exitcodes with Not_found -> grep out regexps) (try List.assoc n exitcodes with Not_found -> grep out regexps)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment