codedetect/docs/examples/basic-usage-tutorial.md

# CodeDetect基础使用教程

## 概述

本教程将指导您完成CodeDetect的基础使用，从安装配置到运行第一次代码验证。

## 前提条件

- Python 3.8或更高版本
- CBMC (C Bounded Model Checker) 安装
- 基本的C语言知识

## 第一步：安装

### 1.1 克隆仓库

```bash
git clone https://github.com/your-username/codedetect.git
cd codedetect
```

### 1.2 安装Python依赖

```bash
pip install -r requirements.txt
pip install -r requirements-dev.txt
```

### 1.3 安装CBMC

**Ubuntu/Debian:**
```bash
sudo apt-get update
sudo apt-get install cbmc
```

**macOS:**
```bash
brew install cbmc
```

### 1.4 验证安装

```bash
# 检查CBMC安装
cbmc --version

# 检查Python依赖
python -m pytest tests/unit/ -v
```

## 第二步：基本使用

### 2.1 准备测试代码

创建一个简单的C文件 `test_function.c`：

```c
int add(int a, int b) {
    return a + b;
}
```

### 2.2 使用命令行界面

```bash
# 运行代码验证
python -m src.main verify test_function.c

# 生成规范
python -m src.main generate-spec test_function.c --function add

# 运行完整分析
python -m src.main analyze test_function.c
```

### 2.3 使用Web界面

启动Web服务器：

```bash
python -m src.ui.web_app
```

然后在浏览器中访问 `http://localhost:5000`

## 第三步：验证结果解读

### 3.1 成功验证

```
VERIFICATION SUCCESSFUL
Property __CPROVER_assert: OK
Property __CPROVER_assert: OK

** 1 of 1 properties verified (2 PASS) **
```

**含义：**
- 所有属性都已验证通过
- 代码在给定条件下是安全的

### 3.2 验证失败

```
VERIFICATION FAILED
Property __CPROVER_assert: FAILED

Violated property:
  File test.c, line 2
  assertion
  arr[index]

STATE:
  - Line 2: arr[index]
  - index: 5
  - size: 3
```

**含义：**
- 发现了潜在的安全问题
- 需要修复代码或添加保护措施

## 第四步：进阶功能

### 4.1 使用突变测试

```bash
# 生成测试突变
python -m src.main mutate test_function.c --function add

# 运行突变验证
python -m src.main verify-mutants test_function.c
```

### 4.2 批量处理

```bash
# 处理整个目录
python -m src.main batch-verify ./src/

# 生成报告
python -m src.main generate-report --format html
```

### 4.3 配置文件

创建配置文件 `config.yaml`：

```yaml
verification:
  cbmc:
    options:
      - "--bounds-check"
      - "--pointer-check"
      - "--unwind 10"
    timeout: 30

  generation:
    llm:
      model: "gpt-4"
      temperature: 0.3
      max_tokens: 1000
```

## 第五步：故障排除

### 5.1 常见问题

**CBMC未找到：**
```bash
# 确保CBMC在PATH中
which cbmc

# 如果没有，手动设置
export CBMC_PATH=/path/to/cbmc
```

**Python依赖问题：**
```bash
# 重新安装依赖
pip install --force-reinstall -r requirements.txt
```

**内存不足：**
```bash
# 减少验证深度
python -m src.main verify test.c --unwind 5
```

### 5.2 性能优化

- 使用 `--unwind` 限制递归深度
- 增加 `--timeout` 防止长时间运行
- 使用 `--jobs` 进行并行处理

## 第六步：最佳实践

### 6.1 编写可验证的代码

```c
// 好的实践：包含边界检查
int safe_access(int* arr, int size, int index) {
    if (arr == NULL || size <= 0 || index < 0 || index >= size) {
        return 0;
    }
    return arr[index];
}

// 避免的做法：没有边界检查
int unsafe_access(int* arr, int size, int index) {
    return arr[index]; // 潜在的缓冲区溢出
}
```

### 6.2 规范编写建议

- 使用清晰的断言
- 考虑边界条件
- 添加前置条件
- 记录假设条件

### 6.3 持续集成

将CodeDetect集成到CI/CD流程中：

```yaml
# .github/workflows/verify.yml
name: Code Verification
on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v2
      - name: Setup Python
        uses: actions/setup-python@v2
        with:
          python-version: 3.9
      - name: Install dependencies
        run: |
          pip install -r requirements.txt
          sudo apt-get install cbmc
      - name: Run verification
        run: python -m pytest tests/ -v
```

## 下一步

完成本教程后，您可以：

1. 阅读 [API参考文档](../api-reference.md)
2. 探索 [开发者指南](../developer-guide.md)
3. 查看 [FreeRTOS示例](../freertos-examples/)
4. 尝试 [高级配置选项](../configuration.md)

## 获取帮助

- 查看 [用户手册](../user-manual.md)
- 提交 [Issue](https://github.com/your-username/codedetect/issues)
- 加入社区讨论