Linux Driver Verification

One of the related issue is #533 (well known jedec_probe problem).

Eugene Novikov wrote:

First of all I want to notice that few such drivers were discovered on investigating #1166 issue (i.e. they are passed to aspectator that reports that it cannot process error_mark tree node). But they also are described in more general terms, Compile error. Some typical error messages are so:
[...]
For further investigation and fixing you can follow this temporary link or perform task with some aspectator model (like 43_1a) on all kernel drivers or upload attached archive.

The issue described here looks like the one which already being fixed in master branch after FAIL of NIGHT tests.
So the link to the run results is obsolete, because the branch model-43_1a was merged with the buggy master and contained the already fixed DEG errors. There is no sense to analyze it. Instead, the run on the newly merged master should be analysed. The pax should already have been generated on cluster (id=224 as far as I remember).

First of all it sounds strange that the issue is fixed since there at least two related bugs that weren't fixed.
Also (may be I'm mistaking) I have launched with non buggy master merged into model-43_1a branch and obtain almost the same problems.

Eugene Novikov wrote:

First of all it sounds strange that the issue is fixed since there at least two related bugs that weren't fixed.

Two bugs attached here are not related to the problem described in the bug (redeclaration and storage size). Also they are not related to the header of the bug, because it contains word OFTEN, but the two attached bugs affect JUST TWO drivers. I suggest to remove dependency of that bugs, bacause they really don't have HIGH priority like this bug (looking to the header only).

Also (may be I'm mistaking) I have launched with non buggy master merged into model-43_1a branch and obtain almost the same problems.

That should be checked, because nobody wants to waste time analysing incorrect runs.

To make it clear I have launched "fixed" model-43_1a model (commit 46733e0).
By the way this bug is a set of all DEG bugs. Some of them are small ones (as blockers). But other bugs should be found out indeed...

Eugene Novikov wrote:

To make it clear I have launched "fixed" model-43_1a model (commit 46733e0).

Thats good.

By the way this bug is a set of all DEG bugs. Some of them are small ones (as blockers). But other bugs should be found out indeed...

I think that fixing all the bugs in DEG including very small ones is not so HIGH priority. (Remembering its regexp nature). The HIGH priority is to find and fix major bugs, not the small ones.