--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on November 2018 ---
[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>