HomeIsabelle/Phabricator

When loading from the stack always load a native word, i.e. 64-bits in 32-in-64.

Description

When loading from the stack always load a native word, i.e. 64-bits in 32-in-64. This is necessary
because the value could be a 64-bit value if it is an address of a "container" (a tuple on the stack).

Details

Provenance
dcjmAuthored on Jun 19 2020, 9:37 AM
Parents
rPOLYML5369884001c7: Invalid constant indexes for arrays or vectors can result in an overflow when…
Branches
Unknown
Tags
Unknown