Jim Grundy

Panic on Pure Function With Loop

6

The following code will crash the Prusti compiler (Version prusti-dev-v-2021-06-21-1121) with this message: ``` thread 'rustc' panicked at 'Procedure DefId(0:5 ~ all_issues1[ca9e]::f) contains a loop', prusti-viper/src/encoder/pure_function_encoder.rs:84:14 note: run with `RUST_BACKTRACE=1`...

Add a page of documentation with step-by-step instructions on how to make a release of the starter kit.

The ability to prove properties in parallel is valuable and so we should have it seamlessly integrated into the starter-kit so that simply setting some options in your makefile is...

Important aspects of the behavior of the starter kit are controlled by environment variables. There should be a section in the documentation alerting users to this, giving them an idea...

Remove dependency on git to use starter-kit

3

Right now, if you attempt to use the starter kit outside of a Git repo you will get the following result: ``` cbmc % cbmc-starter-kit-setup Traceback (most recent call last):...

Ease use of starter-kit for "hello world" type explorations

2

Suppose I'm playing around with CBMC and starter-kit for perhaps the first time, evaluating it. Probably what I want to do is write and run a kind of "hello-world" type...