Project

General

Profile

Actions

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 open0 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

Also available in: Atom PDF