Project

General

Profile

Revision 7291cb80 src/options.ml

View differences:

src/options.ml
31 31
let check = ref false
32 32
let c_spec = ref false
33 33
let output = ref "C"
34
let dest_dir = ref ""
34
let dest_dir = ref "."
35 35
let verbose_level = ref 1
36 36
let global_inline = ref false
37 37
let witnesses = ref false
38 38

  
39 39
let options =
40 40
  [ "-d", Arg.Set_string dest_dir,
41
    "produces code in the specified directory";
41
    "produces code in the specified directory (default: .)";
42 42
    "-node", Arg.Set_string main_node, "specifies the main node";
43 43
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes";
44 44
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node (default: static)";
45
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default is C99)";
45
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default: C99)";
46 46
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";
47 47
    "-c-spec", Arg.Set c_spec, 
48 48
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";

Also available in: Unified diff