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 编写并使用 Creusot 验证的 SAT 求解器。它真正将工具推向了极限，并给出了“实战”的示例。
• 另一个大型项目正在进行中 :)

以用户身份安装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代码库开发工作流程的信息。