Revision 3b2bd83d
Added by Teme Kahsai about 8 years ago
src/options.ml | ||
---|---|---|
10 | 10 |
(********************************************************************) |
11 | 11 |
|
12 | 12 |
let version = Version.number |
13 |
let codename = Version.codename |
|
13 | 14 |
let include_path = Version.include_path |
14 | 15 |
|
15 | 16 |
let print_version () = |
16 |
Format.printf "Lustrec compiler, version %s (dev)@." version;
|
|
17 |
Format.printf "Lustrec compiler, version %s (%s)@." version codename;
|
|
17 | 18 |
Format.printf "Include directory: %s@." include_path |
18 | 19 |
|
19 | 20 |
let main_node = ref "" |
... | ... | |
33 | 34 |
let optimization = ref 2 |
34 | 35 |
let lusi = ref false |
35 | 36 |
let print_reuse = ref false |
36 |
let traces = ref false |
|
37 |
let const_unfold = ref false |
|
38 |
let mpfr = ref false |
|
39 |
let mpfr_prec = ref 0 |
|
37 | 40 |
|
38 |
let horntraces = ref false
|
|
41 |
let traces = ref false |
|
39 | 42 |
let horn_cex = ref false |
40 | 43 |
let horn_query = ref true |
41 | 44 |
|
45 |
let salsa_enabled = ref true |
|
42 | 46 |
|
47 |
let set_mpfr prec = |
|
48 |
if prec > 0 then ( |
|
49 |
mpfr := true; |
|
50 |
mpfr_prec := prec; |
|
51 |
salsa_enabled := false; (* We deactivate salsa *) |
|
52 |
) |
|
53 |
else |
|
54 |
failwith "mpfr requires a positive integer" |
|
55 |
|
|
43 | 56 |
let options = |
44 | 57 |
[ "-d", Arg.Set_string dest_dir, |
45 |
"uses the specified directory as root for generated/imported object and C files (default: .)";
|
|
46 |
"-node", Arg.Set_string main_node, "specifies the main node";
|
|
58 |
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";
|
|
59 |
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
|
|
47 | 60 |
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>"; |
48 | 61 |
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>"; |
49 |
"-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant <default: C99>"; |
|
50 | 62 |
"-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>"; |
63 |
"-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>"; |
|
51 | 64 |
"-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>"; |
52 | 65 |
"-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification"; |
53 |
"-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend (default)";
|
|
66 |
"-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
|
|
54 | 67 |
"-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"; |
55 | 68 |
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; |
56 | 69 |
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C"; |
... | ... | |
59 | 72 |
"-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)"; |
60 | 73 |
"-print_reuse", Arg.Set print_reuse, "prints variable reuse policy"; |
61 | 74 |
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations"; |
62 |
"-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
|
|
75 |
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
|
|
63 | 76 |
"-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation"; |
64 | 77 |
"-print_types", Arg.Set print_types, "prints node types"; |
65 | 78 |
"-print_clocks", Arg.Set print_clocks, "prints node clocks"; |
66 |
"-O", Arg.Set_int optimization, " changes optimization level <default: 2>";
|
|
67 |
"-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
|
|
79 |
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
|
|
80 |
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
|
|
68 | 81 |
"-version", Arg.Unit print_version, " displays the version";] |
69 | 82 |
|
70 | 83 |
|
84 |
let plugin_opt (name, activate, options) = |
|
85 |
( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) :: |
|
86 |
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options) |
|
87 |
|
|
88 |
|
|
71 | 89 |
let get_witness_dir filename = |
72 | 90 |
(* Make sure the directory exists *) |
73 | 91 |
let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in |
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04