1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
(* This section is all for argument processing *)
(* Mode *)
let version = ref false
let auth = ref false
(* file names *)
let output_file = ref "-"
let policy_file = ref ""
let mls_file = ref ""
let anon_var = ref 0
let anon_fun str =
match !anon_var with
0 ->
policy_file := str;
anon_var := 1
| 1 ->
mls_file := str;
anon_var := 2
| _ ->
anon_var := 3
(* set up Arg.parse *)
let arg_spec =
[("-a", Arg.Set(auth),
" - generate an authorization transition relation");
("-f", Arg.Clear(auth),
" - generate an information flow transition relation (default)");
("-o", Arg.String(fun s -> output_file := s),
"name - send output to this file (default stdout)" );
("-v", Arg.Set(version),
" - display version information and exit");
("--", Arg.Rest(anon_fun),
" - treat remaining args as file names, where - means stdin")]
let usage_msg = "Usage: slat [options] policy [mls]";;
Arg.parse arg_spec anon_fun usage_msg;
if !version then
begin
Print_version.print_version();
exit 0
end;
if !anon_var < 1 || !anon_var > 2 then
begin
prerr_string "bad arg count";
prerr_newline();
prerr_string usage_msg;
prerr_newline();
exit 1
end;
if !anon_var = 2 && !auth then
begin
prerr_string "no mls allowed with -a option";
prerr_newline();
prerr_string usage_msg;
prerr_newline();
exit 1
end;
let policy_file_name = !policy_file in
let mls_file_name = !mls_file in
let output_file_name = !output_file in
let auth_flag = !auth in
try
(* read input *)
Read_policy_mls.read_policy policy_file_name;
if mls_file_name <> "" then
Read_policy_mls.read_mls mls_file_name;
(* make lts *)
let lts = Identifier.slat auth_flag in
(* open output file *)
let out =
if output_file_name = "-" then
stdout
else
open_out output_file_name in
Format.set_formatter_out_channel out;
(* produce output *)
Formulas.print_lts lts;
exit 0
with Failure s ->
prerr_string s;
prerr_newline();
exit 1
|
