Changeset 1457 for src/joint


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.