[KsassPeuk]

> Frama-C doesn't need to know anything about the target arch.

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.

[dandotway]

For my use cases thus far, the usual C portability pitfalls haven't applied: whether char is signed or unsigned, the range of 'int', little vs. big endian, etc.