Project

General

Profile

« Previous | Next » 

Revision f20d8ac7

Added by Christophe Garion almost 3 years ago

Ada: skeletons for Ada compiler

View differences:

src/options_management.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11
open Options
12
  
12

  
13 13
let print_version () =
14 14
  Format.printf "Lustrec compiler, version %s (%s)@." version codename;
15 15
  Format.printf "Standard lib: %s@." Version.include_path;
......
21 21
  let removed_slash_suffix =
22 22
    let len = String.length dir in
23 23
    if dir.[len-1] = '/' then
24
      String.sub dir 0 (len - 1) 
24
      String.sub dir 0 (len - 1)
25 25
    else
26 26
      dir
27 27
  in
28 28
  include_dirs := removed_slash_suffix :: !include_dirs
29 29

  
30
    
30

  
31 31
(** Solving the path of required library:
32 32
    If local: look in the folders described in !Options.include_dirs
33 33
    If non local: look first as a local, then in Version.include_path:
......
41 41
    List.fold_right (fun dir res ->
42 42
      match res with Some _ -> res
43 43
      | None ->
44
	 let path_to_lib = dir ^ "/" ^ full_file_name in 
44
	 let path_to_lib = dir ^ "/" ^ full_file_name in
45 45
	 if Sys.file_exists path_to_lib then
46 46
	   Some dir
47 47
	 else
......
57 57
(* Search for path of core libs (without lusic: arrow and io_frontend *)
58 58
let core_dependency lib_name =
59 59
  search_lib_path (false, lib_name ^ ".h")
60
    
60

  
61 61
let name_dependency (local, dep) =
62 62
  let dir = search_lib_path (false, dep ^ ".lusic") in
63 63
  dir ^ "/" ^ dep
64
  
64

  
65 65
let set_mpfr prec =
66 66
  if prec > 0 then (
67 67
    mpfr := true;
......
79 79
      real_type := "mpfr";
80 80
    )
81 81
  | _ -> real_type := s
82
     
82

  
83 83
let set_backend s =
84 84
  output := s;
85 85
  Backends.setup ()
......
90 90
    "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
91 91
    "-print-types", Arg.Set print_types, "prints node types";
92 92
    "-print-clocks", Arg.Set print_clocks, "prints node clocks";
93
    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops"; 
94
    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>"; 
93
    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
94
    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>";
95 95
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
96 96
    "-version", Arg.Unit print_version, " displays the version";
97 97
  ]
98 98

  
99 99
let lustrec_options =
100 100
  common_options @
101
    [ 
101
    [
102 102
      "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
103 103
      "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
104 104
      "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
......
108 108
      "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
109 109
      "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
110 110
      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
111
      "-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C";
111 112
      "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
112 113
      "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
113 114
      "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
......
119 120
      "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
120 121
      "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
121 122
      "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
122
      
123

  
123 124
      "-c++" , Arg.Set        cpp      , "c++ backend";
124 125
      "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
125 126
      "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
......
140 141
let plugin_opt (name, activate, options) =
141 142
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
142 143
    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
143
 
144

  
144 145

  
145 146
let get_witness_dir filename =
146 147
  (* Make sure the directory exists *)

Also available in: Unified diff