Skip to content

Commit

Permalink
lint
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Jun 29, 2024
1 parent 9dc0791 commit 0b1fbf5
Showing 1 changed file with 10 additions and 0 deletions.
10 changes: 10 additions & 0 deletions src/halmos/assertions.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ class VmAssertion:
"""
Forge Standard Assertions
"""

cond: BitVecRef
msg: Optional

Expand Down Expand Up @@ -68,40 +69,48 @@ def vm_assert(bop: str, typ: str, log: bool = False):
if not arr:
# bool, uint256, int256, address, bytes32
if not is_bytes:

def _f(arg):
v1 = extract_bytes(arg, 4, 32)
v2 = extract_bytes(arg, 36, 32)
cond = mk_cond(bop, v1, v2)
msg = extract_string_argument(arg, 2) if log else None
return VmAssertion(cond, msg)

return _f

# bytes, string
else:

def _f(arg):
v1 = extract_bytes_argument(arg, 0)
v2 = extract_bytes_argument(arg, 1)
cond = mk_cond(bop, v1, v2)
msg = extract_string_argument(arg, 2) if log else None
return VmAssertion(cond, msg)

return _f

else:
# bool[], uint256[], int256[], address[], bytes32[]
if not is_bytes:

def _f(arg):
v1 = extract_bytes32_array_argument(arg, 0)
v2 = extract_bytes32_array_argument(arg, 1)
cond = mk_cond(bop, v1, v2)
msg = extract_string_argument(arg, 2) if log else None
return VmAssertion(cond, msg)

return _f

# bytes[], string[]
else:

def _f(arg):
# TODO: implement extract_bytes_array
raise NotImplementedError(f"assert {bop} {typ}[]")

return _f


Expand All @@ -111,6 +120,7 @@ def _f(arg):
cond = test(actual, expected)
msg = extract_string_argument(arg, 1) if log else None
return VmAssertion(cond, msg)

return _f


Expand Down

0 comments on commit 0b1fbf5

Please sign in to comment.