--- layout: fc_discuss_archives title: Message 8 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?



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