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

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

Location:
Deliverables/D2.2/8051/src/LTL
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/LTL/LTL.mli

    r818 r1462  
    7575  | St_call_id of AST.ident * Label.t
    7676
     77  (* Call to a function given its address. Parameters are the registers holding
     78     the address of the function, and the label of the next statement. *)
     79  | St_call_ptr of I8051.register * I8051.register * Label.t
     80
    7781  (* Branch on A accumulator. Parameters are the label to go to when the A
    7882     accumulator is not 0, and the label to go to when the A accumulator is
  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r818 r1462  
    196196  change_pc st next_pc
    197197
    198 let interpret_call lbls_offs st f ra =
    199   let ptr = Mem.find_global st.mem f in
     198let interpret_call lbls_offs st ptr ra =
    200199  match Mem.find_fun_def st.mem ptr with
    201200    | LTL.F_int def ->
     
    303302
    304303    | LTL.St_call_id (f, lbl) ->
    305       interpret_call lbls_offs st f lbl
     304      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     305
     306    | LTL.St_call_ptr (f1, f2, lbl) ->
     307      let addr = List.map (fun r -> get_reg r st) [f1 ; f2] in
     308      interpret_call lbls_offs st addr lbl
    306309
    307310    | LTL.St_condacc (lbl_true, lbl_false) ->
  • Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

    r818 r1462  
    5555    Printf.sprintf "movex @DPTR, %s --> %s" print_a lbl
    5656  | LTL.St_call_id (f, lbl) -> Printf.sprintf "call \"%s\" --> %s" f lbl
     57  | LTL.St_call_ptr (f1, f2, lbl) ->
     58    Printf.sprintf "call_ptr [%s ; %s] --> %s" (print_reg f1) (print_reg f2) lbl
    5759  | LTL.St_condacc (lbl_true, lbl_false) ->
    5860    Printf.sprintf "branch %s <> 0 --> %s, %s" print_a lbl_true lbl_false
  • Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml

    r818 r1462  
    5050  | LTL.St_call_id (f, _) ->
    5151    LIN.St_call_id f
     52  | LTL.St_call_ptr (f1, f2, _) ->
     53    LIN.St_call_ptr (f1, f2)
    5254
    5355  (* Conditional branch statement. In [LIN], control implicitly
  • Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml

    r818 r1462  
    130130        | LTL.St_load l
    131131        | LTL.St_store l
    132         | LTL.St_call_id (_, l) ->
     132        | LTL.St_call_id (_, l)
     133        | LTL.St_call_ptr (_, _, l) ->
    133134
    134135          visit l
  • Deliverables/D2.2/8051/src/LTL/branch.ml

    r818 r1462  
    8080    | LTL.St_call_id (f, l) ->
    8181      LTL.St_call_id (f, rep l)
     82    | LTL.St_call_ptr (f1, f2, l) ->
     83      LTL.St_call_ptr (f1, f2, rep l)
    8284    | LTL.St_condacc (lbl_true, lbl_false) ->
    8385      LTL.St_condacc (rep lbl_true, rep lbl_false)
Note: See TracChangeset for help on using the changeset viewer.