Revision 71999483
Added by Pierre-Loïc Garoche about 4 years ago
| src/backends/C/c_backend_header.ml | ||
|---|---|---|
| 159 | 159 |
pp_machine_static_link_name m.mname.node_id |
| 160 | 160 |
inst |
| 161 | 161 |
|
| 162 |
let print_machine_decl fmt m = |
|
| 163 |
begin |
|
| 164 |
Mod.print_machine_decl_prefix fmt m; |
|
| 165 |
if fst (get_stateless_status m) then |
|
| 166 |
begin |
|
| 167 |
fprintf fmt "extern %a;@.@." |
|
| 168 |
print_stateless_prototype |
|
| 169 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
| 170 |
end |
|
| 171 |
else |
|
| 172 |
begin |
|
| 173 |
(* Static allocation *) |
|
| 174 |
if !Options.static_mem |
|
| 175 |
then |
|
| 176 |
begin |
|
| 177 |
let inst = mk_instance m in |
|
| 178 |
let attr = mk_attribute m in |
|
| 179 |
fprintf fmt "%a@.%a@.%a@." |
|
| 180 |
print_static_declare_macro (m, attr, inst) |
|
| 181 |
print_static_link_macro (m, attr, inst) |
|
| 182 |
print_static_alloc_macro (m, attr, inst) |
|
| 183 |
end |
|
| 184 |
else |
|
| 185 |
begin |
|
| 186 |
(* Dynamic allocation *) |
|
| 187 |
fprintf fmt "extern %a;@.@." |
|
| 188 |
print_alloc_prototype (m.mname.node_id, m.mstatic); |
|
| 189 |
|
|
| 190 |
fprintf fmt "extern %a;@.@." |
|
| 191 |
print_dealloc_prototype m.mname.node_id; |
|
| 192 |
end; |
|
| 193 |
let self = mk_self m in |
|
| 194 |
fprintf fmt "extern %a;@.@." |
|
| 195 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic); |
|
| 196 |
|
|
| 197 |
fprintf fmt "extern %a;@.@." |
|
| 198 |
(print_step_prototype self) |
|
| 199 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs); |
|
| 200 |
|
|
| 201 |
if !Options.mpfr then |
|
| 202 |
begin |
|
| 203 |
fprintf fmt "extern %a;@.@." |
|
| 204 |
(print_init_prototype self) (m.mname.node_id, m.mstatic); |
|
| 205 |
|
|
| 206 |
fprintf fmt "extern %a;@.@." |
|
| 207 |
(print_clear_prototype self) (m.mname.node_id, m.mstatic); |
|
| 208 |
end |
|
| 209 |
end |
|
| 210 |
end |
|
| 211 |
|
|
| 212 |
let print_machine_alloc_decl fmt m = |
|
| 162 |
(* TODO: ACSL |
|
| 163 |
we do multiple things: |
|
| 164 |
- provide the semantics of the node as a predicate: function step and reset are associated to ACSL predicate |
|
| 165 |
- the node is associated to a refinement contract, wrt its ACSL sem |
|
| 166 |
- if the node is a regular node associated to a contract, print the contract as function contract. |
|
| 167 |
- do not print anything if this is a contract node |
|
| 168 |
*) |
|
| 169 |
let print_machine_alloc_decl machines fmt m = |
|
| 213 | 170 |
Mod.print_machine_decl_prefix fmt m; |
| 214 | 171 |
if fst (get_stateless_status m) then |
| 215 | 172 |
begin |
| ... | ... | |
| 332 | 289 |
(********************************************************************************************) |
| 333 | 290 |
(* MAIN Header Printing functions *) |
| 334 | 291 |
(********************************************************************************************) |
| 292 |
(* Seems not used |
|
| 293 |
|
|
| 335 | 294 |
let print_header header_fmt basename prog machines dependencies = |
| 336 | 295 |
(* Include once: start *) |
| 337 | 296 |
let baseNAME = file_to_module_name basename in |
| ... | ... | |
| 369 | 328 |
end; |
| 370 | 329 |
(* Print the struct declarations of all machines. *) |
| 371 | 330 |
fprintf header_fmt "/* Structs declarations */@."; |
| 372 |
List.iter (print_machine_struct header_fmt) machines; |
|
| 331 |
List.iter (print_machine_struct machines header_fmt) machines;
|
|
| 373 | 332 |
pp_print_newline header_fmt (); |
| 374 | 333 |
(* Print the prototypes of all machines *) |
| 375 | 334 |
fprintf header_fmt "/* Nodes declarations */@."; |
| ... | ... | |
| 379 | 338 |
fprintf header_fmt "#endif@."; |
| 380 | 339 |
pp_print_newline header_fmt () |
| 381 | 340 |
end |
| 382 |
|
|
| 383 |
let print_alloc_header header_fmt basename prog machines dependencies = |
|
| 341 |
*) |
|
| 342 |
let print_alloc_header header_fmt basename prog machines dependencies spec =
|
|
| 384 | 343 |
(* Include once: start *) |
| 385 | 344 |
let baseNAME = file_to_module_name basename in |
| 386 | 345 |
begin |
| ... | ... | |
| 399 | 358 |
fprintf header_fmt "@]@."; |
| 400 | 359 |
(* Print the struct definitions of all machines. *) |
| 401 | 360 |
fprintf header_fmt "/* Struct definitions */@."; |
| 402 |
List.iter (print_machine_struct header_fmt) machines; |
|
| 361 |
List.iter (print_machine_struct machines header_fmt) machines;
|
|
| 403 | 362 |
pp_print_newline header_fmt (); |
| 363 |
fprintf header_fmt "/* Specification */@.%a@." C_backend_spec.pp_acsl_preamble spec; |
|
| 404 | 364 |
(* Print the prototypes of all machines *) |
| 405 | 365 |
fprintf header_fmt "/* Node allocation function/macro prototypes */@."; |
| 406 |
List.iter (print_machine_alloc_decl header_fmt) machines; |
|
| 366 |
List.iter (print_machine_alloc_decl machines header_fmt) machines;
|
|
| 407 | 367 |
pp_print_newline header_fmt (); |
| 408 | 368 |
(* Include once: end *) |
| 409 | 369 |
fprintf header_fmt "#endif@."; |
Also available in: Unified diff
Cleaning C backend - removing unused functiions
Preparing for coming ACSL