Project

General

Profile

Revision 45f0f48d src/machine_code.ml

View differences:

src/machine_code.ml
36 36
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
37 37
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
38 38
    | MReset i           -> Format.fprintf fmt "reset %s" i
39
    | MNoReset i         -> Format.fprintf fmt "noreset %s" i
39 40
    | MStep (il, i, vl)  ->
40 41
      Format.fprintf fmt "%a = %s (%a)"
41 42
	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
......
135 136
    var_dec_const = false;
136 137
    var_dec_value = None;
137 138
    var_type =  typ;
138
    var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
139
    var_clock = Clocks.new_ck Clocks.Cvar true;
139 140
    var_loc = Location.dummy_loc
140 141
  }
141 142

  
......
352 353
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
353 354
      let nd = node_from_name id in
354 355
      Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
355
    | Expr_ite (g,t,e) -> (
356
    (*| Expr_ite (g,t,e) -> (
356 357
      (* special treatment depending on the active backend. For horn backend, ite
357 358
	 are preserved in expression. While they are removed for C or Java
358 359
	 backends. *)
......
360 361
	Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
361 362
      | "C" | "java" | _ -> 
362 363
	(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
363
    )
364
    )*)
364 365
    | _                   -> raise NormalizationError
365 366
  in
366 367
  mk_val value_desc expr.expr_type
......
373 374
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
374 375
  match expr.expr_desc with
375 376
  | Expr_ite   (c, t, e) -> let g = translate_guard node args c in
376
			    conditional g [translate_act node args (y, t)]
377
			    conditional g
378
                              [translate_act node args (y, t)]
377 379
                              [translate_act node args (y, e)]
378
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x, List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
380
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x,
381
                                     List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
379 382
  | _                    -> MLocalAssign (y, translate_expr node args expr)
380 383

  
381 384
let reset_instance node args i r c =
382 385
  match r with
383 386
  | None        -> []
384 387
  | Some r      -> let g = translate_guard node args r in
385
                   [control_on_clock node args c (conditional g [MReset i] [])]
388
                   [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
386 389

  
387 390
let translate_eq node ((m, si, j, d, s) as args) eq =
388 391
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
......
434 437
      then []
435 438
      else reset_instance node args o r call_ck) @
436 439
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
437

  
440
(*
438 441
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
439 442
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
440 443
      backends. *)
......
450 453
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
451 454
    )
452 455

  
456
*)
453 457
  | [x], _                                       -> (
454 458
    let var_x = get_node_var x node in
455 459
    (m, si, j, d,
......
556 560
	(* special treatment depending on the active backend. For horn backend,
557 561
	   common branches are not merged while they are in C or Java
558 562
	   backends. *)
559
	match !Options.output with
563
	(*match !Options.output with
560 564
	| "horn" -> s
561
	| "C" | "java" | _ -> join_guards_list s
565
	| "C" | "java" | _ ->*) join_guards_list s
562 566
      );
563 567
      step_asserts =
564 568
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in

Also available in: Unified diff