Предупреждение о шине «Оператор не имеет никакого эффекта» из-за указателя функции - PullRequest
Новая
       48

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

3 голосов
/ 20 апреля 2011

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

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

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

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

#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: Шине не важно, будут ли присвоение и вызов короткими или длинными способом: 

    /* 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 содержит, так что имеет побочные эффекты"

Ответы [ 3 ]

1 голос
/ 20 апреля 2011

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

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

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

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

0 голосов
/ 20 апреля 2011

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

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

0 голосов
/ 20 апреля 2011

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

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

...