..

creusot 安装

creusot 是一个针对Rust语言的验证器。其通过将Annotated Rust code转为Why3进行验证。

creusot GitHub ： https://github.com/creusot-rs/creusot。

creusot 文档： https://creusot-rs.github.io/creusot/guide/

安装过程

安装Rust: https://www.rust-lang.org/tools/install

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

安装opam： https://opam.ocaml.org/doc/Install.html

bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)"

安装依赖：

rustup component add rust-src rustc-dev llvm-tools-preview

进入到creusot目录中，运行安装脚本：

./INSTALL

如果需要使用已经安装好的why3，确保why3, why3-ide, why3find已经安装到当前环境中，使用以下命令：

./INSTALL --external why3-and-why3find

等待安装完毕，脚本会自动安装CVC5，CVC4，Z3，Alt-Ergo等证明器。安装结束后，使用opam切换ocaml环境

eval $(opam env --switch=/home/user/.local/share/creusot)

新建一个rust项目

cargo creusot new project-name --creusot-contracts /PATH/TO/CREUSOT/creusot-contracts

使用prover进行证明

cargo creusot prove