MCPcopy Create free account
hub / github.com/argotorg/solidity / BVSignedCleanupFunction

Function BVSignedCleanupFunction

test/formal/util.py:29–37  ·  view source on GitHub ↗
(x, type_bits)

Source from the content-addressed store, hash-verified

27 return BitVecVal(-(1 << (type_bits - 1)), n_bits)
28
29def BVSignedCleanupFunction(x, type_bits):
30 assert x.size() >= type_bits
31 sign_mask = BitVecVal(1, x.size()) << (type_bits - 1)
32 bit_mask = (BitVecVal(1, x.size()) << type_bits) - 1
33 return If(
34 x & sign_mask == 0,
35 x & bit_mask,
36 x | ~bit_mask
37 )
38
39def BVUnsignedCleanupFunction(x, type_bits):
40 assert x.size() >= type_bits

Calls 2

IfClass · 0.50
sizeMethod · 0.45

Tested by

no test coverage detected