Revision 13507742
Added by PierreLoïc Garoche about 6 years ago
src/backends/backends.ml  

1  1 
(* Backendspecific 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 
(* compilecommand: "make k C .." *) 
18  24 
(* End: *) 
Also available in: Unified diff
Refactored some code: optimization of machine