Zack Grannan

Add `nextPageAsync` method

1

Adds a new method to paginate over a response using `executeAsyncBase` instead of `execute`

rustc panic Option::unwrap() at prusti-viper/src/utils/type_visitor.rs:272:50

5

While running `prusti-rustc` on the following code: ```rust struct Params { letter: char, password: String } fn check(params: Params) -> usize { return params.password.chars().filter(|c| c == &params.letter).count(); } fn main()...

Cannot add `#[requires]` annotation to trait function

5

The following code: ```rust extern crate prusti_contracts; use prusti_contracts::*; trait Foo { fn bar(); } impl Foo for i32 { #[requires(true)] fn bar() {} } fn main() {} ``` fails...

Enable choice of term ordering for REST

1

This PR allows the user to change the termination ordering for use in REST with a flag: `--rest-ordering`. Available options are: - `rpo`: Recursive Path Ordering (default) - `kbo`: Knuth-Bendix...

Cannot reflect GADT definition using DataKinds

9

Minimal example: ```haskell {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} data Nat = Z | S Nat data Op a b where Pop :: Op ('S n) n {-@...

```haskell {-@ inline id' @-} id' x = x {-@ arith :: { id' ( 2

Trying to verify the following code: ```haskell {-@ LIQUID "--ple" @-} {-@ LIQUID "--reflection" @-} {-@ measure f_subset :: Int -> Int -> Bool @-} {-@ assume f_subset :: arg0...

MacOS Support

3

According to the README: > Currently lacking support for Windows, macOS, and web. Support for these platforms will be created when there is a need for them. Starts with a...

Prusti generates invalid Viper code for the following file: ```rust use prusti_contracts::*; #[derive(Copy, Clone, PartialEq, Eq)] struct AccountID(u32); #[pure] fn check_eq(from: &AccountID) -> bool { from != from } fn...