Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / lib / backends.ml @ 9b0432bc

History | View | Annotate | Download (1.26 KB)

1
(* Backend-specific options *)
2
let join_guards = ref true
3

    
4
let setup () =
5
  match !Options.output with
6
  | "tiny" -> begin
7
    Options.global_inline := true;
8
    Options.optimization := 0;
9
    Options.const_unfold := true;
10
  end
11

    
12
  | "emf" ->
13
     (* Not merging branches *)
14
     join_guards := false;
15
     (* In case of a default "int" type, substitute it with the legal int32 value *)
16
     if !Options.int_type = "int" then
17
       Options.int_type := "int32"
18
  | _ -> ()
19

    
20
let is_functional () = 
21
  match !Options.output with
22
  | "horn" | "lustre" | "acsl" | "emf" -> true
23
  | _ -> false
24

    
25
                             
26
(* Special treatment of arrows in lustre backend. We want to keep them *)
27
let unfold_arrow () =
28
  match !Options.output with
29
  | "lustre" -> false
30
  | _ -> true
31

    
32
(* Forcing ite normalization *)
33
let alias_ite () =
34
  match !Options.output with
35
  | "emf" -> true
36
  | _ -> false
37

    
38
(* Forcing basic functions normalization *)
39
let alias_internal_fun () =
40
  match !Options.output with
41
  | "emf" -> true
42
  | _ -> false
43

    
44
let get_normalization_params () = {
45
    Normalization.unfold_arrow_active = unfold_arrow ();
46
    force_alias_ite = alias_ite ();
47
    force_alias_internal_fun = alias_internal_fun ();
48
  }
49

    
50

    
51
(* Local Variables: *)
52
(* compile-command: "make -k -C .." *)
53
(* End: *)