MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / test_signext_negative

Method test_signext_negative

tests/test_z3_semantic.py:621–623  ·  view source on GitHub ↗

Sign-extending 0xFF (= -1 signed) gives 0xFFFF.

(self, kernel)

Source from the content-addressed store, hash-verified

619 assert _try_prove(SignExt(8, BitVecVal(0x7F, 8)) == BitVecVal(0x007F, 16))
620
621 def test_signext_negative(self, kernel):
622 """Sign-extending 0xFF (= -1 signed) gives 0xFFFF."""
623 assert _try_prove(SignExt(8, BitVecVal(0xFF, 8)) == BitVecVal(0xFFFF, 16))
624
625 def test_rotate_left_identity(self, kernel):
626 x = BitVec("x", 8)

Callers

nothing calls this directly

Calls 3

_try_proveFunction · 0.90
SignExtFunction · 0.90
BitVecValFunction · 0.90

Tested by

no test coverage detected