Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/machine_code_common.ml | ||
---|---|---|
339 | 339 |
match m.mspec.mnode_spec with |
340 | 340 |
| None -> |
341 | 341 |
() |
342 |
| Some (NodeSpec (id, c)) -> |
|
343 |
fprintf fmt "cocospec: %s@;%a" id |
|
344 |
(pp_print_option (pp_mspec m)) c |
|
342 |
| Some (NodeSpec id) -> |
|
343 |
fprintf fmt "cocospec: %s" id |
|
345 | 344 |
| Some (Contract spec) -> |
346 | 345 |
pp_mspec m fmt spec) |
347 | 346 |
(pp_memory_packs m) |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example