Project

General

Profile

« Previous | Next » 

Revision 67ef9395

Added by Pierre-Loïc Garoche almost 3 years ago

minor bugs solved in printer: guarantee vs guarantees in cocospec. Imported node shall not be printed as regular code since it is not part of the grammar yet. Kept them as comment.

View differences:

src/printers.ml
316 316
317 317 
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
318 318 
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
319 
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
319 
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r) fmt spec.guarantees;
320 320 
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
321 321 
    fprintf fmt "mode %s (@[<v 0>%a@ %a@]);"
322 322 
      mode.mode_id
......
368 368 
                      original information with the computed one in
369 369 
                      nd. *)
370 370 
     let pp_l = fprintf_list ~sep:"," pp_var_name in
371 
     fprintf fmt "@[<hov 2>(*@@ contract import %s(%a) returns (%a)@]*)@ "
371 
     fprintf fmt "@[<hov 2>(*@@ contract import %s(%a) returns (%a); @]*)@ "
372 372 
       name
373 373 
       pp_l inl
374 374 
       pp_l outl
......
452 452 
let pp_decl fmt decl =
453 453 
  match decl.top_decl_desc with
454 454 
  | Node nd -> fprintf fmt "%a" pp_node nd
455 
  | ImportedNode ind ->
456 
     fprintf fmt "imported %a;" pp_imported_node ind
455 
  | ImportedNode ind -> (* We do not print imported nodes *)
456 
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
457 457 
  | Const c -> fprintf fmt "const %a" pp_const_decl c
458 458 
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
459 459 
  | Include s -> fprintf fmt "include \"%s\"" s

Also available in: Unified diff