Project

General

Profile

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