--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on November 2018 ---
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