Предупреждение о шине не действует из-за указателя на функцию

Я пытаюсь проверить программу на 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: 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 содержит, поэтому она имеет побочные эффекты"


c warnings strict function-pointers splint
person Guillermo Calvo    schedule 20.04.2011    source источник

Ответы (3)


arrow_upward
1
arrow_downward

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

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

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

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

person Philip    schedule 20.04.2011
comment
Нет, это не работает. Я уже пробовал это, и Сплинт продолжает жаловаться. Я даже пытался разыменовать указатель на функцию (вот так: (*my_function_pointer)(foobar);), но потом получил другое предупреждение: Possible out-of-bounds read: *my_function_pointer. Спасибо, в любом случае :) - person Guillermo Calvo; 20.04.2011

arrow_upward
0
arrow_downward

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

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

person David Thornley    schedule 20.04.2011
comment
Я знаю, как запретить предупреждение: /*@-noeffectuncon@*/ my_function_pointer(foobar); /*@=noeffectuncon@*/ Но я хочу сделать это правильно. Дело в том, что Splints принимает: typedef void (*my_function_pointer_type)(int) /*@globals fileSystem@*/ /*@modifiers fileSystem@*/; Итак, ясно, что my_function_pointer_type — это указатель на функцию (потому что это @modifies что-то). Но позже Splint не принимает это во внимание и сообщает мне, что указатель на функцию не будет иметь никакого эффекта. - person Guillermo Calvo; 20.04.2011

arrow_upward
-1
arrow_downward

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

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

person Brian White    schedule 20.04.2011
comment
Вы можете использовать указатель функции, как если бы это было имя функции в вызове. my_function_pointer — это указатель на функцию, которая принимает целое число и возвращает void. - person David Thornley; 20.04.2011
comment
Я не привожу значение; Я вызываю функцию через указатель на функцию. В данном конкретном случае я вызываю функцию с foo по my_function_pointer. - person Guillermo Calvo; 20.04.2011
comment
Виноват. Я пропустил недостающий _type в конце. - person Brian White; 21.04.2011