Re:Why the C Language Will Never Stop You from Making Mistakes
by KsassPeuk on Monday January 03, 2022 @03:52AM
(#29778695)
> 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.
Re:Why the C Language Will Never Stop You from Making Mistakes
by dandotway on Monday January 03, 2022 @07:12PM
(#29789027)
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.
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.