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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

    r1421 r1462  
    243243         | Some(v) -> Some(v)
    244244      )
    245   | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
    246   | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
    247   | St_exit(_)                  -> None
    248   | St_switch(_,_,_)            -> None
    249   | St_return(_)                -> None
    250   | St_label(l,s) when l = lbl  -> Some((s,k))
    251   | St_goto(_)                  -> None
    252   | St_cost(_,s) | St_label(_,s)-> fdlbl k s
     245  | St_loop(s)                     -> fdlbl (Ct_cont(St_loop(s),k)) s
     246  | St_block(s)                    -> fdlbl (Ct_endblock(k)) s
     247  | St_exit(_)                     -> None
     248  | St_switch(_,_,_)               -> None
     249  | St_return(_)                   -> None
     250  | St_label(l,s) when l = lbl     -> Some((s,k))
     251  | St_goto(_)                     -> None
     252  | St_cost (_,s) | St_label (_,s) -> fdlbl k s
    253253  in match fdlbl k st with
    254254      None -> assert false (*Wrong label*)
Note: See TracChangeset for help on using the changeset viewer.