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.
cbmc/codedetect/tests/deepseek/quick_test.py

115 lines
3.0 KiB

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

#!/usr/bin/env python3
"""
快速DeepSeek v3.1测试脚本
独立运行,不依赖复杂导入
"""
import os
import requests
import json
import time
def quick_deepseek_test():
"""快速测试DeepSeek v3.1 API"""
print("🚀 DeepSeek v3.1 快速测试")
print("=" * 40)
# 检查API密钥
api_key = os.getenv('SILICONFLOW_API_KEY')
if not api_key:
print("❌ 错误: 未设置 SILICONFLOW_API_KEY 环境变量")
return
print(f"📡 连接模型: deepseek-ai/DeepSeek-V3.1")
print(f"🔑 API密钥: {api_key[:20]}...")
try:
# 测试连接
headers = {
"Authorization": f"Bearer {api_key}",
"Content-Type": "application/json"
}
data = {
"model": "deepseek-ai/DeepSeek-V3.1",
"messages": [
{
"role": "system",
"content": "你是CBMC形式化验证专家为C代码生成CBMC规约。只输出CBMC代码。"
},
{
"role": "user",
"content": """为以下C函数生成CBMC规约
int add_numbers(int a, int b) {
return a + b;
}
验证目标: functional_correctness
生成CBMC规约
\\requires ...
\\ensures ...
\\assigns ..."""
}
],
"temperature": 0.1,
"max_tokens": 512,
"stream": False
}
print("\n⏳ 调用DeepSeek v3.1 API...")
start_time = time.time()
response = requests.post(
"https://api.siliconflow.cn/v1/chat/completions",
headers=headers,
json=data,
timeout=30
)
response_time = time.time() - start_time
if response.status_code == 200:
result = response.json()
content = result['choices'][0]['message']['content']
tokens_used = result.get('usage', {}).get('total_tokens', 0)
print(f"✅ API调用成功!")
print(f"⏱️ 响应时间: {response_time:.2f}s")
print(f"🔤 消耗Token: {tokens_used}")
print(f"\n📋 生成的CBMC规约:")
print("-" * 40)
print(content)
print("-" * 40)
# 提取CBMC规约
lines = content.split('\n')
cbmc_lines = []
for line in lines:
line = line.strip()
if (line.startswith(r'\requires') or
line.startswith(r'\ensures') or
line.startswith(r'\assigns')):
cbmc_lines.append(line)
if cbmc_lines:
print(f"\n🔧 提取的CBMC规约:")
print("-" * 30)
print('\n'.join(cbmc_lines))
print("-" * 30)
else:
print(f"❌ API调用失败: {response.status_code}")
print(f"错误信息: {response.text}")
except Exception as e:
print(f"❌ 测试失败: {str(e)}")
print(f"\n🎉 快速测试完成!")
if __name__ == "__main__":
quick_deepseek_test()