12.1 概述 用“未知数（比如代数里的x、y）”代替真实数值去“模拟运行”程序，看所有可能的分支路径会得出什么结论。 12.1.1 符号执行与正常执行的对比 想象你在玩一个解谜游戏，游戏里有很多岔路，每条岔路门口有个守卫，他会根据你手里的钥匙（输入值）决定让不让你通过。 普通执行（具体执行）： 你拿一把真的钥匙（比如 x=5, y=3）去试试，能通过就走……