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