Frama-C 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 MoreThis post has been co-written with Solid Sands; it is also available at the Solid Sands blog. Some time ago, the Frama-C team entered into a partner agreement with Solid Sands to make use of SuperTest, a very thorough test suite for C compilers and libraries. From basic syntactic tests...
Read MoreInteger overflows in C A previous post on this blog was a reminder that in C signed integer arithmetic overflow is undefined behavior. In contrast the behavior of overflows in conversions from integer type to signed integer type is implementation-defined. The C99 standard allows for an implementation-defined signal to be...
Read MoreQuiz time What does the program below do? #include <stdio.h> int main(){ struct { int t[4]; int u; } v; v.u = 3; v.t[4] = 4; printf(\v.u=%d" v.u); return 0; } Two answers are “it prints v.u=4” and “it prints v.u=3”: $ gcc t.c && ./a.out v.u=4 $ gcc -O2...
Read MoreThe title of this post, “Attack by Compiler”, has been at the back of my mind for several weeks. It started with a comment by jduck on a post earlier this year. The post's topic, the practical undefinedness of reading from uninitialized memory, and jduck's comment, awakened memories from a...
Read More