Project

General

Profile

Revision 01c7d5e1 src/machine_code.ml

View differences:

src/machine_code.ml
99 99
  mstatic: var_decl list; (* static inputs only *)
100 100
  mstep: step_t;
101 101
  mspec: node_annot option;
102
  mannot: expr_annot option;
102
  mannot: expr_annot list;
103 103
}
104 104

  
105 105
let pp_step fmt s =
......
170 170
    node_dec_stateless = false;
171 171
    node_stateless = Some false;
172 172
    node_spec = None;
173
    node_annot = None;  }
173
    node_annot = [];  }
174 174

  
175 175
let arrow_top_decl =
176 176
  {
......
202 202
                                 [MLocalAssign(var_output, LocalVar var_input2)] ]
203 203
    };
204 204
    mspec = None;
205
    mannot = None;
205
    mannot = [];
206 206
  }
207 207

  
208 208
let new_instance =
......
229 229
(*                       s : step instructions           *)
230 230
let translate_ident node (m, si, j, d, s) id =
231 231
  try (* id is a node var *)
232
    let var_id = node_var id node in
232
    let var_id = get_node_var id node in
233 233
    if ISet.exists (fun v -> v.var_id = id) m
234 234
    then StateVar var_id
235 235
    else LocalVar var_id
......
351 351
  (*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*)
352 352
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
353 353
  | [x], Expr_arrow (e1, e2)                     ->
354
    let var_x = node_var x node in
354
    let var_x = get_node_var x node in
355 355
    let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in
356 356
    let c1 = translate_expr node args e1 in
357 357
    let c2 = translate_expr node args e2 in
......
360 360
     Utils.IMap.add o (arrow_top_decl, []) j,
361 361
     d,
362 362
     (control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)
363
  | [x], Expr_pre e1 when ISet.mem (node_var x node) d     ->
364
    let var_x = node_var x node in
363
  | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d     ->
364
    let var_x = get_node_var x node in
365 365
    (ISet.add var_x m,
366 366
     si,
367 367
     j,
368 368
     d,
369 369
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)
370
  | [x], Expr_fby (e1, e2) when ISet.mem (node_var x node) d ->
371
    let var_x = node_var x node in
370
  | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
371
    let var_x = get_node_var x node in
372 372
    (ISet.add var_x m,
373 373
     MStateAssign (var_x, translate_expr node args e1) :: si,
374 374
     j,
......
376 376
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
377 377

  
378 378
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->
379
    let var_p = List.map (fun v -> node_var v node) p in
379
    let var_p = List.map (fun v -> get_node_var v node) p in
380 380
    let el =
381 381
      match arg.expr_desc with
382 382
      | Expr_tuple el -> el
......
402 402
  | [x], Expr_ite   (c, t, e) 
403 403
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
404 404
      -> 
405
    let var_x = node_var x node in
405
    let var_x = get_node_var x node in
406 406
    (m, 
407 407
     si, 
408 408
     j, 
......
412 412
    )
413 413
      
414 414
  | [x], _                                       -> (
415
    let var_x = node_var x node in
415
    let var_x = get_node_var x node in
416 416
    (m, si, j, d, 
417 417
     control_on_clock 
418 418
       node

Also available in: Unified diff