Changeset 1457


Ignore:
Timestamp:
Oct 23, 2011, 10:15:51 PM (8 years ago)
Author:
sacerdot
Message:

Bug fixed: when calling an internal function, the pc block is now set to
the block allocated for the internal function. However, so far this was
not an invariant used inside joint/semantics.ma, but only in the instantiation
of the different languages.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/TODO

    r1453 r1457  
    550) factorize lin_fetch_function and graph_fetch_function
    66    and maybe also lin_fetch_statement and graph_fetch_statement
    7 1) bug chiamata di funzioni esterne: non riusare il blocco del vecchio pc!
    8    bug semantica: aritmetica dei puntatori su Code non deve essere permessa
     71) bug semantica: aritmetica dei puntatori su Code non deve essere permessa
    982) traduzione LINToASM ed etichetti uniche
    1093) funzioni esterne
  • src/joint/semantics.ma

    r1451 r1457  
    226226      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    227227      let l' ≝ joint_if_entry … fn in
    228       ! st ← goto … ge l' (set_regs p regs st) ;
     228      let st ≝ set_regs p regs st in
     229      let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
     230      ! newpc ← address_of_label … ge pointer_in_fn l' ;
     231      let st ≝ set_pc … newpc st in
    229232       ret ? 〈 E0, st〉
    230233    | External fn ⇒
     
    235238         components; instead I am making a singleton out of it. To be
    236239         fixed once we fully implement external functions. *)
    237         let vs ≝ [mk_val ? evres] in
     240      let vs ≝ [mk_val ? evres] in
    238241      ! st ← set_result … vs st;
    239242      let st ≝ set_pc … ra st in
    240243        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    241244     ].
     245% qed.
    242246
    243247definition eval_call_id:
Note: See TracChangeset for help on using the changeset viewer.