cbmc/specgen/USAGE_GUIDE.md

CBMC SpecGen 使用指南

🎉 恭喜！系统已成功安装并测试通过

🚀 快速开始

1. 设置 API 密钥

   echo "your_deepseek_api_key_here" > api_key.txt
   

2. 创建测试目录

   mkdir test_samples
   cp test_sample.c test_samples/
   

3. 运行批处理

   python src/tools/batch_folder_flow.py --input-dir ./test_samples --output-dir ./output
   

📁 可用工具

🔧 生产级工具 (推荐)

python src/tools/batch_folder_flow.py --help

• 完整的批处理解决方案
• 高级文件过滤
• 综合报告 (HTML, JSON, CSV)
• 邮件通知
• 增强的错误处理

⚙️ 开发测试工具

python src/tools/batch_processor.py --help

• 核心处理引擎
• 开发者调试功能
• 单文件测试
• 性能分析

🎯 工具选择器

python src/tools/cbmc_batch.py

• 帮助选择合适的工具
• 显示工具比较

📊 功能特性

✅ 已实现的功能

• SHA1 文件名冲突防护
• 并行批处理
• 速率限制 (Token Bucket)
• CBMC 验证集成
• API 重试机制
• 恢复中断的批处理
• 多格式报告生成
• 文件大小过滤
• 详细的日志记录
• 优雅的关闭处理

🔧 技术特点

• 安全性: SHA1 哈希防止文件名冲突
• 可靠性: 指数退避重试机制
• 可扩展性: 线程池并行处理
• 可观察性: 详细的进度报告和统计
• 容错性: 优雅的错误处理和恢复

📋 测试验证

基础功能测试

python test_system.py

集成功能测试

python test_integration.py

单元测试

python -m pytest src/tests/ -v

🎯 使用示例

基础批处理

python src/tools/batch_folder_flow.py \
  --input-dir ./src \
  --output-dir ./batch_output

高性能处理

python src/tools/batch_folder_flow.py \
  --input-dir ./src \
  --output-dir ./output \
  --workers 5 \
  --rate-limit 3

恢复中断的批处理

python src/tools/batch_folder_flow.py \
  --input-dir ./src \
  --output-dir ./output \
  --resume

文件大小过滤

python src/tools/batch_folder_flow.py \
  --input-dir ./src \
  --output-dir ./output \
  --min-file-size 1 \
  --max-file-size 100

预览处理

python src/tools/batch_folder_flow.py \
  --input-dir ./src \
  --dry-run

📁 输出目录结构

output/
├── batch_reports/           # 批处理报告
│   ├── batch_summary.json
│   ├── batch_results.csv
│   └── batch_report.md
├── original_code/          # 原始代码
├── generated_code/         # 生成的断言代码
├── verification_results/   # CBMC 验证结果
├── difference_analysis/    # 差异分析
└── summaries/             # 摘要报告

🔧 配置选项

核心配置

• --workers: 并行工作线程数 (默认: 3)
• --rate-limit: API 速率限制 (默认: 2.0 请求/秒)
• --burst-capacity: 突发容量 (默认: 8)
• --timeout: 单文件超时时间 (默认: 300秒)

高级配置

• --retry-attempts: 重试次数 (默认: 3)
• --api-model: API 模型 (默认: deepseek-chat)
• --api-temperature: API 温度 (默认: 0.4)
• --generate-html-report: 生成 HTML 报告
• --email-notification: 邮件通知

🛠️ 故障排除

常见问题

1. CBMC 未安装: sudo apt-get install cbmc
2. API 密钥错误: 检查 api_key.txt 文件
3. 权限问题: 确保输出目录可写
4. 网络问题: 检查 API 连接

调试模式

python src/tools/batch_processor.py \
  --input-dir ./src \
  --output-dir ./debug \
  --single-file ./src/test.c \
  --debug-api \
  --verbose

📈 性能监控

系统提供详细的性能统计：

• 处理时间分析
• API vs CBMC 时间占比
• 成功率统计
• 吞吐量计算
• 错误分类统计

---

🎉 系统已准备就绪，开始你的 CBMC 验证之旅吧！