Splint warning "Statement has no effect" due to function pointer

I'm trying to chec开发者_JAVA技巧k a C program with Splint (in strict mode). I annotated the source code with semantic comments to help Splint understand my program. Everything was fine, but I just can't get rid of a warning:

Statement has no effect (possible undected modification through call to unconstrained function my_function_pointer).

Statement has no visible effect --- no values are modified. It may modify something through a call to an unconstrained function. (Use -noeffectuncon to inhibit warning)

This is caused by a function call through a function pointer. I prefer not to use the no-effect-uncon flag, but rather write some more annotations to fix it up. So I decorated my typedef with the appropriate @modifies clause, but Splint seems to be completely ignoring it. The problem can be reduced to:

#include <stdio.h>

static void foo(int foobar)
/*@globals fileSystem@*/
/*@modifies fileSystem@*/
{
    printf("foo: %d\n", foobar);
}

typedef void (*my_function_pointer_type)(int)
/*@globals fileSystem@*/
/*@modifies fileSystem@*/;

int main(/*@unused@*/ int argc, /*@unused@*/ char * argv[])
/*@globals fileSystem@*/
/*@modifies fileSystem@*/
{
    my_function_pointer_type my_function_pointer = foo;
    int foobar = 123;

    printf("main: %d\n", foobar);

    /* No warning */
    /* foo(foobar); */

    /* Warning: Statement has no effect */
    my_function_pointer(foobar);

    return(EXIT_SUCCESS);
}

I've read the manual, but there's not much information regarding function pointers and their semantic annotations, so I don't know whether I'm doing something wrong or this is some kind of bug (by the way, it's not already listed here: http://www.splint.org/bugs.html).

Has anyone managed to successfully check a program like this with Splint in strict mode? Please help me find the way to make Splint happy :)

Thanks in advance.

Update #1: splint-3.1.2 (windows version) yields the warning, while splint-3.1.1 (Linux x86 version) does not complain about it.

Update #2: Splint doesn't care whether the assignment and the call are short or long way:

    /* assignment (short way) */
    my_function_pointer_type my_function_pointer = foo;

    /* assignment (long way) */
    my_function_pointer_type my_function_pointer = &foo;

    ...

    /* call (short way) */
    my_function_pointer(foobar);

    /* call (long way) */
    (*my_function_pointer)(foobar);

Update #3: I'm not interested in inhibiting the warning. That's easy:

/*@-noeffectuncon@*/
my_function_pointer(foobar);
/*@=noeffectuncon@*/

What I'm looking for is the right way to express:

"this function pointer points to a function which @modifies stuff, so it does have side-effects"

Maybe you are confusing splint by relying on the implicit conversion from "function name" to "pointer to function" in your assignment of my_function_pointer. Instead, try the following:

// notice the &-character in front of foo
my_function_pointer_type my_function_pointer = &foo;

Now you have an explicit conversion and splint doesn't need to guess.

This is just speculation, though. I haven't tested it.

I'm not familiar with splint, but it looks to me that it will check function calls to see if they produce an effect, but it doesn't do analysis to see what a function pointer points to. Therefore, as far as it's concerned, a function pointer could be anything, and "anything" includes functions with no effect, and so you'll continue to get that warning on any use of a function pointer to call a function, unless you so something with the return value. The fact that there's not much on function pointers in the manual may mean they don't handle them properly.

Is there some sort of "trust me" annotation for an entire statement that you can use with function calls through pointers? It wouldn't be ideal, but it would allow you to get a clean run.

I believe the warning is correct. You're casting a value as a pointer but doing nothing with it.

A cast merely makes the value visible in a different manner; it doesn't change the value in any way. In this case you've told the compiler to view "foobar" as a pointer but since you're not doing anything with that view, the statement isn't doing anything (has no effect).