--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on May 2012 ---
Hello, 2012/5/13 dams <damien.balima at free.fr>: > [kernel] preprocessing with "gcc -C -E -I. ?-dD serveur_frama.c" > [jessie] Starting Jessie translation > [kernel] warning: No code for function accept, default assigns generated for > default behavior > :0:[jessie] failure: cannot handle this lvalue > [jessie] warning: Unsupported feature(s). > ? ? ? ? ? ? ? ? ?Jessie plugin can not be used on your code. > > Is there a fatal problem with these function, witch are standard C function > ? My code can compile with GCC, it works fine. As Jens said, you probably won't be able to prove much if you don't provide specifications for the functions you use. Some of stdlib functions have a partial specification in $FRAMAC_SHARE/libc, but this is very incomplete and can have bugs (some of them have already been reported and will be fixed in Oxygen, but there's likely more, as this is not the most tested part of Frama-C). That said, the warnings about the lack of specification for functions without code and the fact there's a feature that Jessie does not understand in your code are not necessarily related. If you happen to compile the Jessie plug-in from sources, the following patch will let Frama-C print the lval that is not handled by the Jessie plug-in. Otherwise, there's little that can be done without seeing the code under analysis. --- frama-c-plugin/norm.ml 2011-10-24 17:21:06.000000000 +0200 +++ frama-c-plugin/norm.ml.new 2012-05-14 09:54:53.038692786 +0200 @@ -1567,7 +1567,7 @@ match lv with | Var _, NoOffset -> lv | Var _, _ -> - unsupported "cannot handle this lvalue" + unsupported "cannot handle this lvalue: %a" !Ast_printer.d_lval lv; | Mem e, NoOffset -> begin match self#wrap_type_if_needed (typeOf e) with | Some newtyp -> Best regards, -- E tutto per oggi, a la prossima volta Virgile