Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (8 years ago)
Author:
ayache
Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r818 r1462  
    4848    ERTL.St_store (addr1, addr2, srcrs, lbl)
    4949  | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
     50  | ERTL.St_call_ptr (f1, f2, nb_args, _) ->
     51    ERTL.St_call_ptr (f1, f2, nb_args, lbl)
    5052  | ERTL.St_cond _ as inst -> inst
    5153  | ERTL.St_return _ as inst -> inst
     
    293295   below. When the called function returns, we put the result where the calling
    294296   function expect it to be. *)
    295 let translate_call_id f args ret_regs start_lbl dest_lbl def =
     297let translate_call stmt args ret_regs start_lbl dest_lbl def =
    296298  let nb_args = List.length args in
    297299  add_translates
     
    299301      adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @
    300302     set_params args @
    301      [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ;
     303     [adds_graph [stmt nb_args] ;
    302304      adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ;
    303305      fetch_result ret_regs ;
     
    358360
    359361  | RTL.St_call_id (f, args, ret_regs, lbl') ->
    360     translate_call_id f args ret_regs lbl lbl' def
    361 
    362   | RTL.St_call_ptr _ ->
    363     assert false (* TODO *)
     362    let stmt nb_args = ERTL.St_call_id (f, nb_args, lbl) in
     363    translate_call stmt args ret_regs lbl lbl' def
     364
     365  | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl') ->
     366    let stmt nb_args = ERTL.St_call_ptr (f1, f2, nb_args, lbl) in
     367    translate_call stmt args ret_regs lbl lbl' def
    364368
    365369  (*
     
    438442    | ERTL.St_load (_, _, _, lbl)
    439443    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
     444    | ERTL.St_call_ptr (_, _, _, lbl)
    440445    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
    441446      ->
Note: See TracChangeset for help on using the changeset viewer.