Ivannikov Institute for System Programming of the RAS

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


M. U. Mandrykin, A. V. Khoroshilov


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


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