Высокоуровневая модель памяти промежуточного языка Jessie с поддержкой произвольного приведения типов указателей.

Авторы

М. У. Мандрыкин, А. В. Хорошилов.

Аннотация

В статье представлен промежуточный язык, предназначенный для использования в качестве целевого анализируемого языка при верификации промышленного кода на языке GNU C (в частности, модулей ядра Linux). Язык представляет собой расширение существующего промежуточного языка, используемого подключаемым модулем Jessie в системе статического анализа Frama-C. Он имеет семантику, совместимую с семантикой языка Си (в частности, для массивов), изначально поддерживает различаемые объединения и префиксные (иерархические) приведения типов указателей на структуры, и расширен ограниченной поддержкой низкоуровневого приведения типов указателей. В статье описаны подходы к трансляции исходного Си-кода в промежуточный язык, а также трансляции промежуточного языка во входной язык платформы дедуктивной верификации Why3.

Полный текст статьи в формате pdf

Издание

Программирование том 41, №4, 2015, с. 23-39.

Научная группа

Технологии программирования

Все публикации за 2015 год

Все публикации