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/ERTL/liveness.ml

    r818 r1462  
    3838  | St_load (_, _, _, l)
    3939  | St_store (_, _, _, l)
    40   | St_call_id (_, _, l) ->
     40  | St_call_id (_, _, l)
     41  | St_call_ptr (_, _, _, l) ->
    4142    Label.Set.singleton l
    4243  | St_cond (_, l1, l2) ->
     
    145146  | St_hdw_to_hdw (r, _, _) ->
    146147    L.hsingleton r
    147   | St_call_id _ ->
     148  | St_call_id _ | St_call_ptr _  ->
    148149      (* Potentially destroys all caller-save hardware registers. *)
    149150    Register.Set.empty, I8051.caller_saved
     
    179180    (* Reads the hardware registers that are used to pass parameters. *)
    180181    Register.Set.empty,
     182    set_of_list (MiscPottier.prefix nparams I8051.parameters)
     183  | St_call_ptr (r1, r2, nparams, _) ->
     184    (* Reads the hardware registers that are used to pass parameters. *)
     185    Register.Set.of_list [r1 ; r2],
    181186    set_of_list (MiscPottier.prefix nparams I8051.parameters)
    182187  | St_get_hdw (_, r, _)
     
    230235  | St_store _
    231236  | St_call_id _
     237  | St_call_ptr _
    232238  | St_cond _
    233239  | St_return _ ->
Note: See TracChangeset for help on using the changeset viewer.