Feature #333
openRestrict abstraction to the actual values used
0%
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...
Updated by Evgeny Novikov about 13 years ago
May it be one of the fundamental ideas concerned with static analysis improvement?
Updated by Pavel Shved about 13 years ago
- Status changed from Open to New
As of today, I doubt that it would be implemented at all.
The whole point of abstract interpretation is to separate necessary and unnecessary information from each other.
May-alias analysis makes this even less useful: we never know if a variable will be used as an alias, and, perhaps, even those variables which are not in program, may appear useful.
I guess, this feature will eventually be rejected.
Updated by Pavel Shved over 12 years ago
- Category deleted (
BLAST) - Project changed from Linux Driver Verification to BLAST