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 about 7 years ago. Updated about 7 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
 #1

Updated by Alexey Khoroshilov about 7 years ago

Model of these functions should be available to all rules.

Actions
Copy link
 #2

Updated by Evgeny Novikov about 7 years ago

  • Tracker changed from Bug to Feature
  • Subject changed from linux:alloc: the models of atomic_dec_and_test and atomic_set are needed for net/unix/unix.ko to Use models of atomic_dec_and_test and atomic_set for all rule specifications
  • Description updated (diff)
Actions
Copy link

Also available in: Atom PDF