Project

General

Profile

« Previous | Next » 

Revision 76c7023b

Added by Pierre-Loïc Garoche about 5 years ago

functional_backend function moved to corelang

View differences:

src/main_lustre_compiler.ml
88 88 
  end
89 89 

  		




  90
  90
  
    

  		




  91
  
  
    
let functional_backend () = 


  		




  92
  
  
    
  match !Options.output with


  		




  93
  
  
    
  | "horn" | "lustre" | "acsl" -> true


  		




  94
  
  
    
  | _ -> false


  		




  95
  91
  
    

  		




  96
  92
  
    
(* From prog to prog *)


  		




  97
  93
  
    
let stage1 prog dirname basename =


  		




  ......




  296
  292
  
    
  in  


  		




  297
  293
  
    
  (* Optimize machine code *)


  		




  298
  294
  
    
  let machine_code =  (* TODO reactivate. I disabled it because output variables were removed *)


  		




  299
  
  
    
    if false && !Options.optimization >= 3 && not (functional_backend ()) then


  		




  
  295
  
    
    if false && !Options.optimization >= 3 && not (Corelang.functional_backend ()) then


  		




  300
  296
  
    
      begin


  		




  301
  297
  
    
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize heap alloc by reusing vars@,");


  		




  302
  298
  
    
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in


  		












Also available in:  Unified diff