Project

General

Profile

« Previous | Next » 

Revision 7ee5f69e

Added by LĂ©lio Brun 9 months ago

corrections on loggers + spec in AST

View differences:

src/backends/EMF/EMF_backend.ml
454 454
  try
455 455
    fprintf fmt "@[<v 2>\"%a\": {@ "
456 456
      print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
457
    (match m.mspec with Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ " | _ -> ());
457
    (match m.mspec.mnode_spec with
458
     | Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "
459
     | _ -> ());
458 460
    fprintf fmt "\"imported\": \"false\",@ ";
459 461
    fprintf fmt "\"kind\": %t,@ "
460 462
      (fun fmt -> if not ( snd (get_stateless_status m) )
......
471 473
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
472 474
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
473 475
      (pp_emf_instrs m) instrs;
474
    (match m.mspec with | None -> () 
475
                        | Some (Contract c) -> (
476
                          assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
477
                          fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
478
                        )
479
                        | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id
476
    (match m.mspec.mnode_spec with
477
     | None -> ()
478
     | Some (Contract c) -> (
479
         assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
480
         fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
481
       )
482
     | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id
480 483
    );
481 484
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
482 485
    fprintf fmt "@]@ }"

Also available in: Unified diff