Project

General

Profile

« Previous | Next » 

Revision 7d62bf41

Added by Pierre-Loïc Garoche almost 5 years ago

Merged code

View differences:

src/machine_code.ml
78 78
  mannot: expr_annot list;
79 79
}
80 80

  
81
let get_node_def id m =
82
  try
83
    let (decl, _) = List.assoc id m.minstances in
84
    Corelang.node_of_top decl
85
  with Not_found -> raise Not_found
86
    
81 87
let pp_step fmt s =
82 88
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
83 89
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
......
562 568
	   backends. *)
563 569
	(*match !Options.output with
564 570
	| "horn" -> s
565
	| "C" | "java" | _ ->*) join_guards_list s
571
	  | "C" | "java" | _ ->*)
572
	if !Backends.join_guards then
573
	  join_guards_list s
574
	else
575
	  s
566 576
      );
567 577
      step_asserts =
568 578
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
......
579 589
  List.map
580 590
    (fun decl ->
581 591
     let node = node_of_top decl in
582
      let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in
592
      let sch = (Scheduling.get_node_schedule node node_schs).Scheduling.schedule in
583 593
      translate_decl node sch
584 594
    ) nodes
585 595

  

Also available in: Unified diff