Extended High-Level C-Compatible Memory Model with Limited Low-Level Pointer Cast Support for Jessie Intermediate Language.


Extended High-Level C-Compatible Memory Model with Limited Low-Level Pointer Cast Support for Jessie Intermediate Language.

Авторы

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

Аннотация

The paper presents an intermediate language which is intended to serve as a target analyzable language for verification of real-world production GNU C programs (Linux kernel modules). The language represents an extension of the existing intermediate language used by the JESSIE plugin for the FRAMA-C static analysis framework. It is compatible with the C semantics of arrays, initially supports hierarchical (prefix) pointer casts and discriminated unions, and extended with limited support for low-level pointer casts. The approaches to translation of the original C code into the intermediate language and translation of the intermediate language into the input language of the Why3 deductive verification platform are explained by examples. The examples illustrate the expressive power of the extended intermediate language and efficiency of the resulting axiomatic representation.

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

Ключевые слова

deductive verification, memory model, C programming language semantics, discriminated unions, hierarchical pointer casts, low-level pointer casts

Издание

Материалы Международной научно-практической конференции: Tools & Methods of Program Analysis, TMPA-2014, место издания Кострома: КГТУ, с. 36-45

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

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

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