Failing splint due to /*@out@*/ annotation in generateDict

Hello,

I essentially have the following problem: My generateDict function works perfectly fine but runs into a linting issue.

src/wordle.c: (in function generateDict)
src/wordle.c:31:17: Out storage selected2 not defined before return
  An out parameter or global is not defined before control is transferred. (Use
  -mustdefine to inhibit warning)

My function body looks something like this:

create dict from file;
do {
    pick selected1 from dict;
    if (quantum mode) {
        find all words that do not share something with selected1;
        if (there are such words) {
              pick selected2 from them;
        }
} while (true);
return the created dict;

The way I see it there are three scenarios (assuming the dictionary is not empty):

  1. I am not in quantum mode, in which case selected2 is NULL.
  2. I am in quantum mode and I find a suitable second word
  3. I am in quantum mode and there is no suitable second word for any first word choice.

So either word2 is Null (case 1), overwritten by sensible input (case 2) or the program diverges and the return statement is never even reached (case 3).

Obviously the situation that the linter complains about never happens. How can I force the linter to shut up about it?

1 Like

Maybe try putting:

// show linter that if selected2 is not NULL, it will be overwritten 
if (selected2) {
  selected2[0] = '\0'
}

at the start of your function (and if the style checker is annoying regarding if(selected2) use if (selected2 != NULL).

Hope this will fix it!
Tim

2 Likes

Thanks for the reply, I tried something like this now by inserting:

if (selected2) {
    for (int i = 0; i < k + 1; i++) { // note that I overwrite all k + 1 entries
        selected2[i] = 'a';
    }
}

but the warning persists. (it also doesn’t help if I add “!= NULL” into the condition)

Is there any way to convince the linter that something has been written? If it helps, the picking of a word from the dictionary is done via a function which in its signature has:

/*@out@*/ char* selected

so that it knows that the selected I pass may be garbage.

We have also seen another case where splint does not recognize the assignment and received a convincing argument against this warning.
Therefore, we decided to add -mustdefine to the options passed to splint on the test server (line 16 in test_registry.py).
This way, splint will no longer warn you if you do not assign a variable marked as output (or if it does not recognize the assignment).
You can safely add this option and be sure that the server has it also enabled if you are sure that you assign selected2 correctly.

2 Likes