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?
- Subject: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- From: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
- Date: Tue, 13 Nov 2018 15:25:33 +0100
- In-reply-to: <1542040978.18747.1.camel@acc.umu.se>
- References: <1541967857.27070.3.camel@acc.umu.se> <13A1E8E0-90B9-48C9-A3B9-3CABDBFA29AE@cea.fr> <1542040978.18747.1.camel@acc.umu.se>
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>
- Follow-Ups:
- [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- From: tjoppen at acc.umu.se (Tomas Härdin)
- [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- References:
- [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- From: tjoppen at acc.umu.se (Tomas Härdin)
- [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- From: tjoppen at acc.umu.se (Tomas Härdin)
- [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- Prev by Date: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- Next by Date: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- Previous by thread: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- Next by thread: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- Index(es):