Skip to content
GitLab
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
7d8f58e4
Commit
7d8f58e4
authored
Jul 20, 2012
by
François Bobot
Browse files
autodetection: version_ok, version_bad, version_old can be a regexp. regexp must start with ^
parent
48685ba9
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/driver/autodetection.ml
View file @
7d8f58e4
...
...
@@ -44,6 +44,8 @@ the version is old (version_old).
The field command can be missing in a block, in that case the block
defines a version known to be buggy: no prover config is generated.
The regexp must start with ^.
*)
open
Format
...
...
@@ -66,9 +68,9 @@ type prover_autodetection_data =
execs
:
string
list
;
version_switch
:
string
;
version_regexp
:
string
;
versions_ok
:
s
tr
ing
list
;
versions_old
:
s
tr
ing
list
;
versions_bad
:
s
tr
ing
list
;
versions_ok
:
S
tr
.
regexp
list
;
versions_old
:
S
tr
.
regexp
list
;
versions_bad
:
S
tr
.
regexp
list
;
(** If none it's a fake prover (very bad version) *)
prover_command
:
string
option
;
prover_driver
:
string
;
...
...
@@ -86,6 +88,8 @@ let prover_keys =
let
load_prover
kind
(
id
,
section
)
=
check_exhaustive
section
prover_keys
;
let
reg_map
=
List
.
rev_map
(
fun
s
->
if
s
.
[
0
]
=
'
^
'
then
Str
.
regexp
s
else
Str
.
regexp_string
s
)
in
{
kind
=
kind
;
prover_id
=
id
;
prover_name
=
get_string
section
"name"
;
...
...
@@ -93,9 +97,9 @@ let load_prover kind (id,section) =
execs
=
get_stringl
section
"exec"
;
version_switch
=
get_string
section
~
default
:
""
"version_switch"
;
version_regexp
=
get_string
section
~
default
:
""
"version_regexp"
;
versions_ok
=
get_stringl
section
~
default
:
[]
"version_ok"
;
versions_old
=
get_stringl
section
~
default
:
[]
"version_old"
;
versions_bad
=
get_stringl
section
~
default
:
[]
"version_bad"
;
versions_ok
=
reg_map
$
get_stringl
section
~
default
:
[]
"version_ok"
;
versions_old
=
reg_map
$
get_stringl
section
~
default
:
[]
"version_old"
;
versions_bad
=
reg_map
$
get_stringl
section
~
default
:
[]
"version_bad"
;
prover_command
=
get_stringo
section
"command"
;
prover_driver
=
get_string
section
"driver"
;
prover_editor
=
get_string
section
~
default
:
""
"editor"
;
...
...
@@ -151,13 +155,14 @@ let read_editors main =
|
Not_found
->
Loc
.
errorm
"provers-detection-data.conf not found at %s@."
filename
let
make_command
exec
com
=
let
make_command
=
let
cmd_regexp
=
Str
.
regexp
"%
\\
(.
\\
)"
in
let
replace
s
=
match
Str
.
matched_group
1
s
with
|
"e"
->
exec
|
c
->
"%"
^
c
in
Str
.
global_substitute
cmd_regexp
replace
com
fun
exec
com
->
let
replace
s
=
match
Str
.
matched_group
1
s
with
|
"e"
->
exec
|
c
->
"%"
^
c
in
Str
.
global_substitute
cmd_regexp
replace
com
let
sanitize_exec
=
let
first
c
=
match
c
with
...
...
@@ -213,7 +218,9 @@ let ask_prover_version env exec_name version_switch =
Hashtbl
.
replace
env
.
prover_output
(
exec_name
,
version_switch
)
res
;
res
let
check_version
(
version
:
string
)
schema
=
schema
=
version
let
check_version
version
schema
=
Str
.
string_match
schema
version
0
&&
Str
.
match_end
()
=
String
.
length
version
let
known_version
env
exec_name
=
Hashtbl
.
replace
env
.
prover_unknown_version
exec_name
None
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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