Feature #10924
Updated by Evgeny Novikov about 3 years ago
Sometimes users develops slightly inaccurate/invalid models. For instance, they forget to add declarations for functions invoked in their models, e.g. by including appropriate headers. This can result in weird failures and trash during running Frama-C (CIL) or even later at verification. I suggest to fail earlier since GCC is capable to report a lot of different issues in sources.
Unfortunately, we can not turn on something like "-Wall -Werror" since models can include project headers and GCC may report errors for them while we would not like to fix them. Hopefully, we can try to consider those "-Werror" options that are used for building the Linux kernel since these options should not result in any extra errors for headers while they can do so for models.