High-Level Memory Model with Low-Level Pointer Cast Support for Jessie Intermediate Language.
High-Level Memory Model with Low-Level Pointer Cast Support for Jessie Intermediate Language.
Authors
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.
Edition
Programming and Computer Software. — 2015. — Vol. 41, no. 4. — P. 197–207.
DOI: 10.1134/S0361768815040040
Research Group
All publications during 2015
All publications