I'm trying to check 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"
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).