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