Feature #8175
open
Add support for high-level interface to static verifiers
Added by Evgeny Novikov about 7 years ago.
Updated almost 7 years ago.
Description
Some properties can require specific options to be specified for static verifiers. For instance, the most well known example is a bit precise analysis that is turned off by default since it requires more resources while it isn't necessary usually - some properties, e.g. checking bit masks, can't be gracefully checked without it.
I suppose to develop step by step the high-level interface to static verifiers. What is really necessary is an ability to translate high-level options into verifier specific ones. Perhaps these specific options can depend on a verifier version and other options (a configuration).
Adapters is definitely a good pattern for integration external tools.
Good to see we have it again.
Alexey Khoroshilov wrote:
Adapters is definitely a good pattern for integration external tools.
Good to see we have it again.
If by an adapter some source files are assumed then it isn't our way. Instead we are actively leveraging BenchExec capabilities.
What we still miss is a configurable configuration for software verifiers. Now it is hardcoded mostly in source code that hardens any changes but blocking issue #7451 will fix this in a near future. In addition we need some more abstract interface to avoid complicated configuration that can be very specific for software verification tools - this issue addresses this.
BTW, there is already a trivial example of such the interface that is even already configurable - we allow to merge all source files together (when #6545 will be fixed then one will be able to also pass several source files without merging). This is trivial since it likely doesn't depend on a particular software verification tool or its version/configuration. As another example #7272 can serve, there likely will be a dependency on verifier tool version and configuration like for bit precise analysis. Those versions and configurations that don't allow this will result in verification unknowns early (#8176).
- Assignee deleted (
Ilja Zakharov)
- Priority changed from Urgent to High
There are too many very high priority issues. This one can be done after really important features will be supported.
Also available in: Atom
PDF