Commit a1f3e192 authored by Andrei Paskevich's avatar Andrei Paskevich

split prover's commandline into args

parent 63115308
......@@ -113,7 +113,7 @@ LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
src/driver/driver_lexer.ml
LIB_UTIL = stdlib exn_printer debug pp loc print_tree \
hashweak hashcons util sysutil rc plugin
cmdline hashweak hashcons util sysutil rc plugin
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
......
......@@ -155,10 +155,10 @@ let main () =
with
| Rc.CannotOpen (f, s)
| Whyconf.ConfigFailure (f, s) ->
autoprovers := true;
autoplugins := true;
eprintf "warning: cannot read config file %s (%s)@." f s;
default_config f
eprintf "warning: cannot read config file %s:@\n %s@." f s;
autoprovers := true;
autoplugins := true;
default_config f
in
let main = get_main config in
(* let main = option_apply main (fun d -> {main with libdir = d})
......
......@@ -159,6 +159,7 @@ let detect_prover main acc0 data =
{name = data.prover_name;
version = ver;
command = c;
command_split = Cmdline.cmdline_split c;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor} acc
with Not_found ->
......
......@@ -51,6 +51,7 @@ type config_prover = {
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string;
command_split : string list; (* "why3-cpulimit" "%t" "%m" "alt-ergo" "%f" *)
}
type main = {
......@@ -175,6 +176,7 @@ let load_prover dirname provers (id,section) =
driver = absolute_filename dirname (get_string section "driver");
version = get_string ~default:"" section "version";
editor = get_string ~default:"" section "editor";
command_split = Cmdline.cmdline_split (get_string section "command");
} provers
let load_main dirname section =
......@@ -206,6 +208,8 @@ exception ConfigFailure of string (* filename *) * string
let () = Exn_printer.register (fun fmt e -> match e with
| ConfigFailure (f, s) ->
Format.fprintf fmt "error in config file %s: %s" f s
| WrongMagicNumber ->
Format.fprintf fmt "outdated config file; rerun why3config"
| _ -> raise e)
let get_config (filename,rc) =
......@@ -235,9 +239,10 @@ let read_config conf_file =
in
try
get_config filenamerc
with WrongMagicNumber ->
let filename, _ = filenamerc in
raise (ConfigFailure (filename, "outdated config file; rerun why3config"))
with e when not (Debug.test_flag Debug.stack_trace) ->
let b = Buffer.create 40 in
Format.bprintf b "%a" Exn_printer.exn_printer e;
raise (ConfigFailure (fst filenamerc, Buffer.contents b))
let save_config config =
let filename = config.conf_file in
......
......@@ -50,7 +50,6 @@ val default_config : string -> config
(** [ default_config filename ] create a default configuration which is going
to be saved in [ filename ]*)
val get_conf_file : config -> string
(** [get_conf_file config] get the rc file corresponding to this
configuration *)
......@@ -89,6 +88,7 @@ type config_prover = {
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string; (* Interative theorem prover *)
command_split : string list; (* "why3-cpulimit" "%t" "%m" "alt-ergo" "%f" *)
}
val get_provers : config -> config_prover Mstr.t
......
......@@ -151,6 +151,7 @@ let save_config t =
driver = pr.driver_name;
version = pr.prover_version;
editor = pr.editor;
command_split = Cmdline.cmdline_split pr.command;
} acc in
let config = t.config in
let config = set_main config
......
(**************************************************************************)
(* *)
(* Copyright (C) 2011- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
exception BadEscape of string * char
exception UnfinishedEscape of string
exception UnclosedQuote of string
exception UnclosedDQuote of string
exception EmptyCommandLine
let is_blank = function
| ' ' | '\t' | '\n' | '\r' -> true
| _ -> false
let escape s c = match c with
| 't' -> '\t' | 'n' -> '\n' | 'r' -> '\r'
| '\'' | '"' | '\\' | ' ' -> c
| _ -> raise (BadEscape (s,c))
type fsm_state =
| Normal
| Blank
| Quote
| DQuote
| Escape
| QEscape
| DQEscape
let cmdline_split s =
let argv = ref [] in
let cur_arg = Queue.create () in
let cstate = ref Blank in
let normal = function
| '\'' -> cstate := Quote
| '"' -> cstate := DQuote
| '\\' -> cstate := Escape
| c when is_blank c ->
let n = Queue.length cur_arg in
let s = String.create n in
for i = 0 to pred n do
String.set s i (Queue.take cur_arg)
done;
argv := s :: !argv;
cstate := Blank
| c -> Queue.add c cur_arg
in
let blank = function
| '\'' -> cstate := Quote
| '"' -> cstate := DQuote
| '\\' -> cstate := Escape
| c when is_blank c -> ()
| c -> Queue.add c cur_arg; cstate := Normal
in
let quote = function
| '\'' -> cstate := Normal
| '\\' -> cstate := QEscape
| c -> Queue.add c cur_arg
in
let dquote = function
| '"' -> cstate := Normal
| '\\' -> cstate := DQEscape
| c -> Queue.add c cur_arg
in
let fsm c = match !cstate with
| Normal -> normal c
| Blank -> blank c
| Quote -> quote c
| DQuote -> dquote c
| Escape -> Queue.add (escape s c) cur_arg; cstate := Normal
| QEscape -> Queue.add (escape s c) cur_arg; cstate := Quote
| DQEscape -> Queue.add (escape s c) cur_arg; cstate := DQuote
in
String.iter fsm s;
fsm ' ';
match !cstate with
| Normal ->
assert false
| Blank ->
List.rev !argv
| Quote ->
raise (UnclosedQuote s)
| DQuote ->
raise (UnclosedDQuote s)
| Escape | QEscape | DQEscape ->
raise (UnfinishedEscape s)
let () = Exn_printer.register (fun fmt e -> match e with
| BadEscape (s,c) ->
Format.fprintf fmt "bad escape sequence '\\%c' in string: %s" c s
| UnfinishedEscape s ->
Format.fprintf fmt "unfinished escape sequence in string: %s" s
| UnclosedQuote s ->
Format.fprintf fmt "unclosed quote in string: %s" s
| UnclosedDQuote s ->
Format.fprintf fmt "unclosed double quote in string: %s" s
| EmptyCommandLine ->
Format.fprintf fmt "empty command line"
| _ -> raise e)
(**************************************************************************)
(* *)
(* Copyright (C) 2011- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
exception BadEscape of string * char
exception UnfinishedEscape of string
exception UnclosedQuote of string
exception UnclosedDQuote of string
exception EmptyCommandLine
val cmdline_split : string -> string list
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