Project

General

Profile

Actions
Copy link

Feature #11014

closed

Avoid infinite loops in environment models

Added by Evgeny Novikov about 3 years ago. Updated over 2 years ago.

Status:
Closed
Priority:
High
Assignee:
Evgeny Novikov
Category:
Environment models
Target version:
3.5
Start date:
11/19/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

After Ilja has supported the way to configure the number of loop iterations for environment processes (#10929), we have an ability to simplify environment models.

Related issues 1 (0 open — 1 closed)

Related to Klever - Feature #10929: Do not invoke callbacks infinitely and allow to configure the number of iterationsClosedIlja Zakharov09/09/2021

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov about 3 years ago

  • Related to Feature #10929: Do not invoke callbacks infinitely and allow to configure the number of iterations added
Actions
Copy link
 #2

Updated by Evgeny Novikov over 2 years ago

  • Status changed from New to Closed

I implemented this in branch avoid-infinite-loops-in-env-models. This branch passed almost all test cases. There were only 2 regressions, one was positive (timeout -> false alarm) and one was negative (safe -> timeout).

Much more important that it helps CPAchecker SMG very considerably at verification of a bunch of drivers. For instance, when verifying 2141 drivers, it could prove 124 more safes (most of them were timeouts earlier). Moreover, several new unsafes were found while many false alarms due to some bugs in CPAchecker SMG have gone.

I merged the branch to master in ad04f7d01.

Actions
Copy link

Also available in: Atom PDF