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

Authors

M.U. Mandrykin, A.V. Khoroshilov

Abstract

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.

Full text of the paper in pdf

Keywords

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

Edition

Proceedings of Tools & Methods of Program Analysis, TMPA-2014, KSTU, Kostroma, Russia, pp. 36-45.

Research Group

Software Engineering

All publications during 2014

All publications