Project

General

Profile

Feature #9221

Add a rule for svcomp tasks generation

Added by Pavel Andrianov about 2 years ago. Updated 8 months ago.

Status:
Open
Priority:
High
Category:
Rule specifications
Target version:
-
Start date:
08/14/2018
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

I implemented a rule, which replace spinlocks and mutexes with pthread_mutexes. The rule is used for generation sv-comp tasks for concurrency. Tests are also available, but they are based on tests for sync:race. The new rule is implemented in the branch svcomp-rule. It is convenient to have it in master, but the issue is not urgent.

History

#1

Updated by Evgeny Novikov about 2 years ago

  • Target version set to 2.0
  • Priority changed from Normal to Urgent

As it is implemented already, it is not so hard to test it and to merge it to master.

#2

Updated by Evgeny Novikov almost 2 years ago

  • Target version changed from 2.0 to 3.0
  • Status changed from Resolved to Open

I forgot about this, but now it should be definitely rebased on top of the latest master as there are very many changes there.

#3

Updated by Evgeny Novikov 8 months ago

  • Target version deleted (3.0)
  • Priority changed from Urgent to High

It seems that we will not have this in Klever 3.0.

Also available in: Atom PDF