模块分析：export

1. 角色定位

export/ 提供 clightgen 工具，将 C 源码导出为 Coq 可读取的 AST 表示（Clight 或 Csyntax）。

2. 核心入口（ExportDriver.ml）

• 与 ccomp 类似的命令行驱动：
  • 预处理 → 解析 → 语义化
  • 支持 -csyntax 或 -clight 输出
• export_clight：
  • 调用 SimplExpr + SimplLocals
  • 可选 Clightnorm 规范化
  • 打印为 Coq .v 文件

3. 输出格式

• ExportCsyntax.ml, ExportClight.ml: 生成 Coq 语法输出
• ExportBase.ml 提供公共打印工具

4. 用途

• 便于在 Coq 中进行程序级验证（如 VST 等工具链）