Project

General

Profile

« Previous | Next » 

Revision 61e0c3c4

Added by Guillaume DAVY about 4 years ago

Ada:
- Correct the merge with lustrec-seal
- Improve support for builtin function(still work to do)
- Add generation of a gpr file for lib(without main).
- Add var initialisation in the reset, still work to do.

View differences:

src/backends/Ada/ada_backend_wrapper.ml
49 49
     @param machine the main machine
50 50
  **)
51 51
  let pp_main_adb fmt machine =
52
    let pp_str str fmt = fprintf fmt "%s"str in
52
    let pp_str str fmt = fprintf fmt "%s" str in
53 53
    (* Dependances *)
54 54
    let text_io = "Ada.Text_IO" in
55 55
    let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in
......
119 119
      pp_with_machine machine
120 120
      (pp_main_procedure_definition machine) (locals, instrs)
121 121

  
122
  (** Print the gpr project file.
122
  (** Print the name of the ada project configuration file.
123
     @param fmt the formater to print on
124
     @param main_machine the machine associated to the main node
125
  **)
126
  let pp_project_configuration_name fmt basename =
127
    fprintf fmt "%s.adc" basename
128

  
129
  (** Print the project configuration file.
123 130
     @param fmt the formater to print on
124 131
     @param machine the main machine
125 132
  **)
126
  let pp_project_file fmt machine =
127
      fprintf fmt "project %a is@.  for Main use (\"%a\");@.end %a;"
128
        pp_package_name machine
129
        (pp_filename "adb") pp_main_procedure_name
130
        pp_package_name machine
133
  let pp_project_configuration_file fmt machine =
134
    fprintf fmt "pragma SPARK_Mode (On);"
135

  
136
  (** Print the name of the ada project file.
137
     @param base_name name of the lustre file
138
     @param fmt the formater to print on
139
     @param machine_opt the main machine option
140
  **)
141
  let pp_project_name basename fmt machine_opt =
142
    fprintf fmt "%s.gpr" basename
143

  
144
  let pp_for_single name arg fmt =
145
    fprintf fmt "for %s use \"%s\"" name arg
146

  
147
  let pp_for name args fmt =
148
    fprintf fmt "for %s use (@[%a@])" name
149
      (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
150
      args
151

  
152
  let pp_content fmt lines =
153
    fprintf fmt "  @[<v>%a%t@]"
154
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
155
      (Utils.pp_final_char_if_non_empty ";" lines)
156

  
157
  let pp_package name lines fmt =
158
    fprintf fmt "package %s is@,%a@,end %s"
159
      name
160
      pp_content lines
161
      name
162

  
163
  (** Print the gpr project file, if there is a machine in machine_opt then
164
        an executable project is made else it is a library.
165
     @param fmt the formater to print on
166
     @param machine_opt the main machine option
167
  **)
168
  let pp_project_file machines basename fmt machine_opt =
169
    let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
170
                  @(match machine_opt with
171
                    | None -> []
172
                    | Some m -> [asprintf "%a" pp_main_filename m]) in
173
    let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
174
    fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
175
    pp_content
176
    ((match machine_opt with
177
      | None -> [
178
          pp_for_single "Library_Name" basename;
179
          pp_for_single "Library_Dir" "lib";
180
        ]
181
      | Some machine -> [
182
          pp_for "Main" [asprintf "%t" pp_main_procedure_name];
183
          pp_for_single "Exec_Dir" "bin";
184
        ])
185
    @[
186
      pp_for_single "Object_Dir" "obj";
187
      pp_for "Source_Files" adbs;
188
      pp_package "Builder" [
189
        pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
190
      ];
191
      pp_package "Prove" [
192
        pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
193
      ]
194
    ])
195
    project_name
196

  
131 197

  
132 198
  end

Also available in: Unified diff