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



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