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] [jessie-plugin] cannot be used on your code

  • Subject: [Frama-c-discuss] [jessie-plugin] cannot be used on your code
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Mon, 14 May 2012 09:58:39 +0200
  • In-reply-to: <4FAFF570.5030309@free.fr>
  • References: <4FAFF570.5030309@free.fr>
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