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