Project

General

Profile

Download (1.18 KB) Statistics
| Branch: | Tag: | Revision:
1 37419cf4 ploc
(* Backend-specific options *)
2
let join_guards = ref true
3
4 13507742 ploc
let setup () =
5 f69e7ea2 LĂ©lio Brun
  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 1bff14ac ploc
14 13507742 ploc
let is_functional () = 
15
  match !Options.output with
16
  | "horn" | "lustre" | "acsl" | "emf" -> true
17
  | _ -> false
18
19 ad4774b0 ploc
                             
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 ef8a361a ploc
45 1bff14ac ploc
(* Local Variables: *)
46
(* compile-command: "make -k -C .." *)
47
(* End: *)