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] How to know whether a function is defined in ghost code or not

  • Subject: [Frama-c-discuss] How to know whether a function is defined in ghost code or not
  • From: haihaoshen at gmail.com (haihao shen)
  • Date: Wed, 12 Sep 2012 15:57:06 +0800
Hi,

Does anyone know whether a function is defined in ghost code or not? From
my observation of a small test, the vghost of a varinfo of a
kernel_function is always false even the function is defined in ghost code.
Is it right?

Thanks,
Haihao
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120912/cf8a07bf/attachment.html>