Blog

Back

Tag Archives: machdep

Pointer alignment verification
Allan Blanchard (reviewed by Hugo Thievenaz, André Maroneze and Virgile Prevosto) on 2 March 2026

This blog post sums up what is the alignment constraint, its meaning for (common) hardware, how it has been derived at the C level and how Frama-C has been modified in version 32.0 (Germanium) to support the verification of this constraint and to support the keywords related to memory alignment....

Read More

New machdep mechanism in Frama-C
André Maroneze on 29 January 2024

A machdep (for machine-dependent) in Frama-C is a set of architecture-specific configurations, which include: integer sizes, predefined macros, compiler type, standard library constants, etc. They are essential when analyzing embedded, non-portable code. Thanks to some C11 features, the machdep generation mechanism has been revised in Frama-C, allowing users to more...

Read More