Проверка битов беззнакового целого числа с помощью леммы frama- c не работает - PullRequest
1 голос
/ 02 августа 2020

Используя frama- c Я работал над кодом, который использует битовое поле для представления набора. Скажите что-нибудь вроде

typedef uint32_t  myset_t;

#define EMPTY_SET  UINT32_C(0)
#define FULL_SET   UINT32_C(0x0ffffff)

, поэтому я использую только n младших битов 32-битного целого числа без знака. Затем я хотел реализовать предикат для проверки, установлен ли бит в "myset_t". Это не сработало так, как ожидалось (frama- c с alt-er go, способным доказывать что-то о таких наборах), и я мог сформулировать простую лемму, которая уже показывает мою проблему. В моей установке (frama- c 21.1 Scandium) он не может автоматически доказать следующую простую лемму:

    lemma test:
        \forall integer i;
        (0U <= i < 16U) ==> (0xFFFFU & (1U << (unsigned int)i)) != 0U;

Может ли кто-нибудь объяснить мне, что я делаю не так и где проблема есть? Или программы доказательства теорем не способны автоматически вычислить эти тривиальные арифметические c вещи (я имею в виду, что это всего лишь 16 случаев, их можно было бы просто перечислить)

1 Ответ

3 голосов
/ 03 августа 2020

Кажется, что автоматические c решатели не могут иметь дело со свойством, сгенерированным WP. Может быть, потому, что они не могут, или может быть из-за кодировки свойства.

Тем не менее, как вы сказали:

это всего лишь 16 случаев, их можно просто перечислить

И WP GUI предоставляет tacti c для создания такого доказательства. Если доказательство признано неудачным, дважды щелкните цель доказательства на панели «WP Goal» в нижней части окна. Затем выберите переменную для перечисления. Нажмите на тактич. c «Диапазон» и установите нижнее значение на 0, а верхнее на 15. Наконец, нажмите на зеленую стрелку рядом с названием тактильного обозначения c. WP сгенерирует 18 контрольных целей:

  • < 0 и > 15: тривиально, поскольку условие: 0 <= i <= 15
  • 0, 1, 2, 3 ..., 15: автоматически сбрасывается WP Qed

Затем вы можете щелкнуть значок сохранения, чтобы можно было легко воспроизвести доказательство.

введите описание изображения здесь

Если вы затем захотите воспроизвести доказательство из GUI, вы можете использовать стрелку, которая появляется на панели «WP Goal», когда существует скрипт проверки. Или вы можете напрямую попросить использовать существующие сценарии в командной строке, добавив tip в список проверяющих:

frama-c -wp -wp-prover alt-ergo,tip file.c

Обратите внимание, что сценарии WP сохраняются в сеансе WP, то есть по умолчанию в каталоге ./.frama-c/wp/scripts. Каталог сеанса WP можно настроить с помощью опции wp-session <directory>.

...