Project

General

Profile

Revision b38ffff3 src/options.ml

View differences:

src/options.ml
1 
(* ----------------------------------------------------------------------------
2 
 * SchedMCore - A MultiCore Scheduling Framework
3 
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4 
 *
5 
 * This file is part of Prelude
6 
 *
7 
 * Prelude is free software; you can redistribute it and/or
8 
 * modify it under the terms of the GNU Lesser General Public License
9 
 * as published by the Free Software Foundation ; either version 2 of
10 
 * the License, or (at your option) any later version.
11 
 *
12 
 * Prelude is distributed in the hope that it will be useful, but
13 
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15 
 * Lesser General Public License for more details.
16 
 *
17 
 * You should have received a copy of the GNU Lesser General Public
18 
 * License along with this program ; if not, write to the Free Software
19 
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20 
 * USA
21 
 *---------------------------------------------------------------------------- *)
1 
(********************************************************************)
2 
(*                                                                  *)
3 
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4 
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5 
(*                                                                  *)
6 
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7 
(*  under the terms of the GNU Lesser General Public License        *)
8 
(*  version 2.1.                                                    *)
9 
(*                                                                  *)
10 
(********************************************************************)
22 11 

  		




  23
  12
  
    
let version = "0.1-"^Version.number


  		




  24
  13
  
    
let main_node = ref ""


  		




  ......




  36
  25
  
    
let global_inline = ref false


  		




  37
  26
  
    
let witnesses = ref false


  		




  38
  27
  
    
let optimization = ref 2


  		




  
  28
  
    

  		




  39
  29
  
    
let horntraces = ref false


  		




  40
  30
  
    
let horn_cex = ref false


  		




  41
  
  
    

  		




  
  31
  
    
let horn_queries = ref false


  		




  42
  32
  
    

  		




  43
  33
  
    
let options =


  		




  44
  34
  
    
  [ "-d", Arg.Set_string dest_dir,


  		




  ......




  55
  45
  
    
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";


  		




  56
  46
  
    
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";


  		




  57
  47
  
    
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";


  		




  58
  
  
    
    "-horn-cex", Arg.Set horn_cex, "generate cex enumeration. Enable the horn backend (work in progress)";


  		




  
  48
  
    
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";


  		




  
  49
  
    
    "-horn-queries", Arg.Unit (fun () -> output := "horn"; horn_queries:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";


  		




  59
  50
  
    
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";


  		




  60
  51
  
    
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";


  		




  61
  52
  
    
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";


  		












Also available in:  Unified diff