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/Ada/ada_backend.ml
86 86
       l) -> assert false | Expr_appl call -> assert false *)
87 87
  in
88 88
  match m.mspec.mnode_spec with
89
  | Some (NodeSpec (ident, _)) ->
89
  | Some (NodeSpec ident) ->
90 90
    let machine_spec = find_submachine_from_ident ident machines in
91 91
    let guarantees =
92 92
      match machine_spec.mspec.mnode_spec with

Also available in: Unified diff