Commit aa063026 authored by MARCHE Claude's avatar MARCHE Claude

out of memory answer in drivers

parent f816685f
...@@ -9,6 +9,7 @@ filename "%f-%t-%g.cvc" ...@@ -9,6 +9,7 @@ filename "%f-%t-%g.cvc"
fail "Parse Error: \\(.*\\)" "\\1" fail "Parse Error: \\(.*\\)" "\\1"
valid "Valid." valid "Valid."
unknown "Unknown." "" unknown "Unknown." ""
outofmemory "Out of memory\\|std::bad_alloc"
time "why3cpulimit time : %s s" time "why3cpulimit time : %s s"
(* À discuter *) (* À discuter *)
......
...@@ -7,8 +7,9 @@ valid "Proof found" ...@@ -7,8 +7,9 @@ valid "Proof found"
invalid "Completion found" invalid "Completion found"
invalid "SZS status CounterSatisfiable" invalid "SZS status CounterSatisfiable"
timeout "Ran out of time" timeout "Ran out of time"
timeout "Resource limit exceeded" (* timeout "Resource limit exceeded" *)
timeout "CPU time limit exceeded" timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" "Unknown" unknown "No Proof Found" "Unknown"
fail "Failure.*" "\"\\0\"" fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s" time "why3cpulimit time : %s s"
......
...@@ -7,6 +7,7 @@ valid "Refutation found" ...@@ -7,6 +7,7 @@ valid "Refutation found"
(* timeout "Aborted by signal SIGXCPU on" *) (* timeout "Aborted by signal SIGXCPU on" *)
unknown "Time limit reached" "Time out" unknown "Time limit reached" "Time out"
unknown "Refutation not found" "Unknown" unknown "Refutation not found" "Unknown"
outofmemory "Memory limit exceeded"
(* invalid "Completion found" *) (* invalid "Completion found" *)
(* invalid "SZS status CounterSatisfiable" *) (* invalid "SZS status CounterSatisfiable" *)
(* timeout "Ran out of time" *) (* timeout "Ran out of time" *)
......
...@@ -8,6 +8,7 @@ filename "%f-%t-%g.smt" ...@@ -8,6 +8,7 @@ filename "%f-%t-%g.smt"
valid "^unsat" valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown" unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
outofmemory "(error \"out of memory\")\\|Cannot allocate memory"
time "why3cpulimit time : %s s" time "why3cpulimit time : %s s"
...@@ -15,6 +16,7 @@ time "why3cpulimit time : %s s" ...@@ -15,6 +16,7 @@ time "why3cpulimit time : %s s"
(*transformation "simplify_recursive_definition"*) (*transformation "simplify_recursive_definition"*)
transformation "inline_trivial" transformation "inline_trivial"
transformation "eliminate_builtin" transformation "eliminate_builtin"
transformation "eliminate_definition" transformation "eliminate_definition"
transformation "eliminate_inductive" transformation "eliminate_inductive"
......
...@@ -45,6 +45,7 @@ ...@@ -45,6 +45,7 @@
"valid", VALID; "valid", VALID;
"invalid", INVALID; "invalid", INVALID;
"timeout", TIMEOUT; "timeout", TIMEOUT;
"outofmemory", OUTOFMEMORY;
"time", TIME; "time", TIME;
"unknown", UNKNOWN; "unknown", UNKNOWN;
"fail", FAIL; "fail", FAIL;
......
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
%token <string> STRING %token <string> STRING
%token <string> OPERATOR %token <string> OPERATOR
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
%token VALID INVALID TIMEOUT UNKNOWN FAIL TIME %token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF %token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
%token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN %token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN
%token LEFTPAR_STAR_RIGHTPAR COMMA %token LEFTPAR_STAR_RIGHTPAR COMMA
...@@ -65,6 +65,7 @@ global: ...@@ -65,6 +65,7 @@ global:
| VALID STRING { RegexpValid $2 } | VALID STRING { RegexpValid $2 }
| INVALID STRING { RegexpInvalid $2 } | INVALID STRING { RegexpInvalid $2 }
| TIMEOUT STRING { RegexpTimeout $2 } | TIMEOUT STRING { RegexpTimeout $2 }
| OUTOFMEMORY STRING { RegexpOutOfMemory $2 }
| TIME STRING { TimeRegexp $2 } | TIME STRING { TimeRegexp $2 }
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) } | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) } | FAIL STRING STRING { RegexpFailure ($2, $3) }
......
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