The UPPAAL bytecode seems to support a STORE instruction, which puts a value into a register but specifies both arguments on the stack.
This is problematic because it interferes with the current approach to rename registers to a fixed range. To support this instruction, we would need to explicitly add this renumbering to the semantics.
The UPPAAL bytecode seems to support a
STOREinstruction, which puts a value into a register but specifies both arguments on the stack.This is problematic because it interferes with the current approach to rename registers to a fixed range. To support this instruction, we would need to explicitly add this renumbering to the semantics.