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?

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