Project

General

Profile

Revision cf9cc6f9 src/machine_code.ml

View differences:

src/machine_code.ml
34 34
  | MLocalAssign of var_decl * value_t
35 35
  | MStateAssign of var_decl * value_t
36 36
  | MReset of ident
37
  | MNoReset of ident (* used to symmetrize the reset function *)
37 38
  | MStep of var_decl list * ident * value_t list
38 39
  | MBranch of value_t * (label * instr_t list) list
39 40

  
......
52 53
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
53 54
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
54 55
    | MReset i           -> Format.fprintf fmt "reset %s" i
56
    | MNoReset i         -> ()
55 57
    | MStep (il, i, vl)  ->
56 58
      Format.fprintf fmt "%a = %s (%a)"
57 59
	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
......
319 321
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
320 322
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
321 323
 | Expr_merge   (g, hl)              -> (
322
   (* Special treatment for functional backends. Is transformed into Ite *)
323
   match !Options.output with
324
   | "horn" -> translate_expr node  args (merge_to_ite g hl)
325
   | ("C" | "java")          -> raise NormalizationError (* should have been replaced by MBranch *)
326
   | _ ->
324
   (* (\* Special treatment for functional backends. Is transformed into Ite *\) *)
325
   (* match !Options.output with *)
326
   (* | "horn" -> translate_expr node  args (merge_to_ite g hl) *)
327
   (* | ("C" | "java")          -> raise NormalizationError (\* should have been replaced by MBranch *\) *)
328
   (* | _ -> *)
327 329
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
328 330

  
329 331
 )
......
363 365
  match r with
364 366
  | None        -> []
365 367
  | Some r      -> let g = translate_guard node args r in
366
                   [control_on_clock node args c (conditional g [MReset i] [])]
368
                   [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
367 369

  
368 370
let translate_eq node ((m, si, j, d, s) as args) eq =
369 371
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
......
415 417
      then []
416 418
      else reset_instance node args o r call_ck) @
417 419
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
418

  
420
(*
419 421
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
420 422
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
421 423
      backends. *)
422 424
  | [x], Expr_ite   _
423 425
  (* similar treatment for merge, avoid generating MBranch instructions when using Horn backend *)
424 426
  | [x], Expr_merge _ 
425
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
427
    when (match !Options.output with | "horn" -> false (* TODO 16/12 was true *) | "C" | "java" | _ -> false)
426 428

  
427 429
      (* Remark for Ocaml: the when is shared among the two patterns *)
428 430
      ->
......
435 437
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
436 438
    )
437 439

  
438
 
440
*)
439 441
  | [x], _                                       -> (
440 442
    let var_x = get_node_var x node in
441 443
    (m, si, j, d,
......
543 545
	   common branches are not merged while they are in C or Java
544 546
	   backends. *)
545 547
	match !Options.output with
546
	| "horn" -> s
548
	(* | "horn" -> s TODO 16/12 *)
547 549
	| "C" | "java" | _ -> join_guards_list s
548 550
      );
549 551
      step_asserts =

Also available in: Unified diff