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

Инструменты 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, либо вручную собрав его из исходного кода, доступного в наших публичных репозиториях. Все изменения публикуются под теми же лицензиями, что и оригинальный код соответствующих инструментов.