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?

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