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] Using Frama-C for Analyzing Linux Kernel

  • Subject: [Frama-c-discuss] Using Frama-C for Analyzing Linux Kernel
  • From: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Wed, 7 Dec 2016 09:48:18 +0100
  • In-reply-to: <1978_1480579245_583FD8AC_1978_6672_1_d0a62b6d-02f4-f067-0e14-dbcf88a2d959@cea.fr>
  • References: <CAPpMX7TdN7-sQ35pv47jPymQ7UWfXaH2-WXJZ3v=y6+9bCJwgA@mail.gmail.com> <b3b87389-900e-850c-8692-54ac9f772ebb@cea.fr> <CAPpMX7QPXUP2HQHcGBi7_k1h5m4=oUFwumfV4V=3+qd_TdmvAg@mail.gmail.com> <6674f642-9082-973f-84b3-6e78e0fad592@cea.fr> <CAPpMX7RXa1WrhRWyQryo0J3HcOzLDuXxpnuQ1Yz4cvTqr7Q0bw@mail.gmail.com> <1978_1480579245_583FD8AC_1978_6672_1_d0a62b6d-02f4-f067-0e14-dbcf88a2d959@cea.fr>
There are some other issues related to parsing your preprocessed file. 
For instance, the following code is present:

static inline void sysfs_enable_ns(struct kernfs_node *kn)
{
   return kernfs_enable_ns(kn);
}

(It seems to have been added to the kernel by this patch: 
https://lkml.org/lkml/2014/2/7/739 )

However, section 6.8.6.4 of the C11 standard says the following:

6.8.6.4 The return statement
Constraints
A return statement with an expression shall not appear in a function 
whose return type is void. A return statement without an expression 
shall only appear in a function whose return type is void.

Frama-C does enforce this, as does Clang (GCC only emits a warning).

So there is either an issue during preprocessing, that led to a 
syntactically invalid program, or some special semantics of GCC that 
needs to be taken into account. It may be possible to simply remove the 
"return" (keeping the call to kernfs_enable_ns for its side-effect), but 
it may change the program semantics. Studying the code in more detail is 
necessary to understand if that is a reasonable choice.


Another problematic point is virt_spin_lock, which uses heavily 
__builtin_constant_p. Frama-C does have some issues with that GCC 
builtin, so it might be worth renaming it just to allow parsing to 
complete (when renamed, Frama-C will no longer treat it as a special GCC 
builtin; again, this may or may not affect the semantics of the program).

Once all these issues are dealt with, there still remain several parsing 
warnings. Dealing with them is not as urgent as dealing with the parsing 
errors, but still, it may require some work.

Overall, I'd say that the chance of obtaining interesting semantic 
analyses with a source code that is so complicated to parse (and uses so 
many GCC-isms, inline assembly, and non-standard constructions) is slim. 
Despite the several GCC extensions supported by Frama-C, the Linux 
kernel is still far from being a standards-compliant piece of code, 
hence hard to be used by semantic-based tools such as Frama-C. Being 
able to analyze such code is indeed part of the goals of the Frama-C 
platform, but currently we do not have a specific project or partnership 
to work on this directly. Parsing errors such as the one you reported 
will be fixed as time allows.

If your purpose is mostly to obtain an AST or to perform syntactic 
analyses on it (some of the tools you mentioned seem to be more 
syntactic-based than semantic-based), then it may be fine. But Frama-C's 
strengths lie mostly in semantic analyses. To proceed further, it may be 
better to abstract away the low-level code, e.g. by stubbing function 
calls and specifying their assigns clauses using ACSL, instead of trying 
to parse everything.


-- 
André Maroneze

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161207/62ba4f72/attachment.html>