Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
208c71dc
Commit
208c71dc
authored
May 23, 2015
by
Andrei Paskevich
Browse files
"steps limit" is bad English, replace with "step limit"
parent
88b5c150
Changes
23
Hide whitespace changes
Inline
Side-by-side
drivers/alt_ergo_common.drv
View file @
208c71dc
...
...
@@ -9,7 +9,7 @@ valid "Valid"
invalid "Invalid"
unknown "I don't know" ""
timeout "Timeout"
step
s
limitexceeded "Steps limit reached"
steplimitexceeded "Steps limit reached"
outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
...
...
drivers/cvc4_14.drv
View file @
208c71dc
...
...
@@ -40,7 +40,7 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
step
s
limitexceeded "??"
steplimitexceeded "??"
(** Extra theories supported by CVC4 *)
...
...
drivers/cvc4_15.drv
View file @
208c71dc
...
...
@@ -51,7 +51,7 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
step
s
limitexceeded "??"
steplimitexceeded "??"
(** Extra theories supported by CVC4 *)
...
...
share/images/icons.rc
View file @
208c71dc
...
...
@@ -10,14 +10,14 @@ unknown = "help32"
invalid = "delete32"
timeout = "clock32"
outofmemory = "deletefile32"
step
s
limitexceeded = "cut32"
steplimitexceeded = "cut32"
failure = "bug32"
valid_obs = "obsaccept32"
unknown_obs = "obshelp32"
invalid_obs = "obsdelete32"
timeout_obs = "obsclock32"
outofmemory_obs = "obsdeletefile32"
step
s
limitexceeded_obs = "cut32"
steplimitexceeded_obs = "cut32"
failure_obs = "obsbug32"
yes = "accept32"
no = "delete32"
...
...
@@ -47,14 +47,14 @@ unknown = "help"
invalid = "exclamation"
timeout = "time_delete"
outofmemory = "database_delete"
step
s
limitexceeded = "brick_delete"
steplimitexceeded = "brick_delete"
failure = "bomb"
valid_obs = "bullet_green"
unknown_obs = "bullet_blue"
invalid_obs = "bullet_red"
timeout_obs = "time_delete"
outofmemory_obs = "database_delete"
step
s
limitexceeded_obs = "brick_delete"
steplimitexceeded_obs = "brick_delete"
failure_obs = "bullet_black"
yes = "accept"
no = "delete"
...
...
share/why3session.dtd
View file @
208c71dc
...
...
@@ -45,7 +45,7 @@
<!ATTLIST proof archived CDATA #IMPLIED>
<!ELEMENT result EMPTY>
<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|step
s
limitexceeded|failure|highfailure) #REQUIRED>
<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|steplimitexceeded|failure|highfailure) #REQUIRED>
<!ATTLIST result time CDATA #IMPLIED>
<!ATTLIST result steps CDATA #IMPLIED>
...
...
src/coq-tactic/why3tac.ml4
View file @
208c71dc
...
...
@@ -1289,7 +1289,7 @@ let why3tac ?(timelimit=timelimit) s gl =
| Call_provers.Failure s -> error ("Failure: " ^ s)
| Call_provers.Timeout -> error "Timeout"
| OutOfMemory -> error "Out Of Memory"
| Step
s
LimitExceeded -> error "Step
s
Limit
reach
ed"
| StepLimitExceeded -> error "Step Limit
Exceed
ed"
| HighFailure ->
error ("Prover failure\n" ^ res.pr_output ^ "\n")
with
...
...
src/driver/call_provers.ml
View file @
208c71dc
...
...
@@ -28,9 +28,10 @@ type timeregexp = {
group
:
timeunit
array
;
(* i-th corresponds to the group i+1 *)
}
type
step
s
regexp
=
{
type
stepregexp
=
{
steps_re
:
Str
.
regexp
;
steps_group_num
:
int
;
(* the number of matched group which corresponds to the number of steps *)
steps_group_num
:
int
;
(* the number of matched group which corresponds to the number of steps *)
}
let
timeregexp
s
=
...
...
@@ -44,7 +45,8 @@ let timeregexp s =
|
"m"
->
add_unit
Min
|
"s"
->
add_unit
Sec
|
"i"
->
add_unit
Msec
|
x
->
failwith
(
"unknown time format specifier: %%"
^
x
^
" (should be either %%h, %%m, %%s or %%i"
)
|
x
->
failwith
(
"unknown time format specifier: %%"
^
x
^
" (should be either %%h, %%m, %%s or %%i"
)
in
let
s
=
Str
.
global_substitute
cmd_regexp
replace
s
in
let
group
=
Array
.
make
!
nb
Hour
in
...
...
@@ -68,7 +70,7 @@ let rec grep_time out = function
with
_
->
grep_time
out
l
end
let
step
s
regexp
s_re
s_group_num
=
let
stepregexp
s_re
s_group_num
=
{
steps_re
=
(
Str
.
regexp
s_re
);
steps_group_num
=
s_group_num
}
let
rec
grep_steps
out
=
function
...
...
@@ -88,7 +90,7 @@ type prover_answer =
|
Invalid
|
Timeout
|
OutOfMemory
|
Step
s
LimitExceeded
|
StepLimitExceeded
|
Unknown
of
string
|
Failure
of
string
|
HighFailure
...
...
@@ -105,7 +107,7 @@ type prover_result = {
type
prover_result_parser
=
{
prp_regexps
:
(
Str
.
regexp
*
prover_answer
)
list
;
prp_timeregexps
:
timeregexp
list
;
prp_step
s
regexp
:
step
s
regexp
list
;
prp_stepregexp
s
:
stepregexp
list
;
prp_exitcodes
:
(
int
*
prover_answer
)
list
;
prp_model_parser
:
Model_parser
.
model_parser
;
}
...
...
@@ -115,7 +117,7 @@ let print_prover_answer fmt = function
|
Invalid
->
fprintf
fmt
"Invalid"
|
Timeout
->
fprintf
fmt
"Timeout"
|
OutOfMemory
->
fprintf
fmt
"Ouf Of Memory"
|
Step
s
LimitExceeded
->
fprintf
fmt
"Step
s
limit exceeded"
|
StepLimitExceeded
->
fprintf
fmt
"Step limit exceeded"
|
Unknown
""
->
fprintf
fmt
"Unknown"
|
Failure
""
->
fprintf
fmt
"Failure"
|
Unknown
s
->
fprintf
fmt
"Unknown (%s)"
s
...
...
@@ -144,7 +146,7 @@ let rec grep out l = match l with
begin
try
ignore
(
Str
.
search_forward
re
out
0
);
match
pa
with
|
Valid
|
Invalid
|
Timeout
|
OutOfMemory
|
Step
s
LimitExceeded
->
pa
|
Valid
|
Invalid
|
Timeout
|
OutOfMemory
|
StepLimitExceeded
->
pa
|
Unknown
s
->
Unknown
(
Str
.
replace_matched
s
out
)
|
Failure
s
->
Failure
(
Str
.
replace_matched
s
out
)
|
HighFailure
->
assert
false
...
...
@@ -193,7 +195,7 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
in
Debug
.
dprintf
debug
"Call_provers: prover output:@
\n
%s@."
out
;
let
time
=
Opt
.
get_def
(
time
)
(
grep_time
out
res_parser
.
prp_timeregexps
)
in
let
steps
=
Opt
.
get_def
(
-
1
)
(
grep_steps
out
res_parser
.
prp_step
s
regexp
)
in
let
steps
=
Opt
.
get_def
(
-
1
)
(
grep_steps
out
res_parser
.
prp_stepregexp
s
)
in
let
ans
=
match
ans
with
|
Unknown
_
|
HighFailure
when
on_timelimit
&&
timelimit
>
0
&&
time
>=
(
0
.
9
*.
float
timelimit
)
->
Timeout
...
...
@@ -210,7 +212,7 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
pr_model
=
model
;
}
let
actualcommand
command
timelimit
memlimit
step
s
limit
file
=
let
actualcommand
command
timelimit
memlimit
steplimit
file
=
let
arglist
=
Cmdline
.
cmdline_split
command
in
let
use_stdin
=
ref
true
in
(* FIXME: use_stdin is never modified below ?? *)
...
...
@@ -228,20 +230,20 @@ let actualcommand command timelimit memlimit stepslimit file =
to prepare the command line in a separate function? *)
|
"l"
->
Config
.
libdir
|
"d"
->
Config
.
datadir
|
"S"
->
string_of_int
step
s
limit
|
"S"
->
string_of_int
steplimit
|
_
->
failwith
"unknown specifier, use %%, %f, %t, %T, %U, %m, %l, %d or %S"
in
(* FIXME: are we sure that tuples are evaluated from left to right ? *)
List
.
map
(
Str
.
global_substitute
cmd_regexp
replace
)
arglist
,
!
use_stdin
,
!
on_timelimit
let
call_on_file
~
command
?
(
timelimit
=
0
)
?
(
memlimit
=
0
)
?
(
step
s
limit
=
(
-
1
))
let
call_on_file
~
command
?
(
timelimit
=
0
)
?
(
memlimit
=
0
)
?
(
steplimit
=
(
-
1
))
~
res_parser
~
printer_mapping
?
(
cleanup
=
false
)
?
(
inplace
=
false
)
?
(
redirect
=
true
)
fin
=
let
command
,
use_stdin
,
on_timelimit
=
try
actualcommand
command
timelimit
memlimit
step
s
limit
fin
try
actualcommand
command
timelimit
memlimit
steplimit
fin
with
e
->
if
cleanup
then
Sys
.
remove
fin
;
if
inplace
then
Sys
.
rename
(
save
fin
)
fin
;
...
...
@@ -252,10 +254,12 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
let
argarray
=
Array
.
of_list
command
in
fun
()
->
let
fd_in
=
if
use_stdin
then
Unix
.
openfile
fin
[
Unix
.
O_RDONLY
]
0
else
Unix
.
stdin
in
let
fd_in
=
if
use_stdin
then
Unix
.
openfile
fin
[
Unix
.
O_RDONLY
]
0
else
Unix
.
stdin
in
let
fout
,
cout
,
fd_out
,
fd_err
=
if
redirect
then
let
fout
,
cout
=
Filename
.
open_temp_file
(
Filename
.
basename
fin
)
".out"
in
let
fout
,
cout
=
Filename
.
open_temp_file
(
Filename
.
basename
fin
)
".out"
in
let
fd_out
=
Unix
.
descr_of_out_channel
cout
in
fout
,
cout
,
fd_out
,
fd_out
else
...
...
@@ -287,7 +291,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
in
{
call
=
call
;
pid
=
pid
}
let
call_on_buffer
~
command
?
(
timelimit
=
0
)
?
(
memlimit
=
0
)
?
(
step
s
limit
=
(
-
1
))
let
call_on_buffer
~
command
?
(
timelimit
=
0
)
?
(
memlimit
=
0
)
?
(
steplimit
=
(
-
1
))
~
res_parser
~
filename
~
printer_mapping
?
(
inplace
=
false
)
buffer
=
...
...
@@ -299,7 +303,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0) ?(stepslimit=(-1))
end
else
Filename
.
open_temp_file
"why_"
(
"_"
^
filename
)
in
Buffer
.
output_buffer
cin
buffer
;
close_out
cin
;
call_on_file
~
command
~
timelimit
~
memlimit
~
step
s
limit
call_on_file
~
command
~
timelimit
~
memlimit
~
steplimit
~
res_parser
~
printer_mapping
~
cleanup
:
true
~
inplace
fin
let
query_call
pc
=
...
...
src/driver/call_provers.mli
View file @
208c71dc
...
...
@@ -22,7 +22,7 @@ type prover_answer =
(** the task timeouts, ie it takes more time than specified *)
|
OutOfMemory
(** the task runs out of memory *)
|
Step
s
LimitExceeded
|
StepLimitExceeded
(** the task required more steps than the limit provided *)
|
Unknown
of
string
(** The prover can't determine if the task is valid *)
...
...
@@ -63,21 +63,21 @@ val debug : Debug.flag
type
timeregexp
(** The type of precompiled regular expressions for time parsing *)
type
step
s
regexp
type
stepregexp
(** The type of precompiled regular expressions for parsing of steps *)
val
timeregexp
:
string
->
timeregexp
(** Converts a regular expression with special markers '%h','%m',
'%s','%i' (for milliseconds) into a value of type [timeregexp] *)
val
step
s
regexp
:
string
->
int
->
step
s
regexp
(** step
s
regexp s n creates a regular expression
for
match
ing
number of steps.
s
is regular expression,
n
is
a
group number with steps
information
*)
val
stepregexp
:
string
->
int
->
stepregexp
(**
[
stepregexp s n
]
creates a regular expression
to
match
the
number of steps.
[s]
is
a
regular expression,
[n]
is
the
group number with steps
number.
*)
type
prover_result_parser
=
{
prp_regexps
:
(
Str
.
regexp
*
prover_answer
)
list
;
prp_timeregexps
:
timeregexp
list
;
prp_step
s
regexp
:
step
s
regexp
list
;
prp_stepregexp
s
:
stepregexp
list
;
prp_exitcodes
:
(
int
*
prover_answer
)
list
;
(* The parser for a model returned by the solver. *)
prp_model_parser
:
Model_parser
.
model_parser
;
...
...
@@ -96,7 +96,7 @@ val call_on_file :
command
:
string
->
?
timelimit
:
int
->
?
memlimit
:
int
->
?
step
s
limit
:
int
->
?
steplimit
:
int
->
res_parser
:
prover_result_parser
->
printer_mapping
:
Printer
.
printer_mapping
->
?
cleanup
:
bool
->
...
...
@@ -108,7 +108,7 @@ val call_on_buffer :
command
:
string
->
?
timelimit
:
int
->
?
memlimit
:
int
->
?
step
s
limit
:
int
->
?
steplimit
:
int
->
res_parser
:
prover_result_parser
->
filename
:
string
->
printer_mapping
:
Printer
.
printer_mapping
->
...
...
@@ -117,7 +117,8 @@ val call_on_buffer :
(** Call a prover on the task printed in the {!type: Buffer.t} given.
@param timelimit : set the available time limit (def. 0 : unlimited)
@param memlimit : set the available time limit (def. 0 : unlimited)
@param memlimit : set the available memory limit (def. 0 : unlimited)
@param steplimit : set the available step limit (def. -1 : unlimited)
@param regexps : if the first field matches the prover output,
the second field is the answer. Regexp groups present in
...
...
src/driver/driver.ml
View file @
208c71dc
...
...
@@ -76,7 +76,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
let
model_parser
=
ref
"no_model"
in
let
transform
=
ref
[]
in
let
timeregexps
=
ref
[]
in
let
step
s
regexps
=
ref
[]
in
let
stepregexps
=
ref
[]
in
let
blacklist
=
Queue
.
create
()
in
let
set_or_raise
loc
r
v
error
=
match
!
r
with
...
...
@@ -90,19 +90,19 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
|
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
)
|
RegexpStep
s
LimitExceeded
s
->
add_to_list
regexps
(
Str
.
regexp
s
,
Step
s
LimitExceeded
)
|
RegexpStepLimitExceeded
s
->
add_to_list
regexps
(
Str
.
regexp
s
,
StepLimitExceeded
)
|
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
)
|
StepRegexp
(
r
,
ns
)
->
add_to_list
step
s
regexps
(
Call_provers
.
step
s
regexp
r
ns
)
add_to_list
stepregexps
(
Call_provers
.
stepregexp
r
ns
)
|
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
)
|
ExitCodeStep
s
LimitExceeded
s
->
add_to_list
exitcodes
(
s
,
Step
s
LimitExceeded
)
|
ExitCodeStepLimitExceeded
s
->
add_to_list
exitcodes
(
s
,
StepLimitExceeded
)
|
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"
...
...
@@ -206,7 +206,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
{
prp_regexps
=
List
.
rev
!
regexps
;
prp_timeregexps
=
List
.
rev
!
timeregexps
;
prp_step
s
regexp
=
List
.
rev
!
step
s
regexps
;
prp_stepregexp
s
=
List
.
rev
!
stepregexps
;
prp_exitcodes
=
List
.
rev
!
exitcodes
;
prp_model_parser
=
Model_parser
.
lookup_model_parser
!
model_parser
};
...
...
@@ -245,9 +245,10 @@ 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
?
stepslimit
?
inplace
~
filename
~
printer_mapping
drv
buffer
=
let
call_on_buffer
~
command
?
timelimit
?
memlimit
?
steplimit
?
inplace
~
filename
~
printer_mapping
drv
buffer
=
Call_provers
.
call_on_buffer
~
command
?
timelimit
?
memlimit
?
step
s
limit
~
res_parser
:
drv
.
drv_res_parser
~
command
?
timelimit
?
memlimit
?
steplimit
~
res_parser
:
drv
.
drv_res_parser
~
filename
~
printer_mapping
?
inplace
buffer
...
...
@@ -308,7 +309,7 @@ let print_theory ?old drv fmt th =
print_task
?
old
drv
fmt
task
let
prove_task_prepared
~
command
?
timelimit
?
memlimit
?
step
s
limit
?
old
?
inplace
drv
task
=
~
command
?
timelimit
?
memlimit
?
steplimit
?
old
?
inplace
drv
task
=
let
buf
=
Buffer
.
create
1024
in
let
fmt
=
formatter_of_buffer
buf
in
let
old_channel
=
Opt
.
map
open_in
old
in
...
...
@@ -326,13 +327,15 @@ let prove_task_prepared
get_filename
drv
fn
"T"
pr
.
pr_name
.
id_string
in
let
res
=
call_on_buffer
~
command
?
timelimit
?
memlimit
?
stepslimit
?
inplace
~
filename
~
printer_mapping
drv
buf
in
call_on_buffer
~
command
?
timelimit
?
memlimit
?
steplimit
?
inplace
~
filename
~
printer_mapping
drv
buf
in
Buffer
.
reset
buf
;
res
let
prove_task
~
command
?
timelimit
?
memlimit
?
step
s
limit
?
old
?
inplace
drv
task
=
let
prove_task
~
command
?
timelimit
?
memlimit
?
steplimit
?
old
?
inplace
drv
task
=
let
task
=
prepare_task
drv
task
in
prove_task_prepared
~
command
?
timelimit
?
memlimit
?
stepslimit
?
old
?
inplace
drv
task
prove_task_prepared
~
command
?
timelimit
?
memlimit
?
steplimit
?
old
?
inplace
drv
task
(* exception report *)
...
...
src/driver/driver.mli
View file @
208c71dc
...
...
@@ -38,7 +38,7 @@ val call_on_buffer :
command
:
string
->
?
timelimit
:
int
->
?
memlimit
:
int
->
?
step
s
limit
:
int
->
?
steplimit
:
int
->
?
inplace
:
bool
->
filename
:
string
->
printer_mapping
:
Printer
.
printer_mapping
->
...
...
@@ -58,7 +58,7 @@ val prove_task :
command
:
string
->
?
timelimit
:
int
->
?
memlimit
:
int
->
?
step
s
limit
:
int
->
?
steplimit
:
int
->
?
old
:
string
->
?
inplace
:
bool
->
driver
->
Task
.
task
->
Call_provers
.
pre_prover_call
...
...
@@ -74,7 +74,7 @@ val prove_task_prepared :
command
:
string
->
?
timelimit
:
int
->
?
memlimit
:
int
->
?
step
s
limit
:
int
->
?
steplimit
:
int
->
?
old
:
string
->
?
inplace
:
bool
->
driver
->
Task
.
task
->
Call_provers
.
pre_prover_call
...
...
src/driver/driver_ast.ml
View file @
208c71dc
...
...
@@ -58,7 +58,7 @@ type global =
|
RegexpInvalid
of
string
|
RegexpTimeout
of
string
|
RegexpOutOfMemory
of
string
|
RegexpStep
s
LimitExceeded
of
string
|
RegexpStepLimitExceeded
of
string
|
RegexpUnknown
of
string
*
string
|
RegexpFailure
of
string
*
string
|
TimeRegexp
of
string
...
...
@@ -67,7 +67,7 @@ type global =
|
ExitCodeInvalid
of
int
|
ExitCodeTimeout
of
int
|
ExitCodeOutOfMemory
of
int
|
ExitCodeStep
s
LimitExceeded
of
int
|
ExitCodeStepLimitExceeded
of
int
|
ExitCodeUnknown
of
int
*
string
|
ExitCodeFailure
of
int
*
string
|
Filename
of
string
...
...
src/driver/driver_lexer.mll
View file @
208c71dc
...
...
@@ -37,7 +37,7 @@
"invalid"
,
INVALID
;
"timeout"
,
TIMEOUT
;
"outofmemory"
,
OUTOFMEMORY
;
"step
s
limitexceeded"
,
STEP
S
LIMITEXCEEDED
;
"steplimitexceeded"
,
STEPLIMITEXCEEDED
;
"time"
,
TIME
;
"unknown"
,
UNKNOWN
;
"fail"
,
FAIL
;
...
...
src/driver/driver_parser.mly
View file @
208c71dc
...
...
@@ -24,7 +24,7 @@
%
token
<
string
>
INPUT
(* never reaches the parser *)
%
token
THEORY
END
SYNTAX
REMOVE
META
PRELUDE
PRINTER
MODEL_PARSER
%
token
VALID
INVALID
UNKNOWN
FAIL
%
token
TIMEOUT
OUTOFMEMORY
STEP
S
LIMITEXCEEDED
TIME
STEPS
%
token
TIMEOUT
OUTOFMEMORY
STEPLIMITEXCEEDED
TIME
STEPS
%
token
UNDERSCORE
LEFTPAR
RIGHTPAR
DOT
QUOTE
EOF
%
token
BLACKLIST
%
token
MODULE
EXCEPTION
VAL
CONVERTER
...
...
@@ -57,7 +57,7 @@ global:
|
INVALID
STRING
{
RegexpInvalid
$
2
}
|
TIMEOUT
STRING
{
RegexpTimeout
$
2
}
|
OUTOFMEMORY
STRING
{
RegexpOutOfMemory
$
2
}
|
STEP
S
LIMITEXCEEDED
STRING
{
RegexpStep
s
LimitExceeded
$
2
}
|
STEPLIMITEXCEEDED
STRING
{
RegexpStepLimitExceeded
$
2
}
|
TIME
STRING
{
TimeRegexp
$
2
}
|
STEPS
STRING
INTEGER
{
StepRegexp
(
$
2
,
$
3
)
}
|
UNKNOWN
STRING
STRING
{
RegexpUnknown
(
$
2
,
$
3
)
}
...
...
@@ -65,7 +65,7 @@ global:
|
VALID
INTEGER
{
ExitCodeValid
$
2
}
|
INVALID
INTEGER
{
ExitCodeInvalid
$
2
}
|
TIMEOUT
INTEGER
{
ExitCodeTimeout
$
2
}
|
STEP
S
LIMITEXCEEDED
INTEGER
{
ExitCodeStep
s
LimitExceeded
$
2
}
|
STEPLIMITEXCEEDED
INTEGER
{
ExitCodeStepLimitExceeded
$
2
}
|
UNKNOWN
INTEGER
STRING
{
ExitCodeUnknown
(
$
2
,
$
3
)
}
|
FAIL
INTEGER
STRING
{
ExitCodeFailure
(
$
2
,
$
3
)
}
|
FILENAME
STRING
{
Filename
$
2
}
...
...
src/driver/whyconf.ml
View file @
208c71dc
...
...
@@ -206,11 +206,13 @@ let running_provers_max m = m.running_provers_max
exception
StepsCommandNotSpecified
of
string
let
get_complete_command
pc
step
s
limit
=
let
comm
=
if
step
s
limit
<
0
then
pc
.
command
let
get_complete_command
pc
steplimit
=
let
comm
=
if
steplimit
<
0
then
pc
.
command
else
match
pc
.
command_steps
with
|
None
->
raise
(
StepsCommandNotSpecified
"The solver is used with step limit and the command for running the solver with steplimit is not specified."
)
|
None
->
raise
(
StepsCommandNotSpecified
"The solver is used with a step limit and the command for \
running the solver with a step limit is not specified."
)
|
Some
command_steps
->
command_steps
in
String
.
concat
" "
(
comm
::
pc
.
extra_options
)
...
...
src/ide/gconfig.ml
View file @
208c71dc
...
...
@@ -287,14 +287,14 @@ 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_step
s
limitexceeded
=
ref
!
image_default
let
image_steplimitexceeded
=
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_step
s
limitexceeded_obs
=
ref
!
image_default
let
image_steplimitexceeded_obs
=
ref
!
image_default
let
image_failure_obs
=
ref
!
image_default
let
image_yes
=
ref
!
image_default
let
image_no
=
ref
!
image_default
...
...
@@ -334,14 +334,14 @@ let iconname_unknown = ref ""
let
iconname_invalid
=
ref
""
let
iconname_timeout
=
ref
""
let
iconname_outofmemory
=
ref
""
let
iconname_step
s
limitexceeded
=
ref
""
let
iconname_steplimitexceeded
=
ref
""
let
iconname_failure
=
ref
""
let
iconname_valid_obs
=
ref
""
let
iconname_unknown_obs
=
ref
""
let
iconname_invalid_obs
=
ref
""
let
iconname_timeout_obs
=
ref
""
let
iconname_outofmemory_obs
=
ref
""
let
iconname_step
s
limitexceeded_obs
=
ref
""
let
iconname_steplimitexceeded_obs
=
ref
""
let
iconname_failure_obs
=
ref
""
let
iconname_yes
=
ref
""
let
iconname_no
=
ref
""
...
...
@@ -391,14 +391,14 @@ let load_icon_names () =
iconname_invalid
:=
get_icon_name
"invalid"
;
iconname_timeout
:=
get_icon_name
"timeout"
;
iconname_outofmemory
:=
get_icon_name
"outofmemory"
;
iconname_step
s
limitexceeded
:=
get_icon_name
"step
s
limitexceeded"
;
iconname_steplimitexceeded
:=
get_icon_name
"steplimitexceeded"
;
iconname_failure
:=
get_icon_name
"failure"
;
iconname_valid_obs
:=
get_icon_name
"valid_obs"
;
iconname_unknown_obs
:=
get_icon_name
"unknown_obs"
;
iconname_invalid_obs
:=
get_icon_name
"invalid_obs"
;
iconname_timeout_obs
:=
get_icon_name
"timeout_obs"
;
iconname_outofmemory_obs
:=
get_icon_name
"outofmemory_obs"
;
iconname_step
s
limitexceeded_obs
:=
get_icon_name
"step
s
limitexceeded_obs"
;
iconname_steplimitexceeded_obs
:=
get_icon_name
"steplimitexceeded_obs"
;
iconname_failure_obs
:=
get_icon_name
"failure_obs"
;
iconname_yes
:=
get_icon_name
"yes"
;
iconname_no
:=
get_icon_name
"no"
;
...
...
@@ -426,14 +426,14 @@ let resize_images size =
image_invalid
:=
image
~
size
!
iconname_invalid
;
image_timeout
:=
image
~
size
!
iconname_timeout
;
image_outofmemory
:=
image
~
size
!
iconname_outofmemory
;
image_step
s
limitexceeded
:=
image
~
size
!
iconname_step
s
limitexceeded
;
image_steplimitexceeded
:=
image
~
size
!
iconname_steplimitexceeded
;
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_step
s
limitexceeded_obs
:=
image
~
size
!
iconname_step
s
limitexceeded_obs
;
image_steplimitexceeded_obs
:=
image
~
size
!
iconname_steplimitexceeded_obs
;
image_failure_obs
:=
image
~
size
!
iconname_failure_obs
;
image_yes
:=
image
~
size
!
iconname_yes
;
image_no
:=
image
~
size
!
iconname_no
;
...
...
@@ -499,8 +499,8 @@ let show_legend_window () =
i
" External prover reached the time limit
\n
"
;
ib
image_outofmemory
;
i
" External prover ran out of memory
\n
"
;
ib
image_step
s
limitexceeded
;
i
" External prover exceeded the step
s
limit
\n
"
;
ib
image_steplimitexceeded
;
i
" External prover exceeded the step limit
\n
"
;
ib
image_unknown
;
i
" External prover answer not conclusive
\n
"
;
ib
image_failure
;
...
...
src/ide/gconfig.mli
View file @
208c71dc
...
...
@@ -89,14 +89,14 @@ 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_step
s
limitexceeded
:
GdkPixbuf
.
pixbuf
ref
val
image_steplimitexceeded
:
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_step
s
limitexceeded_obs
:
GdkPixbuf
.
pixbuf
ref
val
image_steplimitexceeded_obs
:
GdkPixbuf
.
pixbuf
ref
val
image_unknown_obs
:
GdkPixbuf
.
pixbuf
ref
val
image_failure_obs
:
GdkPixbuf
.
pixbuf
ref
...
...
src/ide/gmain.ml
View file @
208c71dc
...
...
@@ -446,9 +446,9 @@ let image_of_result ~obsolete result =
if
obsolete
then
!
image_timeout_obs
else
!
image_timeout
|
Call_provers
.
OutOfMemory
->
if
obsolete
then
!
image_outofmemory_obs
else
!
image_outofmemory
|
Call_provers
.
Step
s
LimitExceeded
->
if
obsolete
then
!
image_step
s
limitexceeded_obs
else
!
image_step
s
limitexceeded
|
Call_provers
.
StepLimitExceeded
->
if
obsolete
then
!
image_steplimitexceeded_obs
else
!
image_steplimitexceeded
|
Call_provers
.
Unknown
_
->
if
obsolete
then
!
image_unknown_obs
else
!
image_unknown
|
Call_provers
.
Failure
_
->
...
...
@@ -1120,7 +1120,7 @@ let bisect_proof_attempt pa =
M
.
schedule_proof_attempt
~
timelimit
:!
timelimit
~
memlimit
:
pa
.
S
.
proof_memlimit
~
step
s
limit
:
(
-
1
)
~
steplimit
:
(
-
1
)
?
old
:
(
S
.
get_edited_as_abs
eS
.
S
.
session
pa
)
(** It is dangerous, isn't it? to be in place for bisecting? *)
~
inplace
:
lp
.
S
.
prover_config
.
C
.
in_place
...
...
@@ -1158,7 +1158,7 @@ let bisect_proof_attempt pa =
M
.
schedule_proof_attempt
~
timelimit
:!
timelimit
~
memlimit
:
pa
.
S
.
proof_memlimit
~
step
s
limit
:
(
-
1
)
~
steplimit
:
(
-
1
)
?
old
:
(
S
.
get_edited_as_abs
eS
.
S
.
session
pa
)
~
inplace
:
lp
.
S
.
prover_config
.
C
.
in_place
~
command
:
(
C
.
get_complete_command
lp
.
S
.
prover_config
(
-
1
))
...
...
src/session/session.ml
View file @
208c71dc
...
...
@@ -553,7 +553,7 @@ let save_result fmt r =
|
Call_provers
.
HighFailure
->
"highfailure"
|
Call_provers
.
Timeout
->
"timeout"
|
Call_provers
.
OutOfMemory
->
"outofmemory"
|
Call_provers
.
Step
s
LimitExceeded
->
"step
s
limitexceeded"
|
Call_provers
.
StepLimitExceeded
->
"steplimitexceeded"
|
Call_provers
.
Invalid
->
"invalid"
)
r
.
Call_provers
.
pr_time
(
opt
pp_print_int
"steps"
)
steps
...
...
@@ -1173,7 +1173,8 @@ let load_result r =
|
"outofmemory"
->
Call_provers
.
OutOfMemory
|
"failure"
->
Call_provers
.
Failure
""
|
"highfailure"
->
Call_provers
.
HighFailure
|
"stepslimitexceeded"
->
Call_provers
.
StepsLimitExceeded
|
"steplimitexceeded"
->
Call_provers
.
StepLimitExceeded
|
"stepslimitexceeded"
->
Call_provers
.
StepLimitExceeded
|
s
->
Warning
.
emit
"[Warning] Session.load_result: unexpected status '%s'@."
s
;
...
...
src/session/session_scheduler.ml
View file @
208c71dc
...
...
@@ -209,13 +209,13 @@ let idle_handler t =
if
Queue
.
length
t
.
proof_attempts_queue
<
3
*
t
.
maximum_running_proofs
then
begin