Project

General

Profile

Actions
Copy link

Feature #7942

open

Use models of atomic_dec_and_test and atomic_set for all rule specifications

Added by Vadim Mutilin almost 8 years ago. Updated almost 8 years ago.

Status:
New
Priority:
High
Assignee:
-
Category:
Requirement specifications
Target version:
-
Start date:
02/01/2017
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

See http://ldvstore:8998/reports/unsafe/75886/

Functions atomic_dec_and_test and atomic_set are not modeled while some of atomic* functions use inline assembler unsupported by verifiers, therefore free is not called in unix_release_addr. Note, that corresponding models already invoked but just by rule specification linux:usb:dev.

Actions
Copy link

Also available in: Atom PDF