Revision 61e0c3c4
Added by Guillaume DAVY about 4 years ago
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
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.