Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

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