Ivannikov Institute for System Programming of the RAS


High-Level Memory Model with Low-Level Pointer Cast Support for Jessie Intermediate Language.

Authors

M. U. Mandrykin, A. V. Khoroshilov

Abstract

The paper presents a target analyzable language used 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. Compared to the original Jessie, the extension is fully compatible with the C semantics of arrays, initially supports discriminated unions and prefix (hierarchical) structure pointer casts and provides a limited, but reasonable support for low-level pointer casts (reinterpretations of the underlying bytes of memory).
The paper describes the approaches to translation of the original C code into the analyzable intermediate language and of the intermediate language into Why3ML i.e. the input language of the Why3 deductive verification platform.

Full text of the paper in pdf

Edition

Programming and Computer Software. — 2015. — Vol. 41, no. 4. — P. 197–207.

DOI: 10.1134/S0361768815040040

Research Group

Software Engineering

All publications during 2015 All publications