Нечетное поведение при проверке шин

Question

Есть ли тут эксперты по шинам?? Я пытаюсь использовать splint для статического анализа большого проекта, который у меня есть в C. Я вижу избыточное количество ошибок проверки границ, которые явно не являются ошибками границ. Я написал небольшую тестовую программу, чтобы попытаться изолировать проблему, и заметил несколько действительно странных предупреждений, когда запускал шину по коду. У меня есть 3 разных примера. Вот первое:

int arr[3];

int main(void)
{
    int i;
    int var;

    arr[3] = 0; // (1) warning with +bounds, no warning with +likely-bounds

    return 0;
}

arr[3] назначение генерирует предупреждение при использовании +bounds как и следовало ожидать, но ничего не делает, когда я использую +likely-bounds, Что значит +likely-bounds Даже сделать? Кажется, не работает. Второй пример:

int arr[3];

int main(void)
{
    int i;
    int var;

    for (i = 0; i < 3; i++)
        var = arr[i]; // (2) warning, even though I'm within the bounds.

    return 0;
}

В этом примере splint жалуется, что я читаю за пределами массива ("чтение памяти ссылается на память за пределами выделенного хранилища") для var = arr[i]хотя я, очевидно, нет. Это должно быть предупреждением, потому что значения в массиве не инициализируются, но это не предупреждение, которое я получаю. Инициализация последнего значения в массиве очистит ошибку (но инициализация первого или второго не даст). Я делаю что-то неправильно? В третьем примере:

int arr[3];

int main(void)
{
    int i;
    int var;

    arr[3] = 0; // warning

    for (i = 0; i < 4; i++)
        var = arr[i]; // (3) no warning because arr[3] = 0 statement.

    return 0;
}

Предупреждение генерируется для arr[3] = 0, но нет var = arr[i]даже если очевидно, что цикл выходит за границы массива. Похоже, что запись в конец массива расширяет представление о том, как выглядит массив. Как это возможно?

Короче мои вопросы:

1. Что делает флаг вероятных границ?
2. Есть ли способ, которым я могу заставить шину дать мне законные ошибки, связанные с выходом за пределы?
3. Можно ли сделать так, чтобы шины не увеличивали размер массивов, к которым осуществляется доступ за их пределами? В данный момент шина сообщает о более чем 750 предупреждениях, и у меня нет времени проверять каждое предупреждение одно за другим.

Answer 1

Вначале: я не знаю "шины", но я хорошо знаю методы, благодаря интенсивному использованию PC Lint и обсуждению нескольких вопросов с его создателями.

Это говорит:

• В вашем первом примере arr[3] помечен только +bounds Вероятно, потому что элемент один за последним является особым случаем: ему разрешено создавать и использовать указатель на элемент, который следует за последним, но не разрешается разыменовывать такой указатель. Следовательно, в средствах проверки синтаксиса (также QA-C) довольно часто случается, что такие предупреждения менее серьезны для N+1. Ты пробовал arr[4]? Я думаю, +likely_bounds будет достаточно для этого.
• Второй пример, вероятно, вызван несколько запутанной "шиной". Я видел подобные ошибки в ранних версиях PC Lint и QA-C, поскольку "отслеживание значений" далеко не просто. Однако я не могу сказать, почему сплит жалуется.
• Ваш третий пример, "splint" правильно жалуется на инициализацию arr[3], но для целей отслеживания стоимости он тогда принял arr[3] быть действительным и воздерживаться от жалоб на петлю. Я полагаю, вы могли бы инициализировать arr[100] и пусть цикл работает до 100 без жалоб!