Revision 86ae18b7 src/options.ml
src/options.ml | ||
---|---|---|
11 | 11 |
|
12 | 12 |
let version = Version.number |
13 | 13 |
let codename = Version.codename |
14 |
let include_path = Version.include_path |
|
14 |
let include_dir = ref "." |
|
15 |
let include_path = |
|
16 |
if (!include_dir != ".") then Version.prefix ^ !include_dir |
|
17 |
else Version.include_path |
|
18 |
|
|
19 |
|
|
20 |
|
|
15 | 21 |
|
16 | 22 |
let print_version () = |
17 | 23 |
Format.printf "Lustrec compiler, version %s (%s)@." version codename; |
18 |
Format.printf "Include directory: %s@." include_path |
|
24 |
Format.printf "Include directory: %s@." include_path; |
|
25 |
Format.printf "User selected Include directory: %s@." !include_dir |
|
19 | 26 |
|
20 | 27 |
let main_node = ref "" |
21 | 28 |
let static_mem = ref true |
... | ... | |
28 | 35 |
let spec = ref "acsl" |
29 | 36 |
let output = ref "C" |
30 | 37 |
let dest_dir = ref "." |
38 |
|
|
31 | 39 |
let verbose_level = ref 1 |
32 | 40 |
let global_inline = ref false |
33 | 41 |
let witnesses = ref false |
... | ... | |
44 | 52 |
|
45 | 53 |
let salsa_enabled = ref true |
46 | 54 |
|
55 |
let sfunction = ref "" |
|
56 |
|
|
47 | 57 |
let set_mpfr prec = |
48 | 58 |
if prec > 0 then ( |
49 | 59 |
mpfr := true; |
... | ... | |
52 | 62 |
) |
53 | 63 |
else |
54 | 64 |
failwith "mpfr requires a positive integer" |
55 |
|
|
65 |
|
|
56 | 66 |
let options = |
57 |
[ "-d", Arg.Set_string dest_dir, |
|
58 |
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>"; |
|
67 |
[ "-d", Arg.Set_string dest_dir, |
|
68 |
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>"; |
|
69 |
"-I", Arg.Set_string include_dir, "Include directory"; |
|
59 | 70 |
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node"; |
60 | 71 |
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>"; |
61 | 72 |
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>"; |
... | ... | |
78 | 89 |
"-print_clocks", Arg.Set print_clocks, "prints node clocks"; |
79 | 90 |
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>"; |
80 | 91 |
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>"; |
92 |
"-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction"; |
|
81 | 93 |
"-version", Arg.Unit print_version, " displays the version";] |
82 | 94 |
|
83 | 95 |
|
84 | 96 |
let plugin_opt (name, activate, options) = |
85 | 97 |
( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) :: |
86 | 98 |
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options) |
87 |
|
|
99 |
|
|
88 | 100 |
|
89 | 101 |
let get_witness_dir filename = |
90 | 102 |
(* Make sure the directory exists *) |
Also available in: Unified diff