Revision 61e0c3c4
Added by Guillaume DAVY about 4 years ago
src/backends/Ada/ada_backend_ads.ml | ||
---|---|---|
106 | 106 |
let pp_procedure_prototype_contract pp_prototype fmt opt_contract = |
107 | 107 |
match opt_contract with |
108 | 108 |
| None -> pp_prototype fmt |
109 |
| Some contract -> |
|
110 |
fprintf fmt "@[<v 2>%t with@,%a%t%a@]" |
|
109 |
| Some (NodeSpec ident) -> pp_prototype fmt (*TODO*) |
|
110 |
| Some (Contract contract) -> |
|
111 |
fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]" |
|
111 | 112 |
pp_prototype |
112 | 113 |
(Utils.fprintf_list ~sep:",@," pp_pre) contract.assume |
113 | 114 |
(Utils.pp_final_char_if_non_empty ",@," contract.assume) |
... | ... | |
118 | 119 |
@param machine the machine |
119 | 120 |
**) |
120 | 121 |
let pp_step_prototype_contract fmt m = |
121 |
() |
|
122 |
(* Temporarily disabled while waiting for the code to stabilize |
|
123 |
pp_procedure_prototype_contract |
|
124 |
(pp_step_prototype m) |
|
125 |
fmt |
|
126 |
m.mspec |
|
127 |
*) |
|
122 |
pp_procedure_prototype_contract |
|
123 |
(pp_step_prototype m) |
|
124 |
fmt |
|
125 |
m.mspec |
|
126 |
|
|
128 | 127 |
|
129 | 128 |
(** Remove duplicates from a list according to a given predicate. |
130 | 129 |
@param eq the predicate defining equality |
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.