Ramla Ijaz

Further improvements to the drivers could be: - Safer interfaces to deal with physical addresses. We can use a higher level type/ trait to make sure that the buffers we...

Option type with Generics: cannot return a value of the generic type

1

I copied the Option code that was given in the user guide, and tried to convert it to use generics: ``` pub enum TrustedOption { Some(T), None, } impl TrustedOption...

I'm trying to create a struct in which one member is a linked list, and in the push() method I call the push() method of the List type, which has...

Prusti fails to compile a crate when it's part of a larger project

2

I'm not sure what's happening here because I though Prusti verified at the modularity of crates, but this exact code is verified in an independent crate. But when this crate...

encode_bitvectors not working with generics instantiated to u32

19

Hi, I'm trying to verify a piece of code using the volatile crate: ``` struct Example { a: Volatile, b: Volatile } impl Example { #[ensures(self.a.read() & 1 == 1)]...

I want to use rulinalg on Complex Matrices, mainly the svd decomposition. I don't know much about linear algebra so I wanted to know that if I add the required...

I'm using the latest dev branch with prusti assistant (Prusti version: commit 19c1732), and code that previously compiled with the latest release branch no longer does. There are two issues:...

This PR merges a verified `TrustedChunk` type into the frame allocator code. The main changes are: **trusted_chunk crate:** - submodule that contains the `TrustedChunk` type, a linked list and static...

This crate includes the `TrustedChunk` type with verified methods that can be used to prove uniqueness of the type. The modules are: - external spec: spec files for external types...

Cannot use PartialOrd in specifications despite marking them as #[pure] using external spec feature

3

I'm trying to use the basic comparison operators for a type in my specifications, and following advice I found from other issues, I've marked the Ord and PartialOrd required methods...