search

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
50 stars 13 forks source link

Fix DPI.Logical_imm instructions to account for aliases TST and MOV #135

Closed shigoel closed 1 week ago

shigoel commented 1 week ago

Description:

Fix spec. of DPI.Logical_imm instructions to account for the behavior of ORR's alias MOV and ANDS's alias TST.

Testing:

make all succeeded on my M3.

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

pennyannn commented 1 week ago

Update description of the PR.