Frama-C works at the C semantic level, without knowledge about processor instruction-level details (expect for some extended assembly syntax, and a few details here and there). If you are talking about unspecified sequences of C statements, then Frama-C can warn about some situations, as mentioned in the user manual (https://www.frama-c.com/download/frama-c-user-manual.pdf):
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 this code, it is unclear in which order the elements of the right-hand side of the last assignment are evaluated. Indeed, the variable j can get any value as i and p are aliased.
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.
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.
In this code, it is unclear in which order the elements of the right-hand side of the last assignment are evaluated. Indeed, the variable j can get any value as i and p are aliased.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.