Revision 01c7d5e1 src/horn_backend.ml
src/horn_backend.ml | ||
---|---|---|
313 | 313 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
314 | 314 |
pp_machine_step_name m.mname.node_id |
315 | 315 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
316 |
|
|
316 |
(* |
|
317 | 317 |
match m.mspec with |
318 | 318 |
None -> () (* No node spec; we do nothing *) |
319 | 319 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> |
... | ... | |
323 | 323 |
|
324 | 324 |
) |
325 | 325 |
| _ -> () (* Other cases give nothing *) |
326 |
*) |
|
326 | 327 |
end |
327 | 328 |
end |
328 | 329 |
|
Also available in: Unified diff