Project

General

Profile

Revision f7caf067 src/machine_code.ml

View differences:

src/machine_code.ml
89 89
  mannot: expr_annot list;
90 90
}
91 91

  
92
(* merge log: get_node_def was in c0f8 *)
93
let get_node_def id m =
94
  try
95
    let (decl, _) = List.assoc id m.minstances in
96
    Corelang.node_of_top decl
97
  with Not_found -> raise Not_found
98
    
99
(* merge log: machine_vars was in 44686 *)
92 100
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
93 101

  
94 102
let pp_step fmt s =
......
616 624
	   backends. *)
617 625
	(*match !Options.output with
618 626
	| "horn" -> s
619
	| "C" | "java" | _ ->*) join_guards_list s
627
	  | "C" | "java" | _ ->*)
628
	if !Backends.join_guards then
629
	  join_guards_list s
630
	else
631
	  s
620 632
      );
621 633
      step_asserts = List.map (translate_expr nd init_args) nd_node_asserts;
622 634
    };

Also available in: Unified diff