经过多次尝试，我发现了问题原因。主要是去混淆的这个函数存在char*入参，而我在初始化的时候没有提供该参数的信息，导致angr将其当为默认符号化参数，长度会一直增加，在第一个循环中出不来，就导致了死循环。

解决方法也很简单，使用gdb调试下，查看参数通过哪个寄存器传递，然后使用blank_state获得开始的状态后，对指定寄存器进行初始化。

经过调试，发现我的程序通过rdi传递指针，我就在内存中找了块空间存放符号化变量，然后地址传给rdi就好了。

注意，这里有个问题，不能使用堆栈存放符号化变量，会导致程序只执行一次循环就退出，原因未知，待深入研究。

添加的代码如下：

flag_chars = [claripy.BVS('%d' % i, 8) for i in range(4)]   
flag = claripy.Concat(*flag_chars + [claripy.BVV(0,32)])
state.regs.rdi = 0x600FB0
passwd = 0x600FB0 # 找到内存空间
state.memory.store(passwd, flag)
state.memory.store(passwd+8, 0)

还原后的汇编F5结果如下：

总结：感觉自己能遇到这个问题，一是对angr的理解不够深入，会的东西太少；二是粗心，没有考虑到参数的初始化问题。说到底还是自己太菜了，55555

天水姜伯约 //Ver1, 可以去掉bogus if (x * (x + 1) % 2 == 0) { bogus(); } //Ver2, 应该不可以去掉bogus，因为angr会在第一个循环进入路 ...

我今天按照你说的第二种代码编了个程序试了下，用原来的代码确实不行，在 

proj.factory.simgr(state)

中加入 veritesting=True 参数也不行。

感觉这种情况应该需要人工干预去处理了。

尝试：

我的源码反汇编之后是

因为这里符号执行是为了找到执行过的块，考虑到后面的if条件永假，所以我这边做了个简单处理：循环执行一次就剪该链路。

处理后的执行代码如下：

while len(simgr.active) > 0:
    for active in simgr.active:
        if active.addr not in blocks and active.addr == 0x4007a2: # 指定该块，执行过后就剪掉
            simgr.active.remove(active)
        blocks.discard(active.addr)
        # hook call instructions
        ......

    simgr.step()

最后的结果反汇编如下

可以看到是去除了。

思考：

我这种处理方法是特例，因为变量 i 对后续代码的影响有限。

要是后续有使用 i 且产生分支，我觉得有两种处理方法，都是人工干预

1、在剪掉这个路径后，在下一个代码块开始时，手动对循环中变化的变量（本例中为 i ）进行符号化赋值，或者直接跳过这个循环，然后符号化赋值。

2、针对本例 for 循环这种单输入输入的代码块，进入前切换到模拟执行（使用类似unicorn工具），该块代码执行完后，切换到符号执行模式，同步变量。思路类似于symbion，也就是帖子 http://www.hackdig.com/09/hack-467817.htm 提到的第四种方法。

感觉第一种方法容易实现些。第二种方法工作量比较大，不知道业内有没有成熟的方法。

当然，这只是我的个人看法，如果有什么不对的地方，希望大佬指针，也希望论坛的朋友们提出建议。