|
1
|
(* Backend-specific options *)
|
|
2
|
let join_guards = ref true
|
|
3
|
|
|
4
|
let setup () =
|
|
5
|
match !Options.output with
|
|
6
|
(* | "emf" -> *)
|
|
7
|
(* join_guards := true; (\* guards should not be joined, in order to have only *)
|
|
8
|
(* if c then x = e1 else x = e2 to ease *)
|
|
9
|
(* reconstruction of flows. *\) *)
|
|
10
|
(* Options.optimization := 0; (\* Optimization=0 prevents expression *)
|
|
11
|
(* elimination. This simplifies largely the *)
|
|
12
|
(* association of lustre expression to *)
|
|
13
|
(* instructions *\) *)
|
|
14
|
| _ -> ()
|
|
15
|
|
|
16
|
let is_functional () =
|
|
17
|
match !Options.output with
|
|
18
|
| "horn" | "lustre" | "acsl" | "emf" -> true
|
|
19
|
| _ -> false
|
|
20
|
|
|
21
|
|
|
22
|
(* Local Variables: *)
|
|
23
|
(* compile-command: "make -k -C .." *)
|
|
24
|
(* End: *)
|