mirror of https://github.com/ConsenSys/mythril
blockchainethereumsmart-contractssoliditysecurityprogram-analysissecurity-analysissymbolic-execution
You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
56 lines
1.1 KiB
56 lines
1.1 KiB
from mythril.laser.smt import Solver, symbol_factory
|
|
import z3
|
|
|
|
|
|
def test_decls():
|
|
# Arrange
|
|
solver = Solver()
|
|
x = symbol_factory.BitVecSym("x", 256)
|
|
expression = x == symbol_factory.BitVecVal(2, 256)
|
|
|
|
# Act
|
|
solver.add(expression)
|
|
result = solver.check()
|
|
model = solver.model()
|
|
|
|
decls = model.decls()
|
|
|
|
# Assert
|
|
assert z3.sat == result
|
|
assert x.raw.decl() in decls
|
|
|
|
|
|
def test_get_item():
|
|
# Arrange
|
|
solver = Solver()
|
|
x = symbol_factory.BitVecSym("x", 256)
|
|
expression = x == symbol_factory.BitVecVal(2, 256)
|
|
|
|
# Act
|
|
solver.add(expression)
|
|
result = solver.check()
|
|
model = solver.model()
|
|
|
|
x_concrete = model[x.raw.decl()]
|
|
|
|
# Assert
|
|
assert z3.sat == result
|
|
assert 2 == x_concrete
|
|
|
|
|
|
def test_as_long():
|
|
# Arrange
|
|
solver = Solver()
|
|
x = symbol_factory.BitVecSym("x", 256)
|
|
expression = x == symbol_factory.BitVecVal(2, 256)
|
|
|
|
# Act
|
|
solver.add(expression)
|
|
result = solver.check()
|
|
model = solver.model()
|
|
|
|
x_concrete = model.eval(x.raw).as_long()
|
|
|
|
# Assert
|
|
assert z3.sat == result
|
|
assert 2 == x_concrete
|
|
|