Project

General

Profile

Revision 40d33d55 src/options.ml

View differences:

src/options.ml
22 22
let print_version () =
23 23
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;
24 24
  Format.printf "Include directory: %s@." include_path;
25
  Format.printf "User selected Include directory: %s@." !include_dir
25
  Format.printf "User selected include directory: %s@." !include_dir
26 26

  
27 27
let main_node = ref ""
28 28
let static_mem = ref true
......
53 53

  
54 54
let sfunction = ref ""
55 55

  
56
(* test generation options *)
57
let nb_mutants = ref 1000
58
let gen_mcdc = ref false
59
let no_mutation_suffix = ref false
60

  
61

  
56 62
let set_mpfr prec =
57 63
  if prec > 0 then (
58 64
    mpfr := true;
......
61 67
  )
62 68
  else
63 69
    failwith "mpfr requires a positive integer"
64
			
65
let options =
66
[ "-d", Arg.Set_string dest_dir,
67
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";
68
"-I", Arg.Set_string include_dir, "Include directory";
70

  
71
let common_options =
72
  [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";
73
    "-I", Arg.Set_string include_dir, "sets include \x1b[4mdirectory\x1b[0m";
69 74
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
75
    "-print-types", Arg.Set print_types, "prints node types";
76
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
77
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
78
    "-version", Arg.Unit print_version, " displays the version";
79
  ]
80

  
81
let lustrec_options =
82
   common_options @
83
  [ 
70 84
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
71 85
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
72 86
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
......
77 91
    "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
78 92
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
79 93
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
80
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
81
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
82
    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
83
    "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";
84
    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
94
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produces traceability file for Horn backend. Enable the horn backend.";
95
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generates cex enumeration. Enable the horn backend (work in progress)";
96
    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generates queries in generated Horn file. Enable the horn backend (work in progress)";
97
    "-horn-sfunction", Arg.Set_string sfunction, "gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
98
    "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
85 99
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
86
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
87
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
88
    "-print_types", Arg.Set print_types, "prints node types";
89
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
100
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
101
    "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
90 102
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
91 103
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
92
    "-version", Arg.Unit print_version, " displays the version";]
104
    "-version", Arg.Unit print_version, " displays the version";
105
  ]
93 106

  
107
let lustret_options =
108
  common_options @
109
  [ "-nb-mutants", Arg.Set_int nb_mutants, "\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>";
110
    "-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage";
111
    "-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix"
112
  ]
94 113

  
95 114
let plugin_opt (name, activate, options) =
96 115
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::

Also available in: Unified diff