• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

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

Programming and Computer Software. 2015. Vol. 41. No. 4. P. 197-207.
Khoroshilov A. V., Мандрыкин М. У.

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.