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



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