Thank you for the write up. I'll be reading up on this more.
Do you know if it models the target arch, too? Like, can it account for different architectures having different instruction reordering rules?
Do you know if it models the target arch, too? Like, can it account for different architectures having different instruction reordering rules?
CompCert, the formally verified C compiler, is a separate thing from Frama-C, but currently supports x86, ARM, RISC-V, and PowerPC. (CompCert is actually mostly programmed in OCaml and the Coq/Gallina proof assistant.) CompCert guarantees that a correct ISO C program (no undefined or implementation defined behavior) is translated into an assembler program with the same semantics, i.e. an assembler program that computes the same results as the C source program. So CompCert for each supported architecture needs a formal semantics for any CPU instructions it generates. CompCert is an optimizing compiler and the optimizer accounts for the delay between when an instruction is issued and when the result is ready, accounts for pipelining and all that if that is what you are asking.
But to write verified C programs you don't need to worry about instruction re-ordering happening lower down changing the meaning of your program and all that. That's a deeper layer of the onion, and, as Bjarne Stroustrup said, each time you peel a layer of the onion you cry more.
In fact, it needs some knowledge, but this knowledge can be configured for the project under analysis. This is the reason why the Frama-C kernel provides the `-machdep` option ;) .
Then depending on your code, you might need to add particular knowledge according to your target platform. For example validity of some hardware memory location, etc.
option -unspecified-access may be used to check when the evaluation of an expression depends on the order in which its sub-expressions are evaluated. For instance, this occurs with the following piece of code.
int i, j, *p;
i = 1;
p = &i;
j = i++ + (*p)++;
In some cases, knowing the architecture is essential to get information such as the width of integer types. Ideally, one would like a completely system-independent, portable analysis, but this is extremely hard in C. For instance, the ISO C11 standard, in section 5.2.4.1 Translation limits, states that The implementation shall be able to translate and execute at least one program that contains at least one instance of every one of the following limits [...] 4095 characters in a string literal (after concatenation), 65535 bytes in an object, [...]. It also states that INT_MAX may be, for instance, as low as 32767. So, for a truly portable analysis, one would have to warn whenever any of these limits are reached, leading to an analysis useless except for some toy examples.