from manticore import Manticore

m = Manticore("./a.out")

@m.hook(0x400703)
def hook(state):
        #change the builtin buffer to symbolic
        blen = 4
        cpu = state.cpu
        buf = state.new_symbolic_buffer(blen, cstring=True)
        cpu.write_bytes(cpu.read_register("RAX"), buf)
        m.context['buf'] = (buf, blen)

@m.hook(0x40071f)
def hook2(state):
        #solve for a crc
        cpu = state.cpu
        state.add(cpu.RAX == 0xff)
        buf, len = m.context['buf']
        print buf, cpu.RAX
        for i in xrange(len-1):
          print state.solve_one(buf[i])


m.verbosity = 2
m.run()