lustrec / src / options.ml @ df647a81
History | View | Annotate | Download (3.48 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
|
23 |
let version = "0.1-"^Version.number |
24 |
let main_node = ref "" |
25 |
let static_mem = ref true |
26 |
let print_types = ref true |
27 |
let print_clocks = ref true |
28 |
let delay_calculus = ref true |
29 |
let track_exceptions = ref true |
30 |
let ansi = ref false |
31 |
let check = ref false |
32 |
let c_spec = ref false |
33 |
let output = ref "C" |
34 |
let dest_dir = ref "." |
35 |
let verbose_level = ref 1 |
36 |
let global_inline = ref false |
37 |
let witnesses = ref false |
38 |
let ghost_mode = ref false |
39 |
|
40 |
let options = |
41 |
[ "-d", Arg.Set_string dest_dir, |
42 |
"produces code in the specified directory (default: .)"; |
43 |
"-node", Arg.Set_string main_node, "specifies the main node"; |
44 |
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes"; |
45 |
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node (default: static)"; |
46 |
"-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default: C99)"; |
47 |
"-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)"; |
48 |
"-c-spec", Arg.Set c_spec, |
49 |
"generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend"; |
50 |
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; |
51 |
"-dot", Arg.Unit (fun () -> output := "dot"), "generates dot graph"; |
52 |
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C"; |
53 |
"-inline", Arg.Set global_inline, "inline all node calls (require a main node)"; |
54 |
"-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation"; |
55 |
"-no-ghost-mode", Arg.Clear ghost_mode, "disable ghost annotations (default)."; |
56 |
"-ghost-mode", Arg.Set ghost_mode, "enable ghost annotations."; |
57 |
"-print_types", Arg.Set print_types, "prints node types"; |
58 |
"-print_clocks", Arg.Set print_clocks, "prints node clocks"; |
59 |
"-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>"; |
60 |
"-version", Arg.Unit (fun () -> print_endline version), " displays the version";] |
61 |
|
62 |
let get_witness_dir filename = |
63 |
(* Make sure the directory exists *) |
64 |
let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in |
65 |
let _ = try |
66 |
if not (Sys.is_directory dir) then ( |
67 |
Format.eprintf "File of name %s exists. It should be a directory.@." dir; |
68 |
exit 1 |
69 |
) |
70 |
with Sys_error _ -> Unix.mkdir dir 0o750 |
71 |
in |
72 |
dir |
73 |
|
74 |
(* Local Variables: *) |
75 |
(* compile-command:"make -C .." *) |
76 |
(* End: *) |