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

关于

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

Creusot 通过将 Rust 代码转换为 WhyML，Why3 的验证和规范语言，来工作。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)
   

   这将在本地的_opam目录中构建why3、alt-ergo及其OCaml依赖项。
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代码库上开发的开发者工作流程。