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/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