|
1
|
(* Backend-specific options *)
|
|
2
|
let join_guards = ref true
|
|
3
|
|
|
4
|
let setup () =
|
|
5
|
if !Options.output = "emf" then (
|
|
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
|
if !Options.optimization < 0 then join_guards := false
|
|
11
|
|
|
12
|
let is_functional () =
|
|
13
|
match !Options.output with
|
|
14
|
| "horn" | "lustre" | "acsl" | "emf" ->
|
|
15
|
true
|
|
16
|
| _ ->
|
|
17
|
false
|
|
18
|
|
|
19
|
(* Special treatment of arrows in lustre backend. We want to keep them *)
|
|
20
|
let unfold_arrow () = match !Options.output with "lustre" -> false | _ -> true
|
|
21
|
|
|
22
|
(* Forcing ite normalization *)
|
|
23
|
let alias_ite () = match !Options.output with "emf" -> true | _ -> false
|
|
24
|
|
|
25
|
(* Forcing basic functions normalization *)
|
|
26
|
let alias_internal_fun () =
|
|
27
|
match !Options.output with "emf" -> true | _ -> false
|
|
28
|
|
|
29
|
let get_normalization_params () =
|
|
30
|
{
|
|
31
|
Normalization.unfold_arrow_active = unfold_arrow ();
|
|
32
|
force_alias_ite = alias_ite ();
|
|
33
|
force_alias_internal_fun = alias_internal_fun ();
|
|
34
|
}
|
|
35
|
|
|
36
|
(* Local Variables: *)
|
|
37
|
(* compile-command: "make -k -C .." *)
|
|
38
|
(* End: *)
|