Project

General

Profile

Revision ed81df06 src/options.ml

View differences:

src/options.ml
25 25
let global_inline = ref false
26 26
let witnesses = ref false
27 27
let optimization = ref 2
28
let lusi = ref false
28 29

  
29 30
let horntraces = ref false
30 31
let horn_cex = ref false
......
34 35
  [ "-d", Arg.Set_string dest_dir,
35 36
    "produces code in the specified directory (default: .)";
36 37
    "-node", Arg.Set_string main_node, "specifies the main node";
37
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes";
38
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node (default: static)";
39
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default: C99)";
40
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";
41

  
38
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
39
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
40
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant <default: C99>";
41
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
42
    "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
42 43
    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
43 44
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend (default)";
44 45
    "-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";

Also available in: Unified diff