Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?



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>