You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
74 lines
1.7 KiB
74 lines
1.7 KiB
#!/bin/bash
|
|
|
|
# CBMC SpecGen 完整流程一键测试脚本
|
|
# 实现从代码输入到验证结果的完整自动化流程
|
|
|
|
echo "🚀 CBMC SpecGen 完整流程测试"
|
|
echo "================================="
|
|
|
|
# 检查Python环境
|
|
if ! command -v python3 &> /dev/null; then
|
|
echo "❌ Python3 未安装"
|
|
exit 1
|
|
fi
|
|
|
|
# 检查CBMC
|
|
if ! command -v cbmc &> /dev/null; then
|
|
echo "❌ CBMC 未安装"
|
|
echo "请安装CBMC: sudo apt-get install cbmc"
|
|
exit 1
|
|
fi
|
|
|
|
# 检查API密钥文件
|
|
if [ ! -f "api_key.txt" ]; then
|
|
echo "❌ API密钥文件不存在: api_key.txt"
|
|
echo "请创建API密钥文件"
|
|
exit 1
|
|
fi
|
|
|
|
# 检查测试文件
|
|
if [ ! -f "testfiles/simple_test.c" ]; then
|
|
echo "❌ 测试文件不存在: testfiles/simple_test.c"
|
|
exit 1
|
|
fi
|
|
|
|
# 创建输出目录
|
|
mkdir -p output
|
|
|
|
# 运行完整测试
|
|
echo "📥 输入文件: testfiles/simple_test.c"
|
|
echo "📤 输出目录: output"
|
|
echo ""
|
|
|
|
# 运行Python脚本
|
|
python3 complete_flow_test.py --input testfiles/simple_test.c --verbose
|
|
|
|
if [ $? -eq 0 ]; then
|
|
echo ""
|
|
echo "✅ 完整流程测试成功完成!"
|
|
|
|
# 显示生成的文件
|
|
echo ""
|
|
echo "📁 生成的文件:"
|
|
ls -la output/ | tail -n +4
|
|
|
|
# 获取最新生成的文件
|
|
LATEST_ASSERTION=$(ls -t output/*_with_assertions_*.c | head -1)
|
|
LATEST_RESULT=$(ls -t output/*_verification_result_*.txt | head -1)
|
|
LATEST_SUMMARY=$(ls -t output/*_summary_*.txt | head -1)
|
|
|
|
echo ""
|
|
echo "📄 最新生成的文件:"
|
|
echo " 断言代码: $LATEST_ASSERTION"
|
|
echo " 验证结果: $LATEST_RESULT"
|
|
echo " 测试摘要: $LATEST_SUMMARY"
|
|
|
|
echo ""
|
|
echo "📋 测试摘要内容:"
|
|
cat "$LATEST_SUMMARY"
|
|
|
|
else
|
|
echo ""
|
|
echo "❌ 完整流程测试失败!"
|
|
exit 1
|
|
fi |