Changeset 2916


Ignore:
Timestamp:
Mar 20, 2013, 12:33:24 PM (8 years ago)
Author:
tranquil
Message:

corrected yet another endianness bug in load and store

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/RTLabsToRTL.ma

    r2915 r2916  
    469469    ]
    470470  ].
    471   >length_map @prf qed.
     471  >length_map >prf % qed.
    472472 
    473473definition translate_notint :
    … …  
    913913      [tmp_addr_l ; tmp_addr_h]
    914914      [tmp_addr_l ; tmp_addr_h]
    915       [zero_byte ; (int_size : Byte)] ? ? @@ acc in
     915      [(int_size : Byte) ; zero_byte ] ? ? @@ acc in
    916916  foldr … f [ ] destrs).
    917917@hide_prf
    … …  
    931931      [tmp_addr_l ; tmp_addr_h]
    932932      [tmp_addr_l ; tmp_addr_h]
    933       [zero_byte ; (int_size : Byte)] ? ? @@ acc in
     933      [(int_size : Byte) ; zero_byte ] ? ? @@ acc in
    934934  foldr … f [ ] srcrs).
    935935@hide_prf [ <addr_prf ] % qed.
Note: See TracChangeset for help on using the changeset viewer.