Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889

关于

Creusot 是一个用于Rust代码的 演绎验证器。它验证您的代码不会发生恐慌、溢出和断言失败。通过添加注释，您可以进一步验证您的代码是否执行了 正确 的操作。

Creusot通过将Rust代码翻译为WhyML（Why3 的验证和规范语言）来工作。用户可以利用Why3的全部功能来（半）自动释放验证条件！

有关技术细节，请参阅 ARCHITECTURE.md。

帮助和讨论

如果您需要使用Creusot的帮助或想进行讨论，您可以在 讨论论坛 上发布或加入我们的 Zulip聊天！

引用Creusot

如果您想在学术环境中引用Creusot，我们鼓励您使用我们的 ICFEM'22 出版物。

验证示例

为了了解使用Creusot验证程序的样子，我们鼓励您查看我们的部分测试套件

• 将向量清零
• 在向量的二分搜索
• 对向量进行排序
• IterMut
• 规范化If-Then-Else表达式

更多示例请见 creusot/tests/should_succeed。

使用Creusot构建的项目

• CreuSAT 是一个用Rust编写的已验证SAT求解器，并用Creusot进行验证。它真正将工具推向了极限，并展示了“实战”的样子。
• 另一个大型项目正在筹备中 :)

以用户身份安装Creusot

1. 安装 rustup，以获取合适的Rust工具链
2. 获取 opam，OCaml的包管理器
3. 克隆 creusot 仓库，然后 进入 creusot 目录 进行后续设置。

   $ git clone https://github.com/creusot-rs/creusot
   $ cd creusot
   

4. 设置 Why3 和 Alt-Ergo。创建一个包含 why3 和 alt-ergo 的本地 opam 切换

   $ opam switch create -y . ocaml.4.14.1
   $ eval $(opam env)
   

   这将构建 why3、alt-ergo 以及它们的 OCaml 依赖项，并在本地 _opam 目录中。
5. 构建 Creusot

   $ cargo install --path creusot-rustc
   $ cargo install --path cargo-creusot
   

   这将构建 cargo-creusot 和 creusot-rustc 可执行文件，并将它们放置在 ~/.cargo/bin 中。
6. 设置 Creusot

   $ cargo creusot setup install
   

   这将下载额外的求解器（Z3、CVC4、CVC5）并配置 Why3 以使用它们。

升级Creusot

1. 进入之前安装Creusot时使用的克隆的Creusot git仓库
2. 更新Creusot的源代码

   $ git pull
   

3. 如有需要，升级Why3和Alt-Ergo

   $ eval $(opam env)
   $ opam update
   $ opam install .
   

4. 重新构建和重新安装Creusot

   $ cargo install --path creusot-rustc
   $ cargo install --path cargo-creusot
   

5. 重新运行Creusot的设置

   $ cargo creusot setup install
   

使用Creusot和Why3进行验证

请参阅 指南。

在Creusot上进行开发

请参阅 HACKING.md 了解在Creusot代码库上进行开发的工作流程。