Revision dccec723
Added by LĂ©lio Brun over 3 years ago
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
a version that almost work for the k-inuctive two_counters example