HomeIsabelle/Phabricator

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

Authored by dcjm on Jun 19 2020, 9:37 AM.

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