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 get the function list from AST?

  • Subject: [Frama-c-discuss] How to get the function list from AST?
  • From: haihaoshen at gmail.com (haihao shen)
  • Date: Tue, 12 Jul 2011 16:38:44 +0800
Hi,

I have a test to get the function list from a file.

Basically, we could do the following steps "1. Ast.get() 2. traverse globals
and match the GFun".

However, for a file with only function declaration on implementation, we
could not get the function list from the globals. So, how to alleviate this
problem?

/*@
  behavior b1:
     assumes x > y;
     ensures \result == x;
  behavior b2:
     assumes x < y;
     ensures \result == y;
*/
int max (int a, int b);

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