HomeIsabelle/Phabricator

Bug fix for X86 code-generator. If a work register is required for a JumpLoop…

Description

Bug fix for X86 code-generator. If a work register is required for a JumpLoop it must be distinct from target registers.

Details

Provenance
dcjmAuthored on Nov 15 2023, 8:30 AM
Parents
rPOLYML4a1e4ec7080d: Fix a couple of problems with the GMP version of left shift.
Branches
Unknown
Tags
Unknown