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?

I found a workaround: tee'ing frama-c output to file, then some grep
magic for what output I don't want to see:

%.o: %.c $(INC)
	frama-c -wp -wp-rte -wp-init-const $(shell grep //% $< | sed -e
's|//%||') $< | tee $<.log
	echo
	# Don't stop on things Frama-C gives up on
	#! grep Unknown $<.log
	! (grep warning $<.log | grep -v comprehension | grep -v
initialization | grep -v calloc | grep -v warnings)
	# malloc() and free() doesn't work right -> Degenerated
	! (grep Timeout $<.log | grep -v Degenerated)
	! grep error $<.log
	gcc $(CFLAGS) -c -o $@ $<

I'm ignoring things Silicon gives up on due to unimplemented features.
I use //% to give file-specific options for frama-c, typically timeout
like so: //%-wp-timeout 60

/Tomas

tis 2018-11-13 klockan 15:25 +0100 skrev Andre Maroneze:
> Indeed, the idea is to use something like:
> 
> frama-c -wp -report-unclassified-unknown ERROR <file.c> -then 
> -report-classify
> 
> Which will return a non-zero code in case there are properties with 
> /Unknown/ status (-report-exit is enabled by default).
> 
> However, as you noticed, -report-exit is not available before Frama-C 
> 17 
> (Chlorine), so in Silicon you won't have it.
> 
> 
> Ideally, installing opam then Frama-C via opam should work on
> Debian, 
> giving you access to the latest Frama-C release; although it is
> indeed 
> more complex than installing the Debian frama-c package.
> 
> However, if there are specific installation issues with opam on
> Debian, 
> it might be worth mentioning them, in case we can find a workaround.
> 
> 
> Best regards,
> 
> 
> On 12/11/2018 17:42, Tomas Härdin wrote:
> > 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss