Skip to content

Commit

Permalink
Use correct sort for x in #testPowerAddiSymbolic
Browse files Browse the repository at this point in the history
In this line:

self assert: (instr fieldValue: 'd') equals: 'x'

the "instr fieldValue: 'd'" is a Z3Int, so the #= down in #assert:equals:
coerces the 'x' to a Z3Int.  So now we have two 'x' symbols: a BV16 'x'
and an Int 'x', which are not necessarily equal.
The correct thing to do is to start from the same BV 'x',
and compare the Int interpretation of `d` to the signed Int
interpretation of 'x'.
  • Loading branch information
shingarov committed May 22, 2024
1 parent 82015e2 commit edb6ba1
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/ArchC-Core-Tests/AcInstrDecodeTest.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ AcInstrDecodeTest >> testPowerAddiSymbolic [
self assert: instr name equals: 'addi'.
self assert: (instr fieldValue: 'rt') equals: 0.
self assert: (instr fieldValue: 'ra') equals: 0.
self assert: (instr fieldValue: 'd') equals: 'x'.
self assert: (instr fieldValue: 'd') equals: ('x'///16) toSignedInt .

]

Expand Down

0 comments on commit edb6ba1

Please sign in to comment.