Project

General

Profile

Revision b3b0dd56 src/machine_code.ml

View differences:

src/machine_code.ml
65 65
and pp_branch fmt (t, h) =
66 66
  Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
67 67

  
68
and pp_instrs fmt il =
69
  Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il
70

  
68 71
type step_t = {
69 72
  step_checks: (Location.t * value_t) list;
70 73
  step_inputs: var_decl list;
......
311 314
      are preserved in expression. While they are removed for C or Java
312 315
      backends. *)
313 316
   match !Options.output with
314
   | "horn"
317
   | "horn" ->
318
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
315 319
   | ("C" | "java") when ite ->
316 320
     Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
317 321
   | _ ->
318
     (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
322
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
319 323
 )
320 324
 | _                   -> raise NormalizationError
321 325

  

Also available in: Unified diff