Project

General

Profile

Revision 01c7d5e1 src/horn_backend.ml

View differences:

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