--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on November 2018 ---
Indeed, the idea is to use something like: frama-c -wp -report-unclassified-unknown ERROR <file.c> -then -report-classify Which will return a non-zero code in case there are properties with /Unknown/ status (-report-exit is enabled by default). However, as you noticed, -report-exit is not available before Frama-C 17 (Chlorine), so in Silicon you won't have it. Ideally, installing opam then Frama-C via opam should work on Debian, giving you access to the latest Frama-C release; although it is indeed more complex than installing the Debian frama-c package. However, if there are specific installation issues with opam on Debian, it might be worth mentioning them, in case we can find a workaround. Best regards, On 12/11/2018 17:42, Tomas Härdin wrote: > So if I understand correctly one tells the report plugin to classify > unproved as error, and give it the -report-exit option (which is > default) and it'll return non-zero in those cases. > > It seems Silicon does have the report plugin (frama-c -report-h works), > but -report-exit is indeed not available. Or maybe it already fails on > error - I haven't gotten around to testing yet > > /Tomas -- André Maroneze Researcher/Engineer CEA/List Software Reliability and Security Laboratory -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181113/4346ea46/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181113/4346ea46/attachment.bin>