Project

General

Profile

Revision 29f59e36 src/options.ml

View differences:

src/options.ml
38 38
let horn_cex = ref false
39 39
let horn_queries = ref false
40 40

  
41
let scopes_mode = ref false
42
let show_scopes = ref false
43
let scopes : string list list ref = ref []
44
let inputs = ref []
45

  
46
let register_scopes s = 
47
  scopes_mode:= true;
48
  let scope_list = Str.split (Str.regexp ", *") s in
49
  let scope_list = List.map (fun scope -> Str.split (Str.regexp "\\.") scope) scope_list in
50
  scopes := scope_list
51

  
52
let register_inputs s = 
53
  scopes_mode:= true;
54
  let input_list = Str.split (Str.regexp "[;]") s in
55
  let input_list = List.map (fun s -> match Str.split (Str.regexp "=") s with | [v;e] -> v, e | _ -> raise (Invalid_argument ("Input list error: " ^ s))) input_list in
56
  let input_list = List.map (fun (v, e) -> v, Str.split (Str.regexp "[;]") e) input_list in
57
  inputs := input_list
58

  
59

  
60

  
41 61

  
42 62
let options =
43 63
  [ "-d", Arg.Set_string dest_dir,
......
64 84
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
65 85
    "-O", Arg.Set_int optimization, " changes optimization level <default: 2>";
66 86
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
67
    "-version", Arg.Unit print_version, " displays the version";]
87
    "-version", Arg.Unit print_version, " displays the version";]@
88
[
89
  "-scopes", Arg.String register_scopes, "specifies which variables to log";
90
  "-input", Arg.String register_inputs, "specifies the simulation input";
91
  "-show-possible-scopes", Arg.Unit (fun () -> show_scopes:= true; scopes_mode := true), "list possible variables to log";
92
] 
68 93

  
69 94
let get_witness_dir filename =
70 95
  (* Make sure the directory exists *)

Also available in: Unified diff