Project

General

Profile

Revision 86ae18b7 src/options.ml

View differences:

src/options.ml
11 11 

  		




  12
  12
  
    
let version = Version.number


  		




  13
  13
  
    
let codename = Version.codename


  		




  14
  
  
    
let include_path = Version.include_path


  		




  
  14
  
    
let include_dir = ref "."


  		




  
  15
  
    
let include_path =


  		




  
  16
  
    
if (!include_dir != ".") then Version.prefix ^ !include_dir


  		




  
  17
  
    
else Version.include_path


  		




  
  18
  
    

  		




  
  19
  
    

  		




  
  20
  
    

  		




  15
  21
  
    

  		




  16
  22
  
    
let print_version () =


  		




  17
  23
  
    
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;


  		




  18
  
  
    
  Format.printf "Include directory: %s@." include_path


  		




  
  24
  
    
  Format.printf "Include directory: %s@." include_path;


  		




  
  25
  
    
  Format.printf "User selected Include directory: %s@." !include_dir


  		




  19
  26
  
    

  		




  20
  27
  
    
let main_node = ref ""


  		




  21
  28
  
    
let static_mem = ref true


  		




  ......




  28
  35
  
    
let spec = ref "acsl"


  		




  29
  36
  
    
let output = ref "C"


  		




  30
  37
  
    
let dest_dir = ref "."


  		




  
  38
  
    

  		




  31
  39
  
    
let verbose_level = ref 1


  		




  32
  40
  
    
let global_inline = ref false


  		




  33
  41
  
    
let witnesses = ref false


  		




  ......




  44
  52
  
    

  		




  45
  53
  
    
let salsa_enabled = ref true


  		




  46
  54
  
    

  		




  
  55
  
    
let sfunction = ref ""


  		




  
  56
  
    

  		




  47
  57
  
    
let set_mpfr prec =


  		




  48
  58
  
    
  if prec > 0 then (


  		




  49
  59
  
    
    mpfr := true;


  		




  ......




  52
  62
  
    
  )


  		




  53
  63
  
    
  else


  		




  54
  64
  
    
    failwith "mpfr requires a positive integer"


  		




  55
  
  
    
			


  		




  
  65
  
    

  		




  56
  66
  
    
let options =


  		




  57
  
  
    
  [ "-d", Arg.Set_string dest_dir,


  		




  58
  
  
    
    "uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";


  		




  
  67
  
    
[ "-d", Arg.Set_string dest_dir,


  		




  
  68
  
    
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";


  		




  
  69
  
    
"-I", Arg.Set_string include_dir, "Include directory";


  		




  59
  70
  
    
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";


  		




  60
  71
  
    
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";


  		




  61
  72
  
    
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";


  		




  ......




  78
  89
  
    
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";


  		




  79
  90
  
    
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";


  		




  80
  91
  
    
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";


  		




  
  92
  
    
    "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";


  		




  81
  93
  
    
    "-version", Arg.Unit print_version, " displays the version";]


  		




  82
  94
  
    

  		




  83
  95
  
    

  		




  84
  96
  
    
let plugin_opt (name, activate, options) =


  		




  85
  97
  
    
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::


  		




  86
  98
  
    
    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)


  		




  87
  
  
    
 


  		




  
  99
  
    

  		




  88
  100
  
    

  		




  89
  101
  
    
let get_witness_dir filename =


  		




  90
  102
  
    
  (* Make sure the directory exists *)


  		












Also available in:  Unified diff