Revision 13507742
Added by Pierre-Loïc Garoche about 6 years ago
| src/backends/backends.ml | ||
|---|---|---|
| 1 | 1 |
(* Backend-specific options *) |
| 2 | 2 |
let join_guards = ref true |
| 3 | 3 |
|
| 4 |
let setup s =
|
|
| 5 |
match s 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 *)
|
|
| 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 | 14 |
| _ -> () |
| 15 | 15 |
|
| 16 |
let is_functional () = |
|
| 17 |
match !Options.output with |
|
| 18 |
| "horn" | "lustre" | "acsl" | "emf" -> true |
|
| 19 |
| _ -> false |
|
| 20 |
|
|
| 21 |
|
|
| 16 | 22 |
(* Local Variables: *) |
| 17 | 23 |
(* compile-command: "make -k -C .." *) |
| 18 | 24 |
(* End: *) |
Also available in: Unified diff
Refactored some code: optimization of machine