--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [jessie-plugin] cannot be used on your code



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