--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on November 2018 ---
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 mån 2018-11-12 klockan 11:10 +0100 skrev Loïc Correnson: > Hi, > Yes it is indeed possible, provided you use facilities offered by the > Report plug-in. > See Frama-C user manual § 10.3 on frama-c.com ; however, you'll have > to upgrade from Silicon, indeed. > L. > > > Le 11 nov. 2018 à 21:24, Tomas Härdin <tjoppen at acc.umu.se> a écrit > > : > > > > Hi > > > > Is it possible to make frama-c return a non-zero exit code if it > > fails > > to prove every goal? This would be very useful in a build system. > > Maybe > > it's already possible in recent versions? I'm stuck on Silicon > > currently (due to Debian). Searching the manual didn't yield much > > > > The reason is of course the sometimes huge proving times, in my > > case > > when dealing with string concatenation. I get the feeling that > > putting > > each function into its own compilation unit may save some headache. > > But > > of course, this is only useful if it's possible to have a sane > > build > > system! > > > > /Tomas > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss