|
1
|
(* Backend-specific options *)
|
|
2
|
let join_guards = ref true
|
|
3
|
|
|
4
|
let setup () =
|
|
5
|
if !Options.output = "emf" then begin
|
|
6
|
(* Not merging branches *)
|
|
7
|
join_guards := false;
|
|
8
|
(* In case of a default "int" type, substitute it with the legal int32 value *)
|
|
9
|
if !Options.int_type = "int" then Options.int_type := "int32"
|
|
10
|
end;
|
|
11
|
if !Options.optimization < 0 then
|
|
12
|
join_guards := false
|
|
13
|
|
|
14
|
let is_functional () =
|
|
15
|
match !Options.output with
|
|
16
|
| "horn" | "lustre" | "acsl" | "emf" -> true
|
|
17
|
| _ -> false
|
|
18
|
|
|
19
|
|
|
20
|
(* Special treatment of arrows in lustre backend. We want to keep them *)
|
|
21
|
let unfold_arrow () =
|
|
22
|
match !Options.output with
|
|
23
|
| "lustre" -> false
|
|
24
|
| _ -> true
|
|
25
|
|
|
26
|
(* Forcing ite normalization *)
|
|
27
|
let alias_ite () =
|
|
28
|
match !Options.output with
|
|
29
|
| "emf" -> true
|
|
30
|
| _ -> false
|
|
31
|
|
|
32
|
(* Forcing basic functions normalization *)
|
|
33
|
let alias_internal_fun () =
|
|
34
|
match !Options.output with
|
|
35
|
| "emf" -> true
|
|
36
|
| _ -> false
|
|
37
|
|
|
38
|
let get_normalization_params () = {
|
|
39
|
Normalization.unfold_arrow_active = unfold_arrow ();
|
|
40
|
force_alias_ite = alias_ite ();
|
|
41
|
force_alias_internal_fun = alias_internal_fun ();
|
|
42
|
}
|
|
43
|
|
|
44
|
|
|
45
|
(* Local Variables: *)
|
|
46
|
(* compile-command: "make -k -C .." *)
|
|
47
|
(* End: *)
|