viperproject
New features and improvements
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.
Sure, sorry I wasn't aware of those. However, how would you resolve the unused variables warnings for example for the function provideCodeActions?
In cases like that one I don't really see how to avoid it since we have to provide this function with a given signature.
Apparently eslint ignores names starting with an underscore, and surrounding the locations with comments such as /* eslint-disable no-unused-vars */ (and enabling it after) does not work for some reason.
Can you try adding the following configuration to the "rules" section of .eslintrc?
// Report unused variables only if they don't start with "_".
// Source: https://stackoverflow.com/a/64067915/2491528
"no-unused-vars": "off",
"@typescript-eslint/no-unused-vars": [
"error",
{
"argsIgnorePattern": "^_",
"varsIgnorePattern": "^_",
"caughtErrorsIgnorePattern": "^_"
}
],
What's important to me is that there are no linting errors. Linting errors that are too restrictive should be downgraded to warnings in the linter's configuration if they still provide some value, or disabled at all if they are too noisy.
To use these new features, prusti needs to be at least at version 0.3.0.
@Aurel300 this means that we should publish a >=0.3.0 Prusti release before merging this PR.
@Aurel300 this means that we should publish a >=0.3.0 Prusti release before merging this PR.
Yes, I know, that's what https://github.com/viperproject/prusti-dev/pull/1334 will do.
