30.11.2016: Опубликована новая версия Astraver Toolset 1.1

user warning: Got error 28 from storage engine query: SELECT t.*,v.weight AS v_weight_unused FROM term_node r INNER JOIN term_data t ON r.tid = t.tid INNER JOIN vocabulary v ON t.vid = v.vid WHERE r.vid = 278 ORDER BY v.weight, t.weight, t.name in /opt/drupal-6.33/modules/taxonomy/taxonomy.module on line 640.

Инструменты Astraver Toolset 1.1 включают в себя следующие улучшения:

Поддержка языка Си

  • Поддержка адресной арифметики с указателями на вложенные структуры, например, макроса `container_of', широкораспространённого в ядре ОС Linux. В частности, теперь появилась возможность доказать корректность указателя на внешнюю структуру, полученного путём вычитания смещения внутренней структуры из указателя на неё.

Новый подход к целочисленным арифметическим операциям в ACSL

  • Прагма `JessieIntegerModel' для переключения между различными моделями целых чисел (`math', `strict' и `modulo') больше не поддерживается. Новая модель целых чисел объединяет `strict' и `modulo', но с гранулярностью на уровне отдельных операторов.
  • В язык ACSL добавлены новые операторы машинной арифметики: +%, -%, *%, /% и (integral_type %) (кастирование), которые представляют аналоги соответствующих операторов без %, но по модулю 2n, где n - размерность соответствующего машинного типа. Эти операции, так же как и все побитовые операторы (&, |, ~, ^, >>, <<) кодируются в теории битовых векторов фиксированного размера.
  • Модифицированный маркер начала блока ACSL кода /*@%*/ означает, чтобы все арифметические операторы в этом блоке рассматриваются как машинные и также кодируются в теории битовых векторов фиксированного размера.

Изменения в Jessie2

  • С целью более эффективной работы решателей реализовано разделение теорий Jessie. Теперь все для каждой аксиоматике, каждой глобальной леммы, каждого машинного целочисленного типа и других Jessie определений используется отдельная теория. Программный модуль также разделяется на несколько: по одному на каждую верифицируемую функцию. Зависимости между теориями и модулями вычисляются автоматически, с тем чтобы импортировать только необходимые определения.
  • Инварианты цикла разделяются по оператору `&&', чтобы уже доказанные коньюнкты инварианта автоматически использовались при доказательстве последующих коньюнктов.

Улучшения в Why3 IDE

  • Добавлен поиск выбранного текста в представлении задач (task view).
  • Добавлен новая галочка в меню View, позволяющая скрыть в дереве целей все пустые теории (теории, не содержащие целей для доказательства).

Описание других улучшений в AstraVer Toolset относительно оригинальных инструментов 'Frama-C + Jessie + Why3 IDE' представлено в анонсе предыдущей версии.

Текущий выпуск системы верификации Astraver Toolset можно установить либо через OPAM, либо вручную собрав его из исходного кода, доступного в наших публичных репозиториях. Все изменения публикуются под теми же лицензиями, что и оригинальный код соответствующих инструментов.