Revision 71999483
Added by Pierre-Loïc Garoche about 4 years ago
| src/backends/C/c_backend_src.ml | ||
|---|---|---|
| 370 | 370 |
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
|
| 371 | 371 |
(pp_c_val m self (pp_c_var_read m)) g |
| 372 | 372 |
(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl |
| 373 |
| MSpec s -> fprintf fmt "@[/*@@ %s */@]@ " s |
|
| 373 | 374 |
| MComment s -> |
| 374 | 375 |
fprintf fmt "/*%s*/@ " s |
| 375 | 376 |
|
| ... | ... | |
| 633 | 634 |
(* dependencies initialization *) |
| 634 | 635 |
(Utils.fprintf_list ~sep:"@," print_import_clear) dependencies |
| 635 | 636 |
|
| 637 |
(* TODO: ACSL |
|
| 638 |
- a contract machine shall not be directly printed in the C source |
|
| 639 |
- but a regular machine associated to a contract machine shall integrate the associated statements, updating its memories, at the end of the function body. |
|
| 640 |
- last one may print intermediate comment/acsl if/when they are present in the sequence of instruction |
|
| 641 |
*) |
|
| 636 | 642 |
let print_machine dependencies fmt m = |
| 637 | 643 |
if fst (get_stateless_status m) then |
| 638 | 644 |
begin |
| ... | ... | |
| 729 | 735 |
(* Print the struct definitions of all machines. *) |
| 730 | 736 |
fprintf source_fmt "/* Struct definitions */@."; |
| 731 | 737 |
fprintf source_fmt "@[<v>"; |
| 732 |
List.iter (print_machine_struct source_fmt) machines; |
|
| 738 |
List.iter (print_machine_struct machines source_fmt) machines;
|
|
| 733 | 739 |
fprintf source_fmt "@]@."; |
| 734 | 740 |
pp_print_newline source_fmt (); |
| 735 | 741 |
(* Print nodes one by one (in the previous order) *) |
Also available in: Unified diff
Cleaning C backend - removing unused functiions
Preparing for coming ACSL