Le marteau-pilon, 铁匠和钢铁厂 Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889

关于

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

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上修改

有关在Creusot代码库上修改的开发者工作流程信息，请参阅HACKING.md。