2. 验证环境搭建准备：Linux操作系统选择、GCC/G++编译器安装、CMake工具安装、Python环境配置
好，咱们正式开始动手了。搭建形式化验证环境，说白了就是给你的代码找个靠谱的“家”。我见过太多人，一上来就急着写验证脚本，结果环境没配好，后面全是坑。今天咱们就把地基打牢。
2.1 Linux操作系统选择：别在起点上纠结
我个人习惯用 Ubuntu 20.04 LTS 或 22.04 LTS。为什么？因为社区活跃，遇到问题一搜就有答案。你想想看，搞形式化验证本来就够烧脑了，操作系统再跟你闹别扭，那真是雪上加霜。
当然，如果你团队统一用 Debian 或 Fedora，也没问题。核心原则就一条：包管理器要顺手。apt、yum、dnf 都行，但别用那种需要自己编译所有东西的发行版——除非你想把时间花在“如何装软件”上，而不是“如何做验证”上。
| 发行版 | 推荐指数 | 理由 |
|---|---|---|
| Ubuntu 22.04 LTS | ⭐⭐⭐⭐⭐ | 社区活跃，包新，兼容性好 |
| Debian 12 | ⭐⭐⭐⭐ | 稳定，但包略旧 |
| Fedora 40 | ⭐⭐⭐ | 够新，但有些工具要额外配置 |
| CentOS 7 | ⭐ | 别用了，真的，听我的 |
2.2 GCC/G++编译器安装：C语言的“翻译官”
形式化验证工具很多是用 C/C++ 写的，或者需要你写一些 C 扩展。所以编译器是必须的。安装其实很简单：
sudo apt update
sudo apt install build-essential
这一行命令会帮你装好 gcc、g++、make 等一堆基础工具。装完后检查一下版本：
gcc --version
g++ --version
嗯，这里要注意：版本别太老。我建议 GCC 版本至少 9.0 以上。为什么？因为 C++17 和 C++20 的特性，很多新工具都在用。我曾经在 GCC 7 上编译一个验证框架，结果报了一堆“不支持”的错误，折腾了两天才发现是编译器太旧。
sudo apt install gcc-11 g++-11 直接装，然后用 update-alternatives 切换默认版本。我试过自己编译，编译了三个小时，最后还缺依赖——那感觉，别提了。
2.3 CMake工具安装：构建系统的“项目经理”
有了编译器，还得有个工具来管理整个构建过程。CMake 就是干这个的。它不直接编译代码，而是生成 Makefile，然后让 make 去干活。
安装同样简单：
sudo apt install cmake
cmake --version
我个人建议装 CMake 3.20 以上。因为很多形式化验证工具（比如 CBMC、ESBMC）的 CMakeLists.txt 用了较新的语法。版本太低的话，你会看到一堆“CMake Error”飘过。
/usr/local 里。比用 apt 装的新很多。我在项目中就这么干，省心。
2.4 Python环境配置：脚本界的“瑞士军刀”
形式化验证里，Python 主要用来写测试脚本、解析结果、甚至驱动整个验证流程。所以 Python 环境必须配好。
先检查系统有没有自带 Python：
python3 --version
如果没有，或者版本低于 3.8，那就装一个：
sudo apt install python3 python3-pip python3-venv
这里我强烈建议你使用 虚拟环境。为什么？因为不同项目可能依赖不同版本的库，混在一起会出大问题。我曾经在一个项目里同时用了两个版本的 z3-solver，结果一个能跑，一个报错，查了半天才发现是环境冲突。
创建虚拟环境很简单：
python3 -m venv venv
source venv/bin/activate
激活后，你的终端前面会出现 (venv) 字样。这时候装的所有包都只在这个环境里生效。
z3-solver— 微软的 SMT 求解器，验证必备pycparser— 解析 C 代码的利器pytest— 写测试用例的好帮手numpy— 处理数据时可能会用到
pip install z3-solver pycparser pytest numpy
2.5 知识体系总览：一张图看懂
说了这么多，咱们用一张 SVG 图把整个环境搭建的逻辑串起来。你一看就明白：
你看，整个环境搭建就四个核心部分：操作系统打底，编译器和构建工具负责“翻译”和“组织”代码，Python 负责“调度”和“分析”。缺一个，你的验证流程就跑不顺。
2.6 验证一下：环境是否配好了？
配完环境，别急着走。咱们写个简单的 C 程序，编译一下，看看整个链路通不通：
// test.c
#include <stdio.h>
int main() {
printf("形式化验证环境搭建成功！\n");
return 0;
}
编译运行：
gcc test.c -o test
./test
如果看到“形式化验证环境搭建成功！”，那恭喜你，基础环境已经就绪。接下来，咱们就可以开始装那些真正的验证工具了。