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

关于

Creusot 是一个用于Rust代码的 演绎验证器。它验证你的代码是否安全，避免panic、溢出和断言失败。通过添加注解，你可以进一步验证你的代码是否执行了 正确的 操作。

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

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

帮助和讨论

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

引用Creusot

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

验证示例

为了了解使用Creusot验证程序的过程，我们鼓励你查看我们的测试套件

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

更多示例请参阅creusot/tests/should_succeed。

使用Creusot构建的项目

• CreuSAT 是一个经过验证的 SAT 求解器，用 Rust 编写并使用 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 代码库上黑客攻击的开发者工作流程。