Method test_ashr_negative

tests/test_z3_semantic.py:561–563

Arithmetic shift right of negative value fills with 1s.

(self, kernel)

        assert _try_prove(AShr(BitVecVal(64, 8), 2) == BitVecVal(16, 8))

    def test_ashr_negative(self, kernel):
        """Arithmetic shift right of negative value fills with 1s."""
        assert _try_prove(AShr(BitVecVal(0x80, 8), 2) == BitVecVal(0xE0, 8))


class TestBVUniversal: