viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.56k stars 108 forks source link

Support domains #94

Open mueller55 opened 4 years ago

mueller55 commented 4 years ago

It would be useful to lift Viper's domains to Prusti. One of the main questions is the language design for that, for instance, to what extent we can build on existing Rust features. Instead of general domains, we might also want to provide a more limited feature such as ADTs.

fpoli commented 4 years ago

Have you seen this?

https://github.com/viperproject/prusti-dev/blob/7b5b2f677d4809b6a110d578572ccf638a535ca8/prusti-common/src/vir/ast/domain.rs#L10-L16

Christoph recently added it.

cmatheja commented 4 years ago

@fpoli I think the issue is not about generating Viper domains inside of Prusti (which is indeed supported), but giving programmers a mechanism to write custom domains in Rust programs that are then verified with Prusti.

fpoli commented 4 years ago

Ah, I see. Thanks for the clarification.