符号执行

今天看《开发者测试》时，被符号执行那一块弄得一头雾水，而且还突然冒出一个“约束求解器”，搜了半天还弄不明白，结果往后一翻一看图弄明白了，特此记录。

书上所讲：

上面的意思就是：
静态符号执行过程，首先生成符号执行树，然后约束求解器（SMT）求解，当SMT发现一个解时，返回，over。
附两张图：


这个目的目测就是：防止程序中出现无法到达的部分、或者获取程序输入约束条件。