Project

General

Profile

Revision 59294251 src/options.ml

View differences:

src/options.ml
35 35
let verbose_level = ref 1
36 36
let global_inline = ref false
37 37
let witnesses = ref false
38
let optimization = ref 2
38 39

  
39 40
let options =
40 41
  [ "-d", Arg.Set_string dest_dir,
......
48 49
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
49 50
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
50 51
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
52
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
51 53
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
52 54
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
53 55
    "-print_types", Arg.Set print_types, "prints node types";
54 56
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
57
    "-O", Arg.Set_int optimization, " changes optimization level <default: 2>";
55 58
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
56 59
    "-version", Arg.Unit (fun () -> print_endline version), " displays the version";]
57 60

  

Also available in: Unified diff