Project

General

Profile

Actions
Copy link

Feature #8092

open

Support lightweight verificaiton for rules checking API usage

Added by Evgeny Novikov about 7 years ago. Updated over 6 years ago.

Status:
New
Priority:
High
Assignee:
-
Category:
-
Target version:
-
Start date:
04/19/2017
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

In our paper I with Ilja suggested to early set verdict Safe for verification tasks that don't invoke API which usage is checked. This will extremely simplify checking of rules which aren't relevant for the most of Linux kernel modules. Moreover we will be able to get rid of annoying bugs from CIF, CIL and CPAchecker, for instance, parsing errors without much efforts (for relevant modules-rules these bugs will still exist).

Related issues 1 (1 open — 0 closed)

Related to Klever - Feature #8176: Report verification unknowns early if it is clear that verfier does not have capabilities to decide corresponding verification tasksNewIlja Zakharov04/26/2017

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov about 7 years ago

  • Assignee set to Ilja Zakharov

Let's do this and evaluate benefits.

Actions
Copy link
 #2

Updated by Evgeny Novikov almost 7 years ago

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

Actions
Copy link
 #3

Updated by Evgeny Novikov almost 7 years ago

  • Assignee set to Ilja Zakharov
  • Priority changed from High to Urgent

Ilja likes this feature so that he will implement it :)

Actions
Copy link
 #4

Updated by Evgeny Novikov over 6 years ago

  • Assignee deleted (Ilja Zakharov)
  • Priority changed from Urgent to High
Actions
Copy link

Also available in: Atom PDF