Feature #8175: Add support for high-level interface to static verifiers - Klever - Open-Source Projects

Actions

Copy link

Feature #8175

open

Add support for high-level interface to static verifiers

Added by Evgeny Novikov almost 7 years ago. Updated almost 7 years ago.

Status:

New

Priority:

High

Assignee:

Category:

Target version:

Start date:

04/26/2017

Due date:

% Done:

Estimated time:

Published in build:

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).

Related issues 2 (1 open — 1 closed)

Actions

Copy link

Updated by Alexey Khoroshilov almost 7 years ago

Adapters is definitely a good pattern for integration external tools.
Good to see we have it again.

Actions

Copy link

Updated by Evgeny Novikov almost 7 years ago

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).

Actions

Copy link