Prusti Examples

[EmilyOng]

https://github.com/FabianWolff/closure-examples/tree/master

Program	Prusti	Heifer	Status	Purpose	Remark
all	code	code	✘		Possible issues due to usage of pure predicates
any	code	code	✘		Possible issues due to usage of pure predicates
blameassgn	code	code	✔	From Contracts for Higher-Order functions	Preconditions on function parameters are supported
cl_returned	code	code	✔	Returning a function from another function
counter	code	code	✔
delegation	code	code	✘	Passing a function g into another function f and verifying that g's preconditions hold when it is called in f. Invocation of h and declaration of other variables in f is supposed to make the verification harder (Example 10 from Specification and Verification of Closures)	This relies heavily on the ownership feature in Rust
filter	code	code	✘		Requires increasing the unfolding bound/some use of pure predicates
fold	code	code	✘		Possible issues due to usage of pure predicates
fold_list_rev	code 1 code 2
for_each	code	code	✘
map	code	code	✘		Specific examples requires increasing the unfolding bound
option_map	code			Currently, matching Some and None is unsupported
repeat_with_n	code	code	✔
result_uoe	code

[EmilyOng]

Note on syntax, w.r.t. to https://github.com/FabianWolff/closure-examples/tree/master

---