prusti dev:基于Viper验证基础结构的Rust静态验证程序 源码

普鲁斯蒂 是Rust的原型验证器,建立在。 默认情况下,Prusti通过证明unreachable!()和panic!()类的语句unreachable!()来验证是否存在恐慌。 可以使用配置标志启用溢出检查,否则所有整数都将被视为无界。 在Prusti中,可以使用批注指定函数的功能行为,其中包括前置条件,后置条件和循环不变式。 该工具会检查它们,并在代码不符合所提供的规范时报告错误消息。 有关教程和更多信息,请查阅。 使用Prusti 试用Prusti的最简单方法是使用VS Code的扩展。 另外,如果您希望从命令行使用Prusti,则有两个选项: 从下载适用于Ubuntu,Wi