Skip to content

New features and improvements - #216

Closed
cedihegi wants to merge 83 commits into
viperproject:masterfrom
cedihegi:master
Closed

New features and improvements#216
cedihegi wants to merge 83 commits into
viperproject:masterfrom
cedihegi:master

Conversation

@cedihegi

@cedihegi cedihegi commented Mar 1, 2023

Copy link
Copy Markdown

Practical Work project by @jthomme1 and me, supervised by @Aurel300.

The new features include:

  • Show quantifier instantiations via inlay hints, and split by which verification caused them on hover
  • Display chosen viper quantifier triggers on hover
  • Selective verification via code-lenses
  • Generate templates for external specifications via code-actions
  • Get per method verification results and display them with gutter symbols
  • Display per method verification time and whether the result was cached or not
  • Verification results, diagnostics and quantifier messages are processed asynchronously, which allows users to see progress while prusti is still running.
  • (optional and rather experimental) For function calls, users can "peek definitions" for that call to see its contract. This feature is turned off by default and it's design is more of a temporary proof of concept.

Additionally, @jthomme1 did a rather extensive refactoring of the diagnostics and verification parts.

To use these new features, prusti needs to be at least at version 0.3.0.

Cedric and others added 30 commits October 23, 2022 14:15
…or crate

and codelenses only updating after reloading a file or editing it.
verifying different files or crates, not just the info
of the most recent one is stored.
Not yet actually depending on the verification's result.
…s. However the textual decorators just stack in subsequent verifications so they will have to be removed at some point
@Aurel300

Aurel300 commented Mar 2, 2023

Copy link
Copy Markdown
Member

@Aurel300 this means that we should publish a >=0.3.0 Prusti release before merging this PR.

Yes, I know, that's what viperproject/prusti-dev#1334 will do.

@Aurel300

Aurel300 commented Apr 4, 2026

Copy link
Copy Markdown
Member

Superseded by #262.

@Aurel300 Aurel300 closed this Apr 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants