前端处理结束后
cbmc_parse_options.cpp:647进入验证步骤- 不同的verifier有不同的验证策略（是否在发现错误后停止等），但都会调用checker（主要分multi-path和single-path，以及是否在符号执行后进行求解）
- bmc使用的策略在
bmc_util.cpp:setup_symex中被设置 - 执行过程中，程序转换为
symex_target_equationt即一系列SSA形式的指令。deagle所需的oc边都会存在这里 deagle implementation notes- symex dispatcher在
goto_symext::execute_next_instruction - 具体细节参见 CBMC Symex and GOTO program instructions
- single_path的symex一次探索一个路径（氛围fifo和lifo两种策略），同时将遇到的的分支加入worklist中，上层的checker会决定是否继续进行探索；默认情况下是探索所有路径并形成一个equation进行求解。
- symex dispatcher在
symex_from_entry_point_of开始符号执行- 结束后，
postprocess_equation中对记录的oc边进行了处理，最终在SC model中被告知Deagle的求解器。