Revision dda9eb32
Added by Guillaume DAVY almost 5 years ago
| src/backends/Ada/ada_backend_ads.ml | ||
|---|---|---|
| 107 | 107 |
match opt_contract with |
| 108 | 108 |
| None -> pp_prototype fmt |
| 109 | 109 |
| Some contract -> |
| 110 |
fprintf fmt "@[<v 2>%t with@,%a,@,%a@]"
|
|
| 110 |
fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
|
|
| 111 | 111 |
pp_prototype |
| 112 | 112 |
(Utils.fprintf_list ~sep:",@," pp_pre) contract.assume |
| 113 |
(Utils.pp_final_char_if_non_empty ",@," contract.assume) |
|
| 113 | 114 |
(Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees |
| 114 | 115 |
|
| 115 | 116 |
(** Print the prototype with a contract of the reset procedure from a machine. |
Also available in: Unified diff
Ada: Correct contract printing