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] about checking xen by frama-c

  • Subject: [Frama-c-discuss] about checking xen by frama-c
  • From: gjk.liu at gmail.com (Liu Jian)
  • Date: Mon, 16 Aug 2010 20:56:44 +0800
Dear All,
     I am interested in the work about "static analysis of the Xen kernel
using Frama-C". But there is no more details about the following key
porints.

1) how to write analysis/test driver. You know, when testing a hypercall or
syscall, a testing driver is needed to initiating environment parameters,
such as your dealing with "_start_xen" by a man function (P 545~546).

2) how to deal with in-lined assembly code. As you papers says, "... we
manually transformed this code into equivalence but simpler C code.." (P645)

I want to know methods to deal with the above questions. Moreover, I think
your XEN 3.0.1 source code tarbar will be helpful to me. If
possible, anyone can send a copy of it to me?

  cheers,

  LIU Jian
----
email to: gjk.liu at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100816/5cab39c5/attachment.htm>