Changeset 1709 for src/joint


Ignore:
Timestamp:
Feb 17, 2012, 11:52:36 AM (8 years ago)
Author:
mulligan
Message:

Changes to the execution of the MOVC instruction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_paolo.ma

    r1643 r1709  
    177177  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    178178  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    179   OK … (set_m … m (set_sp … isp st)).
     179  OK … (set_m … m (set_isp … isp st)).
    180180
    181181definition pop: ∀p. state p → res (state p × beval) ≝
     
    183183  let isp ≝ isp ? st in
    184184  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    185   let ist ≝ set_sp … isp st in
     185  let ist ≝ set_isp … isp st in
    186186  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    187187  OK ? 〈st,v〉.
Note: See TracChangeset for help on using the changeset viewer.