Revision 228ebb2c src/backends/Horn/horn_backend.ml
| src/backends/Horn/horn_backend.ml | ||
|---|---|---|
| 629 | 629 |
Format.fprintf fmt " <Init name=\"%a\">@." |
| 630 | 630 |
pp_machine_init_name m.mname.node_id; |
| 631 | 631 |
|
| 632 |
Format.fprintf fmt "\t<input name=\"%a\" type=\"\">%a</input> @." |
|
| 633 |
(Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_inputs) |
|
| 632 |
|
|
| 633 |
let input_vars = rename_machine_list m.mname.node_id m.mstep.step_inputs in |
|
| 634 |
Format.fprintf fmt "\t<input name=\"%a\" type=\"%a\">%a</input> @." |
|
| 635 |
(Utils.fprintf_list ~sep:" | " pp_var) input_vars |
|
| 636 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) input_vars |
|
| 634 | 637 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs); |
| 635 | 638 |
|
| 636 | 639 |
Format.fprintf fmt "\t<output name=\"%a\" type=\"\">%a</output> @." |
Also available in: Unified diff