Style test fails

the very first public test fails with following error:

splint found warnings.
stdout:
Command Line: Setting +ptrnegat redundant with current value
src/wordle.c: (in function generateDict)
src/wordle.c:100:21: Out storage selected1 not defined before retun
an out parameter or global is not defined before control is transferred. (use - mustdefine to inhibit warning)
src/wordle.c:100:21: Out storage selected2 not defined before return

stderr:
Splint 3.1.2a — May 25 2020

I dont seem to understand what this is supposed to tell me.
What is the line starting with " Command Line" supposed to mean?
and more important: how is checked if selected1 and selected2 are defined or not? i am picking them in src/wordle.c line 98 so I dont know why the test tells me I dont.
all other test are succesfull so far.( so i know the picking of words works due to test public.wordle.simple_load)

Because of the:

/*@out@*/

Essentially this signifies that the pointers prefixed by this are not assumed to hold meaningful information in them. So when you have something like this:

void g(char* p) {
    doSomething();
}

void f(/*@out@*/ char* p) {
    g(p);
}

there will be a warning. Basically the linter interprets this as you passing garbage to the function g.

The reason for this is that whoever implements g might not be the same person implementing f. So g might be written under the assumption that the input pointer contains meaningful information. Thus it could happen that the implementer of f interprets p as garbage to be overwritten with a call of g while the implementer of g interprets p as meaningful and operates on it. This sooner or later produces an error (which might be hard to catch). The annotation provided here is meant to stop this from happening.

The solution to this is to also annotate the argument p of g with /*@out@*/. (and of course g needs to actually fill p with information or call a function h to do so, which then in turn needs the same annotation on the corresponding argument)

hello,

I have now the same problem and that’s my error message
Screenshot 2022-06-02 152900
I’ve tried to use the same format from the header file wordle.h to implement the generateDict function but still it doesn’t work.
image
am I missing something?

It might be the case that you do not assign selected1 and selected2 (if it is not NULL).

It might also be the case that split does not recognize the assignment due to complex control flow.
In the second case, you could ignore the warning and tell splint to do so using -mustdefine in testregistry.py:

2 Likes