Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
9f77a2ab
Commit
9f77a2ab
authored
Mar 15, 2016
by
Johannes Kanig
Browse files
P114-013 set steps default value to 0
parent
50a9b62a
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/driver/call_provers.ml
View file @
9f77a2ab
...
...
@@ -51,12 +51,12 @@ let empty_limit =
let
get_time
x
=
Opt
.
get_def
0
x
.
limit_time
let
get_mem
x
=
Opt
.
get_def
0
x
.
limit_mem
let
get_steps
x
=
Opt
.
get_def
(
-
1
)
x
.
limit_steps
let
get_steps
x
=
Opt
.
get_def
0
x
.
limit_steps
let
mk_limit
t
m
s
=
{
limit_time
=
if
t
=
0
then
None
else
Some
t
;
limit_mem
=
if
m
=
0
then
None
else
Some
m
;
limit_steps
=
if
s
=
-
1
then
None
else
Some
s
limit_steps
=
if
s
=
0
then
None
else
Some
s
}
let
limit_max
a
b
=
...
...
src/driver/call_provers.mli
View file @
9f77a2ab
...
...
@@ -139,7 +139,7 @@ val get_time : resource_limit -> int
val
get_mem
:
resource_limit
->
int
(* return time, return default value 0 if not set *)
val
get_steps
:
resource_limit
->
int
(* return time, return default value
(-1)
if not set *)
(* return time, return default value
0
if not set *)
val
mk_limit
:
int
->
int
->
int
->
resource_limit
(* build a limit object, transforming the default values into None on the fly
...
...
src/session/session_scheduler.ml
View file @
9f77a2ab
...
...
@@ -422,22 +422,22 @@ let adapt_limits ~use_steps a =
let
increased_mem
=
3
*
memlimit
/
2
in
begin
match
r
with
|
Call_provers
.
OutOfMemory
->
increased_time
,
memlimit
,
-
1
|
Call_provers
.
Timeout
->
timelimit
,
increased_mem
,
-
1
|
Call_provers
.
OutOfMemory
->
increased_time
,
memlimit
,
0
|
Call_provers
.
Timeout
->
timelimit
,
increased_mem
,
0
|
Call_provers
.
Valid
->
let
steplimit
=
if
use_steps
&&
not
a
.
proof_obsolete
then
s
else
-
1
if
use_steps
&&
not
a
.
proof_obsolete
then
s
else
0
in
increased_time
,
increased_mem
,
steplimit
|
Call_provers
.
Unknown
_
|
Call_provers
.
StepLimitExceeded
|
Call_provers
.
Invalid
->
increased_time
,
increased_mem
,
-
1
|
Call_provers
.
Invalid
->
increased_time
,
increased_mem
,
0
|
Call_provers
.
Failure
_
|
Call_provers
.
HighFailure
->
(* correct ? failures are supposed to appear quickly anyway... *)
timelimit
,
memlimit
,
-
1
timelimit
,
memlimit
,
0
end
|
_
->
timelimit
,
memlimit
,
-
1
|
_
->
timelimit
,
memlimit
,
0
let
adapt_limits
~
use_steps
a
=
let
t
,
m
,
s
=
adapt_limits
~
use_steps
a
in
...
...
src/tools/why3replay.ml
View file @
9f77a2ab
...
...
@@ -400,7 +400,7 @@ let run_as_bench env_session =
eprintf
" done.@."
;
exit
0
in
let
limit
=
Call_provers
.
mk_limit
2
0
(
-
1
)
in
let
limit
=
Call_provers
.
mk_limit
2
0
0
in
M
.
play_all
env_session
sched
~
callback
~
limit
provers
;
main_loop
()
;
eprintf
"main replayer (in bench mode) exited unexpectedly@."
;
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment