Предупреждение о шине "Оператор не имеет эффекта" из-за указателя функции

Question

Я пытаюсь проверить программу на C с помощью Splint (в строгом режиме). Я аннотировал исходный код семантическими комментариями, чтобы помочь Splint понять мою программу. Все было хорошо, но я просто не могу избавиться от предупреждения:

Оператор не имеет никакого эффекта (возможна необнаруженная модификация через вызов неограниченной функции my_function_pointer).

Оператор не имеет видимого эффекта - значения не изменяются. Это может изменить что-то через вызов неограниченной функции. (Используйте -noeffectuncon, чтобы запретить предупреждение)

Это вызвано вызовом функции через указатель на функцию. Я предпочитаю не использовать no-effect-uncon флаг, но лучше написать еще несколько аннотаций, чтобы исправить это. Так я украсил свой typedef с соответствующими @modifies пункт, но Сплинт, кажется, полностью игнорирует его. Проблема может быть уменьшена до:

#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);
}

Я прочитал руководство, но не так много информации относительно указателей функций и их семантических аннотаций, поэтому я не знаю, делаю ли я что-то не так или это какая-то ошибка (кстати, она еще не указана здесь: http://www.splint.org/bugs.html).

Кому-нибудь удалось успешно проверить такую ​​программу с помощью Splint в строгом режиме? Пожалуйста, помогите мне найти способ сделать Сплинта счастливым:)

Заранее спасибо.

Обновление № 1: splint-3.1.2 (версия для Windows) выдает предупреждение, в то время как splint-3.1.1 (версия для Linux x86) не жалуется на это.

Обновление № 2: Splint не заботится о том, является ли назначение и вызов коротким или длинным путем:

    /* 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);

Обновление № 3: я не заинтересован в запрещении предупреждения. Это легко:

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

То, что я ищу, это правильный способ выразить:

"этот указатель на функцию указывает на функцию, которая @modifies вещи, так что у него есть побочные эффекты "

Answer 1

Возможно, вы путаете сплинт, полагаясь на неявное преобразование из "имени функции" в "указатель на функцию" в вашем присваивании my_function_pointer, Вместо этого попробуйте следующее:

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

Теперь у вас есть явное преобразование, и шины не нужно угадывать.

Это всего лишь предположение, хотя. Я не проверял это.

Answer 2

Я не знаком с splint, но мне кажется, что он проверит вызовы функций, чтобы увидеть, производят ли они эффект, но он не выполняет анализ, чтобы увидеть, на что указывает указатель функции. Поэтому, насколько это возможно, указатель на функцию может быть чем угодно, а "все" включает в себя функции без эффекта, и поэтому вы продолжите получать это предупреждение при любом использовании указателя на функцию для вызова функции, если только вы этого не сделаете. что-то с возвращаемым значением. Тот факт, что в руководстве мало указателей на функции, может означать, что они не обрабатывают их должным образом.

Есть ли какая-то аннотация "доверять мне" для всего оператора, которую вы можете использовать с вызовами функций через указатели? Это не было бы идеально, но это позволило бы вам получить чистую пробежку.

Answer 3

Я считаю, что предупреждение верно. Вы приводите значение в качестве указателя, но ничего не делаете с ним.

Приведение просто делает значение видимым по-другому; это никак не меняет значение. В этом случае вы сказали компилятору рассматривать "foobar" как указатель, но поскольку вы ничего не делаете с этим представлением, оператор ничего не делает (не имеет никакого эффекта).