Feature #10924
Updated by Evgeny Novikov over 2 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 (this will not the case after updating CIF - https://forge.ispras.ru/issues/10927). 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. We Hopefully, we can try to consider those "-Werror" options that are used for building the Linux kernel or any other projects since these options should not result in any extra errors for headers while they can do so for models. Hopefully, "Clade 3.4.8":https://github.com/17451k/clade/releases/tag/v3.4.8 does not filter out options enabling error messages about implicit function declarations. So, we need to update it and fix appropriate errors if so.