Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/backends/EMF/EMF_backend.ml | ||
---|---|---|
489 | 489 |
(* TODO *) |
490 | 490 |
(* assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []); *) |
491 | 491 |
fprintf fmt "\"spec\": %a,@ " pp_emf_spec c |
492 |
| Some (NodeSpec (id, _)) -> fprintf fmt "\"contract\": \"%s\",@ " id);
|
|
492 |
| Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id);
|
|
493 | 493 |
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" |
494 | 494 |
(pp_emf_annots_list (ref 0)) |
495 | 495 |
m.mannot; |
... | ... | |
519 | 519 |
(match ind.nodei_spec with |
520 | 520 |
| None -> fprintf fmt "@ " |
521 | 521 |
| Some (Contract _) -> assert false (* should have been processed *) |
522 |
| Some (NodeSpec (id, _)) -> fprintf fmt ",@ \"coco_contract\": %s" id);
|
|
522 |
| Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);
|
|
523 | 523 |
fprintf fmt "@]@ }" |
524 | 524 |
(* XXX: UNUSED *) |
525 | 525 |
(* with Unhandled msg -> |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example