Commit 9d76a5cd authored by François Bobot's avatar François Bobot

increase magic number, pvs version < 5, message for old version

parent a07707c1
...@@ -286,6 +286,7 @@ exec = "pvs" ...@@ -286,6 +286,7 @@ exec = "pvs"
version_switch = "-version" version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)" version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "5.0" version_ok = "5.0"
version_old = "^[0-4]\..*"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f" command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
driver = "drivers/pvs.drv" driver = "drivers/pvs.drv"
in_place = true in_place = true
......
...@@ -89,7 +89,7 @@ let prover_keys = ...@@ -89,7 +89,7 @@ let prover_keys =
let load_prover kind (id,section) = let load_prover kind (id,section) =
check_exhaustive section prover_keys; check_exhaustive section prover_keys;
let reg_map = List.rev_map why3_regexp_of_string in let reg_map = List.rev_map why3_regexp_of_string in
{ kind = kind; let prover = { kind = kind;
prover_id = id; prover_id = id;
prover_name = get_string section "name"; prover_name = get_string section "name";
prover_altern = get_string section ~default:"" "altern"; prover_altern = get_string section ~default:"" "altern";
...@@ -100,11 +100,15 @@ let load_prover kind (id,section) = ...@@ -100,11 +100,15 @@ let load_prover kind (id,section) =
versions_old = reg_map $ get_stringl section ~default:[] "version_old"; versions_old = reg_map $ get_stringl section ~default:[] "version_old";
versions_bad = reg_map $ get_stringl section ~default:[] "version_bad"; versions_bad = reg_map $ get_stringl section ~default:[] "version_bad";
prover_command = get_stringo section "command"; prover_command = get_stringo section "command";
prover_driver = get_string section "driver"; prover_driver = get_string section ~default:"" "driver";
prover_editor = get_string section ~default:"" "editor"; prover_editor = get_string section ~default:"" "editor";
prover_in_place = get_bool section ~default:false "in_place"; prover_in_place = get_bool section ~default:false "in_place";
message = get_stringo section "message"; message = get_stringo section "message";
} } in
if prover.prover_command != None && prover.prover_driver = "" then
invalid_arg
(sprintf "In section prover %s command specified without driver" id);
prover
let editor_keys = let editor_keys =
let add acc k = Sstr.add k acc in let add acc k = Sstr.add k acc in
...@@ -346,7 +350,9 @@ let detect_exec env main data acc exec_name = ...@@ -346,7 +350,9 @@ let detect_exec env main data acc exec_name =
if good || old then begin if good || old then begin
eprintf "Found prover %s version %s%s@." eprintf "Found prover %s version %s%s@."
data.prover_name ver data.prover_name ver
(def_option (if old then " (it is an old version)." else ", Ok.") (def_option (if old then
" (it is an old version that is less tested than \
the current one)." else ", Ok.")
data.message); data.message);
known_version env exec_name; known_version env exec_name;
add_prover_shortcuts env prover; add_prover_shortcuts env prover;
......
...@@ -35,10 +35,11 @@ open Stdlib ...@@ -35,10 +35,11 @@ open Stdlib
- 10 require %f in editor lines - 10 require %f in editor lines
- 11 change prover identifiers in provers-detection-data.conf - 11 change prover identifiers in provers-detection-data.conf
- 12 split editors out of provers - 12 split editors out of provers
- 13 add shortcuts
If a configuration doesn't contain the actual magic number we don't use it.*) If a configuration doesn't contain the actual magic number we don't use it.*)
let magicnumber = 12 let magicnumber = 13
exception WrongMagicNumber exception WrongMagicNumber
......
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