Commit 34578b05 authored by David Hauzar's avatar David Hauzar

Fix of failure in_of_string on Windows.

The file of the form "file:line:col1:col2" was created, than split on ":"
and and int_of_string was used to get line number and colon numbers. This
failed on windows because the file name contained ':', i.e.,
"C:\...\gnatprove\p\..\p.mlw:2254:55:150".
parent 763d4d0d
......@@ -194,16 +194,27 @@ let () = Trans.register_transform "intro_vc_vars_counterexmp"
intro_vc_vars_counterexmp
~desc:"Introduce."
let rec string_join sep l =
match l with
| [] -> ""
| [x] -> x
| x :: rest -> x ^ sep ^ string_join sep rest
let get_location_of_vc task =
let meta_args = Task.on_meta_excl meta_vc_location task in
match meta_args with
| Some [Theory.MAstr loc_str] ->
let splitted = Strings.bounded_split ':' loc_str 4 in
let loc = match splitted with
| [filename; line; col1; col2] ->
(* There may be colons in the file name. We still split on the colon, look at
the last three elements, and put the remaining ones back together to form the
file name. We may lose colons at the beginning or end of the filename, but
even on windows that's not allowed. *)
let split = Strings.rev_split ':' loc_str in
let loc = match split with
| col2 :: col1 :: line :: (_ :: _) as rest ->
let line = int_of_string line in
let col1 = int_of_string col1 in
let col2 = int_of_string col2 in
let filename = string_join ":" (List.rev rest) in
Some (Loc.user_position filename line col1 col2)
| _ -> None in
loc
......
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