在angr和claripy中,可以使用以下方式定义非连续约束:
import angr
import claripy
proj = angr.Project('/path/to/binary')
a = claripy.BVS('a', 32)
constraint = claripy.And(a[0:7] == claripy.BVV(0x5A, 8),
a[8:15] == claripy.BVV(0x41, 8),
a[16:23] == claripy.BVV(0x47, 8),
a[24:31] == claripy.BVV(0x4F, 8))
state = proj.factory.entry_state()
state.add_constraints(constraint)
sm = proj.factory.simulation_manager(state)
sm.run()
上一篇:按构造函数比较值