Project

General

Profile

Actions
Copy link

Feature #333

open

Restrict abstraction to the actual values used

Added by Pavel Shved over 13 years ago. Updated over 12 years ago.

Status:
New
Priority:
Low
Assignee:
Pavel Shved
Category:
-
Target version:
-
Start date:
08/03/2010
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

The thing is that sometimes we can understand what code is of use and what is of no use without running solvers. In usual CEGAR workflow only counterexample analysis procedure can report this, but we could implement a heuristic.

For example, if variable is uninitialized, but it's not used, its initializer is unnecessary. This may aid speed of analysis (if bug #331 is fixed).

Another example, if address of a local variable is taken into account, then its inequality with the other pointers may be necessary (if we implemented it, see bug #327). Otherwise, it's definitely not, and we could detect it!

I think that when trace is analyzed, we can determine that certain variable initializers, or certain address information is necessary. Of course, we use it during trace analysis, but we also should rewrite abstraction, so that its refinement and further processing would use the information enforced.

That's still just an idea...

Actions
Copy link

Also available in: Atom PDF