High-level memory model with low-level pointer cast support for Jessien intermediate language

摘要

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 reaso